Stream: Dune devs & users

Topic: Target to build coqtop and plugins but not Prelude.vo


view this post on Zulip Hugo Herbelin (Aug 26 2021 at 11:19):

A typical workflow I have is:

I can do that with dune exec -- coqtop.byte -l the_file.v when I know the file name and that works well. However, when the options on the command line are complicated, I would prefer to be able to redo coqtop and the cmxs and to restart the CI (with make ci-foo) so that the options are added automatically.

dune build dev/shim/coqtop-prelude almost do that except that it recompile Prelude.vo and forces to rebuild all v dependencies.

What would be the best approach? For instance, I'm thinking at adding a new target coqtop-binary to dev/shim/dune which would looks like the coqtop-prelude but replacing %{project_root}/theories/Init/Prelude.vo with the list of expected cmxs.

@Emilio Jesús Gallego Arias : Would it make sense?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 12:19):

I think that just rebuilding the coq-core package should do the trick

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 12:19):

something like dune build coq-core.install will build all public ML things

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 12:19):

and install them

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 12:21):

shim only exists because of limitation of the build / install layout

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 12:21):

and to gain a few miliseconds by more precise dependencies, but in your setup, coq-core will fit well IMHO

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 12:22):

Note you may need to build also coqide-server.install and coqide.install if you wanna use coqide

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 12:23):

Indeed if you wanna use the shim, you'd need a raw target after the install build tho, but if you are gonna call make ci-foo , then just the dune build will do the job

view this post on Zulip Hugo Herbelin (Aug 27 2021 at 15:19):

That seems to work. Thanks!


Last updated: Oct 16 2021 at 07:02 UTC