Allow compiling the packages with dune.

.gitignore

@@ -22,3 +22,5 @@ Makefile.package.*
 html/
 builddep/
 _opam
+_build/
+*.install

.gitlab-ci.yml

@@ -67,6 +67,14 @@ build-coq.8.19.0-mr:
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
+# Also ensure Dune works.
+build-coq.8.19.0-dune:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.19.0 dune   version 3.15.2"
+    MAKE_TARGET: "dune"
+
 # The oldest version runs in MRs, without name mangling.
 build-coq.8.18.0:
   <<: *template

CHANGELOG.md

@@ -7,6 +7,7 @@ API-breaking change is listed.
   `gmultiset_set_fold_comm_acc` to have more general type. (by Yannick Zakowski)
 - Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
   thereby make them consistent with the corresponding lemmas for sets.
+- Allow compiling the packages with dune (!552, by Rodolphe Lepigre).
 
 ## std++ 1.10.0 (2024-04-12)
 

Makefile

@@ -3,6 +3,12 @@ all: Makefile.coq
 	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are trick you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q stdpp stdpp
+-Q _build/default/stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
+-Q _build/default/stdpp_bitvector stdpp.bitvector
+-Q stdpp_unstable stdpp.unstable
+-Q _build/default/stdpp_unstable stdpp.unstable
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build stdpp/options.vo`. To build only
+the `stdpp` folder, you can do `dune build stdpp`.

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -argument-scope-delimiter)))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)

stdpp/dune

+(include_subdirs qualified)
+(coq.theory
+ (name stdpp)
+ (package coq-stdpp))

stdpp_bitvector/dune

+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.bitvector)
+ (package coq-stdpp-bitvector)
+ (theories stdpp))

stdpp_unstable/dune

+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.unstable)
+ (package coq-stdpp-unstable)
+ (theories stdpp stdpp.bitvector))