From 1e9cd3d63c9d6dd6947a258cd4f000b8d6681fd2 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
Date: Fri, 10 May 2024 15:57:22 +0200
Subject: [PATCH] Allow compiling the packages with dune.
---
.gitignore | 2 ++
.gitlab-ci.yml | 8 ++++++++
CHANGELOG.md | 1 +
Makefile | 6 ++++++
docs/dune.md | 45 ++++++++++++++++++++++++++++++++++++++++++++
dune | 7 +++++++
dune-project | 2 ++
stdpp/dune | 4 ++++
stdpp_bitvector/dune | 5 +++++
stdpp_unstable/dune | 5 +++++
10 files changed, 85 insertions(+)
create mode 100644 docs/dune.md
create mode 100644 dune
create mode 100644 dune-project
create mode 100644 stdpp/dune
create mode 100644 stdpp_bitvector/dune
create mode 100644 stdpp_unstable/dune
diff --git a/.gitignore b/.gitignore
index 847c638f..76f29b1c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,3 +22,5 @@ Makefile.package.*
html/
builddep/
_opam
+_build/
+*.install
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 74782b10..48b28040 100644
--- a/.gitlab-ci.yml
+++ b/.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
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 68701b60..5de5b303 100644
--- a/CHANGELOG.md
+++ b/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)
diff --git a/Makefile b/Makefile
index ac8dba01..c837f883 100644
--- a/Makefile
+++ b/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
diff --git a/docs/dune.md b/docs/dune.md
new file mode 100644
index 00000000..e45a0a3f
--- /dev/null
+++ b/docs/dune.md
@@ -0,0 +1,45 @@
+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`.
diff --git a/dune b/dune
new file mode 100644
index 00000000..822f87d0
--- /dev/null
+++ b/dune
@@ -0,0 +1,7 @@
+(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)))))
diff --git a/dune-project b/dune-project
new file mode 100644
index 00000000..8b858cde
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)
diff --git a/stdpp/dune b/stdpp/dune
new file mode 100644
index 00000000..d9ff07de
--- /dev/null
+++ b/stdpp/dune
@@ -0,0 +1,4 @@
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp)
+ (package coq-stdpp))
diff --git a/stdpp_bitvector/dune b/stdpp_bitvector/dune
new file mode 100644
index 00000000..c088d182
--- /dev/null
+++ b/stdpp_bitvector/dune
@@ -0,0 +1,5 @@
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.bitvector)
+ (package coq-stdpp-bitvector)
+ (theories stdpp))
diff --git a/stdpp_unstable/dune b/stdpp_unstable/dune
new file mode 100644
index 00000000..0c360b62
--- /dev/null
+++ b/stdpp_unstable/dune
@@ -0,0 +1,5 @@
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.unstable)
+ (package coq-stdpp-unstable)
+ (theories stdpp stdpp.bitvector))
--
GitLab