From 62893c44a5dcf9d7e3da93110ba431c48344ff04 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Sat, 6 Dec 2025 19:51:34 -0600 Subject: [PATCH 1/4] Set up basic dune build --- .gitignore | 1 + dune | 17 +++++++++++++++++ dune-project | 3 +++ external/Goose/github_com/mit_pdos/dune | 8 ++++++++ src/program_proof/dune | 8 ++++++++ 5 files changed, 37 insertions(+) create mode 100644 dune create mode 100644 dune-project create mode 100644 external/Goose/github_com/mit_pdos/dune create mode 100644 src/program_proof/dune diff --git a/.gitignore b/.gitignore index 9f8a828..b971c51 100644 --- a/.gitignore +++ b/.gitignore @@ -5,5 +5,6 @@ *.glob .*.aux .*.cache +_build/ # generated by rocq dep .rocqdeps.d diff --git a/dune b/dune new file mode 100644 index 0000000..e1fa3cf --- /dev/null +++ b/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 //'"))))) + diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..b918028 --- /dev/null +++ b/dune-project @@ -0,0 +1,3 @@ +(lang dune 3.17) +(using coq 0.10) + diff --git a/external/Goose/github_com/mit_pdos/dune b/external/Goose/github_com/mit_pdos/dune new file mode 100644 index 0000000..6acb335 --- /dev/null +++ b/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)) + diff --git a/src/program_proof/dune b/src/program_proof/dune new file mode 100644 index 0000000..59df0f0 --- /dev/null +++ b/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)) + From eafd208c58a261257128c9bebd48cae3f8160409 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Sat, 6 Dec 2025 20:10:55 -0600 Subject: [PATCH 2/4] Put code into packages --- dune-project | 7 +++++++ tulip-proof.opam | 7 ++----- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/dune-project b/dune-project index b918028..c6eb656 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +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")) + diff --git a/tulip-proof.opam b/tulip-proof.opam index c0533ef..a437931 100644 --- a/tulip-proof.opam +++ b/tulip-proof.opam @@ -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"] From fe97d7d0186c470c7cb032cdb8dc8167da292ef9 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Sat, 6 Dec 2025 20:27:52 -0600 Subject: [PATCH 3/4] Use only dune build --- .github/workflows/ci.yml | 2 +- Makefile | 48 ---------------------------------------- _RocqProject | 2 ++ 3 files changed, 3 insertions(+), 49 deletions(-) delete mode 100644 Makefile diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2ee9b41..5b91310 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Makefile b/Makefile deleted file mode 100644 index b093402..0000000 --- a/Makefile +++ /dev/null @@ -1,48 +0,0 @@ -SRC_DIR := '.' -PROJ_VFILES := $(shell find $(SRC_DIR) -name "*.v") - -# extract any global arguments for Rocq from _RocqProject -ROCQPROJECT_ARGS := $(shell sed -E -e '/^\#/d' -e "s/'([^']*)'/\1/g" -e 's/-arg //g' _RocqProject) - -# user configurable -Q:=@ -ROCQ_ARGS := -ROCQC := rocq compile -ROCQ_DEP_ARGS := -w +module-not-found - -default: vo -.PHONY: default - -vo: $(PROJ_VFILES:.v=.vo) -vos: $(PROJ_VFILES:.v=.vos) -vok: $(PROJ_VFILES:.v=.vok) - -.rocqdeps.d: $(PROJ_VFILES) _RocqProject - @echo "ROCQ dep $@" - $(Q)rocq dep $(ROCQ_DEP_ARGS) -vos -f _RocqProject $(PROJ_VFILES) > $@ - -# do not try to build dependencies if cleaning -ifeq ($(filter clean,$(MAKECMDGOALS)),) --include .rocqdeps.d -endif - -%.vo: %.v _RocqProject | .rocqdeps.d - @echo "ROCQ compile $<" - $(Q)$(ROCQC) $(ROCQPROJECT_ARGS) $(ROCQ_ARGS) -o $@ $< - -%.vos: %.v _RocqProject | .rocqdeps.d - @echo "ROCQ -vos $<" - $(Q)$(ROCQC) $(ROCQPROJECT_ARGS) -vos $(ROCQ_ARGS) $< -o $@ - -%.vok: %.v _RocqProject | .rocqdeps.d - @echo "ROCQ -vok $<" - $(Q)$(ROCQC) $(ROCQPROJECT_ARGS) -vok $(ROCQ_ARGS) $< -o $@ - -clean: - @echo "CLEAN vo glob aux" - $(Q)find $(SRC_DIR) \( -name "*.vo" -o -name "*.vo[sk]" \ - -o -name ".*.aux" -o -name ".*.cache" -o -name "*.glob" \) -delete - $(Q)rm -f .rocqdeps.d - -.PHONY: default -.DELETE_ON_ERROR: diff --git a/_RocqProject b/_RocqProject index 1c7fea2..c29b82b 100644 --- a/_RocqProject +++ b/_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 From 852f62bdcb741abf579c58d19546a0463900b646 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Sun, 7 Dec 2025 06:30:32 -0600 Subject: [PATCH 4/4] Trigger a new cache --- tulip-proof.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tulip-proof.opam b/tulip-proof.opam index a437931..38a0ca3 100644 --- a/tulip-proof.opam +++ b/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"