Support building with dune - #11
chandradeepdey wants to merge 1 commit into
Conversation
chandradeepdey
commented
Jun 9, 2026
chandradeepdey
commented
- following std++/Iris dune scripts
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
This PR updates the build/dependency tooling to support multi-package builds (main library + examples) and introduces dune/Rocq project-file generation helpers.
Changes:
- Add a per-package build/install helper (
make-package) and switch opam build/install commands to use it. - Introduce dune configuration for
cryptisandexamplesRocq theories plus shared flag generation. - Add scripts/config to generate
_RocqProjectand update Makefile/ignore rules accordingly.
Reviewed changes
Copilot reviewed 12 out of 13 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| rocq-cryptis.opam | Adds logpath tags and switches build/install to ./make-package. |
| rocq-cryptis-examples.opam | Adds a new opam package for building/installing examples separately. |
| make-package | New helper script to generate a per-package Rocq makefile and build/install it. |
| gen_RocqProject.sh | New generator for _RocqProject based on config/* inputs. |
| dune-project | Declares dune language version and enables rocq integration. |
| dune | Generates flags.dune from config/flags and applies flags to rocq builds. |
| cryptis/dune | Defines the main Rocq theory/package for dune builds. |
| examples/dune | Defines an examples Rocq theory/package for dune builds. |
| config/paths | Declares Rocq logical paths per package. |
| config/flags | Declares shared Rocq compilation flags. |
| _CoqProject | Removes flags/path directives, leaving a sources list layout. |
| Makefile | Switches to _RocqProject + rocq makefile, adds dune target, updates clean/builddep behavior. |
| .gitignore | Expands ignored build artifacts for Rocq/dune/opam workflows. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
9c6b414 to
ed64f46
Compare
There was a problem hiding this comment.
Isn't this a bit overkill? We don't have separate packages per se in this repository, unless we view the examples as a separate entity.
There was a problem hiding this comment.
I will remove the separate package for examples from this PR and rebase. But the plan is to eventually have separate packages.
There was a problem hiding this comment.
Removing separate packages is more work than I thought. Cryptis's directory structure is nice (cryptis and examples in separate directories). I don't think I want to change that, though I want to split out the Actris parts into a third directory (and the ReLoC parts into a fourth directory eventually). The way the scripts are designed to take one directory per line is also great, which I don't think I want to change.
Once the Actris dependency is added to opam, I will do the three directory split but with a single package. I will then rebase this on top of that, and we will have dune + three packages.
- following std++/Iris dune scripts
ed64f46 to
6a21100
Compare
|
Rebased, but it is dependent on #23 for now |
