Stream: Dune devs & users

Topic: Mixing coq & ocaml


view this post on Zulip Julien Puydt (May 25 2023 at 06:15):

My little experiment is an ocaml lib and an ocaml test ; the ocaml test is in fact supposed to be compiled, run to print (stdout) a coq file, which should then be fed to coq to check for correctness.

How does one do something like this?

view this post on Zulip Ali Caglayan (May 25 2023 at 19:11):

You can make a rule that runs the test that will output the .v file into a directory. That directory should have a coq.theory stanza and it will p;ick up the .v file.

view this post on Zulip Ali Caglayan (May 25 2023 at 19:16):

So if your ocaml executable is mytest.exe you can do a rule like

(rule
 (targets outfile.v)
 (action
  (run %{mytest.exe}}}}

{coq.theory
 (name mytest))

view this post on Zulip Julien Puydt (May 26 2023 at 07:51):

@Ali Caglayan thanks for you answer ; that set me on a better path:

(executable
  (name main_test)
  (libraries elaboration str))

(rule
  (target main_test.v)
  (deps (:main_test "main_test.exe"))
  (action (with-stdout-to %{target} (run %{main_test}))))

(coq.theory (name main_test.v))

but that makes the test run on "dune build" which wasn't my purpose, so I guess it isn't perfect yet...

view this post on Zulip Ali Caglayan (May 26 2023 at 09:05):

When you are running dune build you are really doing dune build @default. The default alias can be configured further but is by default @all. If you want to build the theory when building @runtest (that is what dune test(/runtest) builds), then you can add the targets of the coq theory to the alias using the (alias) stanza. Something like:

(alias
 (name runtest)
 (deps main_test.vo))

should work.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 01 2023 at 16:12):

This (name main_test.v) seems fishy

view this post on Zulip Emilio Jesús Gallego Arias (Jun 01 2023 at 16:13):

Indeed dune build means by default dune build @all , you may want to change that.


Last updated: May 25 2024 at 20:01 UTC