Karl Palmskog (Oct 23 2023 at 12:16): Karl Palmskog (Oct 23 2023 at 12:16):progressed a bit this weekend on a port to Dune of a really complicated extraction-based project currently using make+ocamlbuild: https://github.com/uwplse/verdi-raft
So far I only made Coq .vo Dune builds possible, but the rest seem within reach. The main lesson seems to be that Dune porting is made a lot easier by redesigning project directory structure, not least due to this bug: https://github.com/ocaml/dune/issues/8042
However, changing the directory structure can also seemingly make the project a bit more maintainable.
Emilio Jesús Gallego Arias (Oct 23 2023 at 14:04):Thanks for the very valuable feedback and work @Karl Palmskog , it is very important!
We are planning to do a Coq Dune hackaton soon, with the hopes to fix the last remaining issues you folks identified towards a 1.0 version; I've been a bit busy last weeks but we'll likely announce it soon.
Karl Palmskog (Oct 23 2023 at 14:16):I think Dune+Coq+extraction works best with the following structure:
theories for all .v except extraction preamble, including subdirectoriessrc for all OCaml code, with subdirectories for each module to extract and its .v preambletests for tests of executables built by extraction Karl Palmskog (Oct 23 2023 at 14:19):one final piece of the puzzle is what to do with shell scripts for running extracted executables with different parameters. It feels shaky to assume the executable lives in _build
Emilio Jesús Gallego Arias (Oct 23 2023 at 14:19):The structure sounds good; IMHO the philosophy with Dune is that when you follow its proposed structure, things should work "out of the box", but IMHO still should be possible to use config options to adapt to different structures users want. This has a maintenance cost tho, so how much configurability we want is a delicate balance.
Emilio Jesús Gallego Arias (Oct 23 2023 at 14:21):Karl Palmskog said:
one final piece of the puzzle is what to do with shell scripts for running extracted executables with different parameters. It feels shaky to assume the executable lives in
_build
Indeed; tho the build layout is a public interface I understand. There are two solutions that I know of for people not willing to use the _build path:
dune exec from the shell scriptany other option that would be convenient can be of course explored
Karl Palmskog (Oct 23 2023 at 14:36):dune exec in script probably makes the most sense for now
Emilio Jesús Gallego Arias (Oct 23 2023 at 14:37):Indeed. On the other side it is still a bit of PITA to use in some cases, the interface could use many improvements, but not sure how.
Typical is that for example people is using a profile, the dune exec without arguments uses other, etc...
Last updated: Oct 13 2024 at 01:02 UTC