Support building with dune

.gitignore

@@ -1,14 +1,33 @@
-*.aux
-*.v.d
 *.vo
-*.vok
 *.vos
-*RocqMakefile*
-.lia.cache
+*.vok
+*.vio
+*.v.d
+.coqdeps.d
 *.glob
+*.cache
+*.aux
+\#*\#
+.\#*
+*~
+*.bak
 .coqdeps.d
+.coq-native/
+*.crashcoqide
+.env
+builddep/
+_RocqProject
+_RocqProject.*
+Makefile.rocq
+Makefile.rocq.conf
+.Makefile.rocq.d
+Makefile.package.*
+.Makefile.package.*
+_opam
+_build
+*.install
+config/local-flags
 .envrc
 .direnv
-builddep
 rocq_mcp_cache_*
 .nia.cache

Makefile

@@ -1,29 +1,40 @@
 # Default target
-all: RocqMakefile
-	+@$(MAKE) -f RocqMakefile all
+all: Makefile.rocq
+	+@$(MAKE) -f Makefile.rocq 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
 
+# Generate the _RocqProject file.
+_RocqProject: gen_RocqProject.sh config/paths config/flags config/source-list $(wildcard config/local)
+	@./$< > $@
+
 # Forward most targets to Rocq makefile (with some trick to make this phony)
-%: RocqMakefile phony
+%: Makefile.rocq phony
 	@#echo "Forwarding $@"
-	+@$(MAKE) -f RocqMakefile $@
+	+@$(MAKE) -f Makefile.rocq $@
 phony: ;
 .PHONY: phony
 
-clean: RocqMakefile
-	+@$(MAKE) -f RocqMakefile clean
+clean: Makefile.rocq
+	+@$(MAKE) -f Makefile.rocq clean
 	@# Make sure not to enter the `_opam` folder.
 	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	find . -maxdepth 1 \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f RocqMakefile* .lia.cache builddep/*
+	rm -rf Makefile.rocq Makefile.rocq.conf .lia.cache builddep/* _build */_RocqProject
+	# We do not clean _RocqProject since ProofGeneral and other editors need that,
+	# and 'make clean' is often needed to remove the .vo files after a dependency update.
 .PHONY: clean
 
 # Create Rocq Makefile.
-RocqMakefile: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o RocqMakefile $(EXTRA_COQFILES)
+Makefile.rocq: _RocqProject Makefile
+	"$(COQBIN)rocq" makefile -f _RocqProject -o Makefile.rocq $(EXTRA_COQFILES)
 
 # Install build-dependencies
 OPAMFILES=$(wildcard *.opam)
@@ -47,6 +58,10 @@ builddep: builddep-opamfiles
 	@opam install $(OPAMFLAGS) -y $(BUILDDEPFILES)
 .PHONY: builddep
 
-# Some files that do *not* need to be forwarded to RocqMakefile.
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
+# Some files that do *not* need to be forwarded to Makefile.rocq.
 # ("::" lets Makefile.local overwrite this.)
-Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
+Makefile Makefile.local config/paths config/flags config/source-list config/local $(OPAMFILES):: ;

config/flags

@@ -0,0 +1,14 @@
+# Specification for custom Rocq compilation flags (turns into `-arg` values in `_RocqProject`).
+# Syntax:
+# - One flag per line with no leading/trailing blanks.
+# - Empty lines and lines starting with '#' are ignored.
+
+# We sometimes want to locally override notation, and there is no good way to do
+# that with scopes.
+-w
+-notation-overridden
+
+# Cannot use non-canonical projections as it causes massive unification failures
+# (https://github.com/coq/coq/issues/6294).
+-w
+-redundant-canonical-projection

config/paths

@@ -0,0 +1,6 @@
+# Search paths for all packages.
+# Each line should be of the form "<PACKAGE> <LOGICAL_PATH>",
+# where <PACKAGE> is the name of a directory that matches the
+# corresponding package name.
+cryptis cryptis
+examples cryptis.examples

_CoqProject → config/source-list

@@ -1,9 +1,4 @@
--arg "-w -convert_concl_no_check"
--arg "-w -redundant-canonical-projection"
--arg "-w -notation-overridden"
-
--R examples cryptis.examples
--R cryptis cryptis
+# List of source files included in the libraries.
 
 cryptis/lib/mathcomp_compat.v
 cryptis/lib/list_sort.v
@@ -101,6 +96,8 @@ examples/alist/impl.v
 examples/alist/proofs.v
 examples/alist.v
 
+## Storage
+
 examples/store.v
 examples/store/impl.v
 examples/store/proofs/base.v
@@ -122,11 +119,12 @@ examples/store/game.v
 
 examples/permanent.v
 examples/counter.v
-examples/nsl_secr.v
-examples/nsl_auth.v
 
 ## NSL
 
+examples/nsl_secr.v
+examples/nsl_auth.v
+
 ## CR
 
 examples/challenge_response.v
@@ -170,4 +168,3 @@ examples/store_sess/proofs/client.v
 examples/store_sess/proofs/server.v
 examples/store_sess/proofs.v
 examples/store_sess/game.v
-

cryptis/dune

@@ -0,0 +1,6 @@
+(include_subdirs qualified)
+(rocq.theory
+ (name cryptis)
+ (package rocq-cryptis)
+ (generate_project_file)
+ (theories Stdlib Ltac2 HB elpi elpi_elpi mathcomp deriving stdpp iris))

dune

@@ -0,0 +1,12 @@
+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (rocq
+   ; Configure rocq flags.
+   (flags (:standard %{read-lines:flags.dune})))))
+
+(rule
+ (action
+  (with-stdout-to flags.dune
+   (pipe-stdout
+    (cat config/flags)
+    (bash "grep '^[^#]\\+' || true")))))

dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.21)
+(using rocq 0.11)

examples/dune

@@ -0,0 +1,6 @@
+(include_subdirs qualified)
+(rocq.theory
+ (name cryptis.examples)
+ (package rocq-cryptis-examples)
+ (generate_project_file)
+ (theories cryptis))

gen_RocqProject.sh

@@ -0,0 +1,22 @@
+#!/bin/sh
+set -e
+# Script generating the contents of [_RocqProject] based on files [config/*].
+
+echo "# Generated file, edit [config/*] instead."
+
+echo
+echo "# Search paths"
+# Adding "-Q " prefix to all non-empty, non-comment lines of [config/paths].
+cat config/paths | grep "^[^#]\+" | sed "s/^/-Q /"
+
+echo
+echo "# Flags"
+# Adding "-arg " prefix to all non-empty, non-comment lines of [config/flags]
+# after adding quotes around each line.
+cat config/flags | grep "^[^#]\+" | sed "s/\(.*\)/\"\1\"/" | sed "s/^/-arg /"
+
+# List of source files.
+echo
+echo "# Sources"
+# Take only non-empty, non-comment lines of [config/source-list].
+cat config/source-list | grep "^[^#]\+"

make-package

@@ -0,0 +1,44 @@
+#!/bin/sh
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+# Make sure we get a GNU version of make.
+# This is exactly how opam determines which make executable to use.
+OS=$(uname)
+MAKE="make"
+if [ "$OS" = "FreeBSD" ] || [ "$OS" = "OpenBSD" ] ||\
+       [ "$OS" = "NetBSD" ] || [ "$OS" = "DragonFly" ]; then
+    MAKE="gmake"
+fi
+
+PROJECT="$1"
+shift
+
+ROCQFILE="_RocqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+# Ensure we have an up-to-date _RocqProject file.
+$MAKE _RocqProject
+
+if ! grep -E -q "^$PROJECT/" _RocqProject; then
+    echo "No files in $PROJECT/ found in _RocqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _RocqProject file and Makefile
+rm -f "$ROCQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _RocqProject >> "$ROCQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _RocqProject | grep -E -v "^-Q " >> "$ROCQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _RocqProject >> "$ROCQFILE"
+# Now we can generate the makefile.
+"${COQBIN}rocq" makefile -f "$ROCQFILE" -o "$MAKEFILE"
+
+# Run build
+$MAKE -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*

rocq-cryptis-examples.opam

@@ -0,0 +1,17 @@
+opam-version: "2.0"
+name: "rocq-cryptis-examples"
+version: "dev"
+license: "MIT"
+maintainer: "Arthur Azevedo de Amorim <arthur.aa@gmail.com>"
+authors: "Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi"
+synopsis: "Cryptis: Cryptographic Reasoning in Separation Logic"
+homepage: "https://github.com/arthuraa/cryptis"
+bug-reports: "https://github.com/arthuraa/cryptis/issues"
+dev-repo: "git+https://github.com/arthuraa/cryptis.git"
+
+depends: [
+  "rocq-cryptis" {= version}
+]
+
+build: ["./make-package" "examples" "-j%{jobs}%"]
+install: ["./make-package" "examples" "install"]

rocq-cryptis.opam

@@ -9,6 +9,13 @@ homepage: "https://github.com/arthuraa/cryptis"
 bug-reports: "https://github.com/arthuraa/cryptis/issues"
 dev-repo: "git+https://github.com/arthuraa/cryptis.git"
 
+tags: [
+  "logpath:cryptis.lib"
+  "logpath:cryptis.core"
+  "logpath:cryptis.primitives"
+  "logpath:cryptis"
+]
+
 depends: [
   "rocq-prover"
   "rocq-core" {= "9.1.1"}
@@ -18,5 +25,5 @@ depends: [
   "rocq-iris-heap-lang" {= "4.5.0"}
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "cryptis" "-j%{jobs}%"]
+install: ["./make-package" "cryptis" "install"]