Switch to dune build

.github/workflows/ci.yml

@@ -23,7 +23,7 @@ jobs:
           opam pin add --no-action .
           opam install --deps-only .
       - name: Rocq build
-        run: make -j4
+        run: dune build
       - name: opam install
         run: opam install --assume-built .
       - name: opam uninstall

.gitignore

@@ -5,5 +5,6 @@
 *.glob
 .*.aux
 .*.cache
+_build/
 # generated by rocq dep
 .rocqdeps.d

_RocqProject

@@ -1,5 +1,7 @@
 -Q src Perennial
 -Q external/Goose Goose
+-Q _build/default/src Perennial
+-Q _build/default/external/Goose Goose
 -arg -w -arg +deprecated-instance-without-locality
 # don't allow ambiguous coercions
 -arg -w -arg +ambiguous-paths

dune

@@ -0,0 +1,17 @@
+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   ; Configure coqc flags.
+   (flags (:standard %{read-lines:flags.dune})))))
+
+(rule
+ (action
+  (with-stdout-to flags.dune
+   (pipe-stdout
+    (cat _RocqProject)
+    ; delete comments
+    (bash "sed -E -e '/^#/d'")
+    ; get only args (not logical paths)
+    (bash "grep -o -- '-arg [^ ]*'")
+    (bash "sed -E -e 's/-arg //'")))))
+

dune-project

@@ -0,0 +1,10 @@
+(lang dune 3.17)
+(using coq 0.10)
+
+(package
+  (name tulip-code)
+  (synopsis "tulip translated code"))
+(package
+  (name tulip-proof)
+  (synopsis "tulip program proof"))
+

external/Goose/github_com/mit_pdos/dune

@@ -0,0 +1,8 @@
+(include_subdirs qualified)
+(coq.theory
+ (name Goose.github_com.mit_pdos)
+ (package tulip-code)
+ (theories Stdlib Ltac2 stdpp iris
+           coqutil RecordUpdate iris_named_props
+           Perennial Goose))
+

src/program_proof/dune

@@ -0,0 +1,8 @@
+(include_subdirs qualified)
+(coq.theory
+ (name Perennial.program_proof)
+ (package tulip-proof)
+ (theories Stdlib Ltac2 stdpp iris
+           coqutil RecordUpdate iris_named_props
+           Goose Goose.github_com.mit_pdos Perennial))
+

tulip-proof.opam

@@ -6,7 +6,7 @@ homepage: "https://github.com/mit-pdos/tulip-proof"
 bug-reports: "https://github.com/mit-pdos/tulip-proof/issues"
 dev-repo: "git+https://github.com/mit-pdos/tulip-proof.git"
 version: "dev"
-synopsis: "Verification of tulip"
+synopsis: "Program proofs for tulip"
 
 depends: [
   "perennial-old"
@@ -23,8 +23,5 @@ pin-depends: [
   ## end
 ]
 
-build: [make "-j%{jobs}%"]
-install: ["go" "tool" "perennial-cli" "install"]
-build-env: [
-  [GOCACHE = "%{build}%/_build/.gocache"]
-]
+build: ["dune" "build"]
+install: ["dune" "install"]