From e4446d9a2ffbf3eaa1736917764c85ec390e6788 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Jun 2025 14:43:43 +0200 Subject: [PATCH 01/11] Waterproof proof mode: first prototype. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Joint work with Gaëtan Gilbert, Pim Otte, Jim Portegies. --- .gitmodules | 4 ++-- Makefile | 2 +- coq-waterproof | 2 +- rocq | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.gitmodules b/.gitmodules index 5686103..5a6c8ce 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "rocq"] path = rocq - url = git@github.com:rocq-prover/rocq.git + url = git@github.com:ejgallego/coq.git [submodule "stdlib"] path = stdlib url = git@github.com:rocq-prover/stdlib.git @@ -9,4 +9,4 @@ url = git@github.com:ejgallego/coq-lsp.git [submodule "coq-waterproof"] path = coq-waterproof - url = git@github.com:impermeable/coq-waterproof.git + url = git@github.com:ejgallego/coq-waterproof.git diff --git a/Makefile b/Makefile index 06b1396..e0faf7d 100644 --- a/Makefile +++ b/Makefile @@ -37,7 +37,7 @@ clean: # Test .PHONY: test -launch: build +test: build echo "Test not implemented" # Launch where the _CoqProject file is diff --git a/coq-waterproof b/coq-waterproof index dd712eb..e89f108 160000 --- a/coq-waterproof +++ b/coq-waterproof @@ -1 +1 @@ -Subproject commit dd712eb0b7f5c205870dbd156736a684d40eeb9a +Subproject commit e89f1081c995bf970cd49b872f0ca2aa168b387b diff --git a/rocq b/rocq index be26673..e281e88 160000 --- a/rocq +++ b/rocq @@ -1 +1 @@ -Subproject commit be266736842a4ee7ef860bb7d7dc24769596a635 +Subproject commit e281e88b86fa2b782cf5f78a4434a2f2572c4d81 From 2373f93181065e0933d540eb127b5f319508c08a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Jun 2025 14:43:40 +0200 Subject: [PATCH 02/11] Version with parsing debug info. --- Makefile | 2 +- coq-waterproof | 2 +- rocq | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index e0faf7d..5b5e7f1 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ PKG_SET=coq-lsp/coq-lsp.install rocq/coq-core.install rocq/rocq-core.install roc .PHONY: build build: rocq/config/coq_config.ml - dune build $(PKG_SET) + dune build $(DUNEOPT) $(PKG_SET) # Ideally we could regenerate this on Rocq updates, usually not needed rocq/config/coq_config.ml: rocq diff --git a/coq-waterproof b/coq-waterproof index e89f108..3e336db 160000 --- a/coq-waterproof +++ b/coq-waterproof @@ -1 +1 @@ -Subproject commit e89f1081c995bf970cd49b872f0ca2aa168b387b +Subproject commit 3e336db3408a5b0784804cfd4aa6a6fb513e226b diff --git a/rocq b/rocq index e281e88..c45c1a3 160000 --- a/rocq +++ b/rocq @@ -1 +1 @@ -Subproject commit e281e88b86fa2b782cf5f78a4434a2f2572c4d81 +Subproject commit c45c1a3d2cbc6512b3b12caac6b5f08f20fc0798 From 434e3ffc2f684e07b2a9c7721c65376b267e9e30 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Jun 2025 15:14:56 +0200 Subject: [PATCH 03/11] Better printing --- rocq | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rocq b/rocq index c45c1a3..890701e 160000 --- a/rocq +++ b/rocq @@ -1 +1 @@ -Subproject commit c45c1a3d2cbc6512b3b12caac6b5f08f20fc0798 +Subproject commit 890701e63901229551236ac57e967e835faaddef From 5deee01fb5e71879570aa1e0ea25f250fe442ed1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 25 Jun 2025 15:58:44 +0200 Subject: [PATCH 04/11] update rocq --- rocq | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rocq b/rocq index 890701e..6f2f9c2 160000 --- a/rocq +++ b/rocq @@ -1 +1 @@ -Subproject commit 890701e63901229551236ac57e967e835faaddef +Subproject commit 6f2f9c22006f66f464dee8056c345e292b408d10 From 7e8325716a8c8ce16828d65a0064eb8a13687ad0 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Wed, 25 Jun 2025 16:13:27 +0200 Subject: [PATCH 05/11] coq-waterproof improvements --- coq-waterproof | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-waterproof b/coq-waterproof index 3e336db..f2850e6 160000 --- a/coq-waterproof +++ b/coq-waterproof @@ -1 +1 @@ -Subproject commit 3e336db3408a5b0784804cfd4aa6a6fb513e226b +Subproject commit f2850e6ec019b0c32de986ef80bb9a95300f243f From 204087ab742e9a7cb29680ccf5c50979abf9324d Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Wed, 25 Jun 2025 16:25:37 +0200 Subject: [PATCH 06/11] Better error --- coq-waterproof | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-waterproof b/coq-waterproof index f2850e6..c9c0046 160000 --- a/coq-waterproof +++ b/coq-waterproof @@ -1 +1 @@ -Subproject commit f2850e6ec019b0c32de986ef80bb9a95300f243f +Subproject commit c9c00466e3b35fe59c393eb2dedfa7a334c67a5c From 8c509c582196681ea611e9d192cbfb14f8a7d6bc Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Wed, 25 Jun 2025 16:37:00 +0200 Subject: [PATCH 07/11] Point submodules to impermeable forks --- .gitmodules | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.gitmodules b/.gitmodules index 5a6c8ce..ba63d1a 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "rocq"] path = rocq - url = git@github.com:ejgallego/coq.git + url = git@github.com:impermeable/rocq.git [submodule "stdlib"] path = stdlib url = git@github.com:rocq-prover/stdlib.git @@ -9,4 +9,4 @@ url = git@github.com:ejgallego/coq-lsp.git [submodule "coq-waterproof"] path = coq-waterproof - url = git@github.com:ejgallego/coq-waterproof.git + url = git@github.com:impermeable/coq-waterproof.git From 5430bf160faf261e1dbda0c2bb8fab0a2714471b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 25 Jun 2025 17:27:45 +0200 Subject: [PATCH 08/11] update rocq --- rocq | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rocq b/rocq index 6f2f9c2..7953d1e 160000 --- a/rocq +++ b/rocq @@ -1 +1 @@ -Subproject commit 6f2f9c22006f66f464dee8056c345e292b408d10 +Subproject commit 7953d1e648fc0c3047b46484c980595923b83465 From c4a1e0c180935655dcce2a0b9cc3eb3c8a542496 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Wed, 25 Jun 2025 17:35:10 +0200 Subject: [PATCH 09/11] Fix some tests --- coq-waterproof | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-waterproof b/coq-waterproof index c9c0046..9f01a2e 160000 --- a/coq-waterproof +++ b/coq-waterproof @@ -1 +1 @@ -Subproject commit c9c00466e3b35fe59c393eb2dedfa7a334c67a5c +Subproject commit 9f01a2e2351683252e47fc150e23bdbd918eb5be From 46f58474464a7182e0bbcceea04fe1fe30f2d2c4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Jun 2025 11:36:43 +0200 Subject: [PATCH 10/11] [build] Small updates to README and gitmodule setup We now specify that both Rocq and Waterproof submodules are associated to the wp_proof_mode branch. This makes rebases easier. --- .gitmodules | 8 +++++--- README.md | 16 ++++++++++++++-- 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/.gitmodules b/.gitmodules index ba63d1a..5fb5ef3 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,12 +1,14 @@ [submodule "rocq"] path = rocq url = git@github.com:impermeable/rocq.git + branch = wp_proof_mode +[submodule "coq-waterproof"] + path = coq-waterproof + url = git@github.com:impermeable/coq-waterproof.git + branch = wp_proof_mode [submodule "stdlib"] path = stdlib url = git@github.com:rocq-prover/stdlib.git [submodule "coq-lsp"] path = coq-lsp url = git@github.com:ejgallego/coq-lsp.git -[submodule "coq-waterproof"] - path = coq-waterproof - url = git@github.com:impermeable/coq-waterproof.git diff --git a/README.md b/README.md index 017fcfc..5e0c0c8 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,10 @@ ## Waterproof Dev environment -This is a meta-project providing a setup to build coq-waterproof against the Rocq master branch along with master branches of other tools. +This is a meta-project providing a setup to build coq-waterproof +against the Rocq master branch along with master branches of other +tools. -Building is done using `make all`. +Building is done using `make`. To use `coq-lsp` in vscode, one can then run @@ -16,3 +18,13 @@ To execute tests against the Waterproof exercises, run ``` dune test ``` +## Branch setup for the composed build + +As of today, we have two specific branches for the Waterproof proof +mode setup, in particular for Rocq and Waterproof, we store the +changes in the `wp_proof_mode` branch at the impermeable repository: + +- https://github.com/impermeable/coq-waterproof/tree/wp_proof_mode +- https://github.com/impermeable/rocq/tree/wp_proof_mode +- stdlib: we use the main branch +- coq-lsp: we use the main branch From 8adaf681ac2a92e25f6212639dc26f32b032ea1b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 25 Nov 2025 10:43:30 +0100 Subject: [PATCH 11/11] Rebase to latest Rocq, WP, and rocq-lsp --- coq-lsp | 2 +- coq-waterproof | 2 +- rocq | 2 +- stdlib | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/coq-lsp b/coq-lsp index 8812ff6..f6e6fb8 160000 --- a/coq-lsp +++ b/coq-lsp @@ -1 +1 @@ -Subproject commit 8812ff6b00d5738517c5e40af94e0ad4988176ef +Subproject commit f6e6fb8204a3ace6420d072bb4b75bf7f56104ca diff --git a/coq-waterproof b/coq-waterproof index 9f01a2e..fa829a1 160000 --- a/coq-waterproof +++ b/coq-waterproof @@ -1 +1 @@ -Subproject commit 9f01a2e2351683252e47fc150e23bdbd918eb5be +Subproject commit fa829a15899ede5029eebbedd498b16a9455d3e9 diff --git a/rocq b/rocq index 7953d1e..3f5e263 160000 --- a/rocq +++ b/rocq @@ -1 +1 @@ -Subproject commit 7953d1e648fc0c3047b46484c980595923b83465 +Subproject commit 3f5e26306a082b8ffd038ffb79059eb242f5e46a diff --git a/stdlib b/stdlib index 71a6beb..e343c58 160000 --- a/stdlib +++ b/stdlib @@ -1 +1 @@ -Subproject commit 71a6beb0b14452fe8042d1c010b56be4b66403c0 +Subproject commit e343c58314f5a902e08ec6a211f4e1b5812a8c89