Stream: Dune devs & users

Topic: Mixing coq & ocaml

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?

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.

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))

Julien Puydt (May 26 2023 at 07:51):

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

• I enabled coq in dune-project ;
• I rewrote my test/dune to:

(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...

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.

Emilio Jesús Gallego Arias (Jun 01 2023 at 16:12):

This (name main_test.v) seems fishy

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: Sep 15 2024 at 13:02 UTC