Waterproof proof mode: first prototype.

.gitmodules

@@ -1,12 +1,14 @@
 [submodule "rocq"]
 	path = rocq
-	url = git@github.com:rocq-prover/rocq.git
+	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

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
@@ -37,7 +37,7 @@ clean:
 
 # Test
 .PHONY: test
-launch: build
+test: build
 	echo "Test not implemented"
 
 # Launch where the _CoqProject file is

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