Merge branch 'rodolphe/dune' into 'master'

Allow compiling the packages with dune.

See merge request iris/iris!1056

.gitignore

@@ -23,3 +23,5 @@ Makefile.coq.conf
 Makefile.package.*
 .Makefile.package.*
 _opam
+_build
+*.install

.gitlab-ci.yml

@@ -67,6 +67,14 @@ build-coq.8.19.1-mr:
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
+# Also ensure Dune works.
+build-coq.8.19.1-dune:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.19.1   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

@@ -17,6 +17,10 @@ lemma.
 * Add lemma `na_own_empty` and persistence instance for `na_own p ∅` for
   non-atomic invariant tokens. (by Benjamin Peters)
 
+**Infrastructure:**
+
+* Add support for compiling the packages with dune. (by Rodolphe Lepigre) 
+
 ## Iris 4.2.0 (2024-04-12)
 
 The highlights of this release are:

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
 

_CoqProject

@@ -10,6 +10,8 @@
 -Q iris_heap_lang iris.heap_lang
 -Q iris_unstable iris.unstable
 -Q iris_deprecated iris.deprecated
+
+# Custom flags (to be kept in sync with the dune file at the root of the repo).
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures

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 tricks 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 iris iris
+-Q _build/default/iris iris
+-Q iris_heap_lang iris.heap_lang
+-Q _build/default/iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q _build/default/iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+-Q _build/default/iris_deprecated iris.deprecated
+```
+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 iris/prelude/options.vo`. To build
+only the `iris` folder, you can do `dune build iris`.

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 -notation-overridden
+     -w -redundant-canonical-projection
+     -w -unknown-warning
+     -w -argument-scope-delimiter)))))

dune-project

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

iris/dune

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

iris_deprecated/dune

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

iris_heap_lang/dune

+(include_subdirs qualified)
+(coq.theory
+ (name iris.heap_lang)
+ (package coq-iris-heap-lang)
+ (theories stdpp iris))

iris_unstable/dune

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