Dune Working Group

The Dune Hacking Event and Working Group Summer 2022 Edition will take place Wed June 22th 2022 , 4pm-7pm Paris time.

We will use Zoom https://wesleyan.zoom.us/j/8577973776

We are using this Zulip topic for coordination: https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/Dune.20Hacking.20event

Log

• Implementation of queries to Coq (such as %{coq:config}) so we (and users) can setup conditional rules. We implemented a coq-version variable. Questions about what that variable means were raised. PRs submitted

  • https://github.com/ocaml/dune/pull/5913
  • https://github.com/ocaml/dune/pull/5914

• Michael Soegtrop did a review of Dune documentation and terminology, and discussed their notes.

  • Notes here https://github.com/ocaml/dune/issues/5915

• Discussion over warnings was held, very interesting points reached.

• We also discussed on-demand compilation and deeper integration of Coq with Dune.

Topics for discussion

Here are some preliminary things we might like to discuss / work on in this working group.

The Coq Dune project

https://github.com/coq/coq/projects/15

Topics for discussion:

• Benefits of using dune
• Converting your Coq project to dune
• Advanced dune / Coq usage (plugins etc)
• (opam) Packaging with help from dune
• Hacking on dune itself

Issues

• https://github.com/ocaml/dune/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+label%3Acoq

Improvements to coq stanza

• Composing installed libs (This should be top priority IMO) (Ali)
• Coqdoc support (+ other documentation support, alectryon, dpdgraph, proviola) (Ali)
  • In progress https://github.com/ocaml/dune/pull/5695 (done)
  • Lots to improve here IMO.
• coqchk rules (Ali)
• Error on warning for Coq (Ali) (I think we already have this?)
• Native support (e.g. not building by default, but declaring .cmxs targets anyway) (Ali)
• Vos, vok support (Should be configurable, perhaps with a mode?) (Ali)
• vio, vio2vo support (do we want to support this? I hear no, but it still exists) (Ali)
• Extraction: https://github.com/ocaml/dune/issues/4158 https://github.com/coq/coq/pull/16126
• coqffi https://github.com/ocaml/dune/pull/4007
• Install rules for Coq
• Compositionality (done for workspaces)
• External dependencies (external libs)
• Sandboxing for coq theory rules

Dune usability

• dune init for Coq projects and plugin projects (Ali)
• Fixing watch mode: (Ali)
  • https://github.com/ocaml/dune/issues/5449
  • https://github.com/ocaml/dune/pull/5450

Dune performance

• Possible mutable state in watch mode: https://github.com/ocaml/dune/issues/5549 (Ali)

Participants

• Emilio J. Gallego Arias
• Ali Caglayan
• Rudi Grinberg