Hugo Herbelin (Aug 26 2021 at 11:19): Hugo Herbelin (Aug 26 2021 at 11:19):A typical workflow I have is:
v fileI 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?
Emilio Jesús Gallego Arias (Aug 26 2021 at 12:19):I think that just rebuilding the coq-core package should do the trick
Emilio Jesús Gallego Arias (Aug 26 2021 at 12:19):something like dune build coq-core.install will build all public ML things
Emilio Jesús Gallego Arias (Aug 26 2021 at 12:19):and install them
Emilio Jesús Gallego Arias (Aug 26 2021 at 12:21):shim only exists because of limitation of the build / install layout
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
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
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
Hugo Herbelin (Aug 27 2021 at 15:19):That seems to work. Thanks!
Last updated: Jun 03 2023 at 18:01 UTC