Stream: Dune devs & users

Topic: Port of Verdi Raft to Dune


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 23 2023 at 14:16):

I think Dune+Coq+extraction works best with the following structure:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

any other option that would be convenient can be of course explored

view this post on Zulip Karl Palmskog (Oct 23 2023 at 14:36):

dune exec in script probably makes the most sense for now

view this post on Zulip 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: May 25 2024 at 21:01 UTC