DuneWG 2022
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
-
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
-
Michael Soegtrop did a review of Dune documentation and terminology, and discussed their notes.
-
Discussion over warnings was held, very interesting points reached.
-
We also discussed on-demand compilation and deeper integration of Coq with Dune.
Here are some preliminary things we might like to discuss / work on in this working group.
https://github.com/coq/coq/projects/15
- 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
- https://github.com/ocaml/dune/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+label%3Acoq
- 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 init for Coq projects and plugin projects (Ali)
- Fixing watch mode: (Ali)
- Possible mutable state in watch mode: https://github.com/ocaml/dune/issues/5549 (Ali)
- Emilio J. Gallego Arias
- Ali Caglayan
- Rudi Grinberg
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.