From e87cfb850bedf8e3b6456bc48b58ae2780143a09 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 1 Jan 2025 07:02:07 +0100
Subject: [PATCH 1/3] Remove rocq-doc submodule

---
 .gitmodules | 3 ---
 rocq-doc    | 1 -
 2 files changed, 4 deletions(-)
 delete mode 160000 rocq-doc

diff --git a/.gitmodules b/.gitmodules
index 6b5bb9e44..e69de29bb 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +0,0 @@
-[submodule "rocq-doc"]
-	path = rocq-doc
-	url = https://github.com/coq/doc
diff --git a/rocq-doc b/rocq-doc
deleted file mode 160000
index df17f8071..000000000
--- a/rocq-doc
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit df17f8071a472d582cb3dab8fbdc2c1594c9e9f7

From adc17dbca232b0c919202d5ec150674e6ad40642 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 1 Jan 2025 07:12:41 +0100
Subject: [PATCH 2/3] Handle the local copy of the documentation in the
 Makefile

---
 Makefile | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 62d2e9d49..0debc0c99 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,5 @@
 .DEFAULT_GOAL := all
+DOC_PATH=`pwd`/rocq-doc/
 
 .PHONY: all
 all:
@@ -32,8 +33,18 @@ playground:
 install: all ## Install the packages on the system
 	opam exec -- dune install --root .
 
+.PHONY: local-doc
+local-doc:
+	if [ -d rocq-doc ]; then cd rocq-doc && git pull; \
+	else git clone --depth 1 https://github.com/coq/doc.git rocq-doc; fi
+
+.PHONY: update-local-doc
+update-local-doc:
+	@if [ -d rocq-doc ]; then cd rocq-doc && git pull; \
+	else echo "No local doc copy, use \"make local-doc\" to get a local copy (~ 8 GB)"; fi
+
 .PHONY: start
-start: all ## Run the produced executable
+start: all update-local-doc ## Run the produced executable
 	opam exec -- dune exec src/rocqproverorg_web/bin/main.exe
 
 .PHONY: test
@@ -51,11 +62,9 @@ doc: ## Generate odoc documentation
 .PHONY: fmt
 fmt: ## Format the codebase with ocamlformat
 	opam exec -- dune build --root . --auto-promote @fmt
-
-DOC_PATH=`pwd`/rocq-doc/
 	
 .PHONY: watch
-watch: ## Watch for the filesystem and rebuild on every change
+watch: update-local-doc ## Watch for the filesystem and rebuild on every change
 	DOC_PATH=${DOC_PATH} opam exec -- dune build @run -w --force --no-buffer
 
 .PHONY: utop

From 9cc2234df91a302906cb1c0aada0392fde191afb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 1 Jan 2025 07:25:03 +0100
Subject: [PATCH 3/3] Disable format code step for now

---
 .github/workflows/ci.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 1d08ec058..28671fb33 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -58,6 +58,6 @@ jobs:
       - name: Run tests
         run: opam exec -- dune test
 
-      - name: Format code
-        run: opam exec -- dune build --auto-promote @fmt
-        if: runner.os == 'Linux'
+#      - name: Format code
+#        run: opam exec -- dune build --auto-promote @fmt
+#        if: runner.os == 'Linux'