From 6752d5babd739684367416cad6ddb4462d788d8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 16 Jul 2024 15:24:42 +0200
Subject: [PATCH] "make world" and dune default target don't build coqide

makefile: add coqide target

The current behaviour seems mostly annoying to those who don't care
about coqide.
---
 .gitlab-ci.yml                                   |  2 +-
 Makefile                                         | 16 ++++++++++------
 .../19378-make-world-coqide.rst                  |  5 +++++
 dune                                             |  2 +-
 4 files changed, 17 insertions(+), 8 deletions(-)
 create mode 100644 doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9878c3fe50b7a..3137df4b4632d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -110,7 +110,7 @@ before_script:
     - make $DUNE_TARGET
     - tar cfj _build.tar.bz2 _build
   variables:
-    DUNE_TARGET: world
+    DUNE_TARGET: "world coqide"
   artifacts:
     name: "$CI_JOB_NAME"
     when: always
diff --git a/Makefile b/Makefile
index 6ffda3eacc840..c3e76d9c46b07 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@
 
 # Dune Makefile for Coq
 
-.PHONY: help help-install states world watch check    # Main developer targets
+.PHONY: help help-install states world coqide watch check    # Main developer targets
 .PHONY: refman-html refman-pdf stdlib-html apidoc     # Documentation targets
 .PHONY: test-suite dev-targets
 .PHONY: fmt ocheck obuild ireport clean               # Maintenance targets
@@ -39,8 +39,9 @@ help:
 	@echo "make help-install for installation instructions. Common developer targets are:"
 	@echo ""
 	@echo "  - states: build a minimal functional coqtop"
-	@echo "  - world:  build all public binaries and libraries in developer mode"
-	@echo "  - watch:  build all public binaries and libraries [continuous build]"
+	@echo "  - world:  build main public binaries and libraries in developer mode (no coqide)"
+	@echo "  - watch:  build main public binaries and libraries [continuous build]"
+	@echo "  - coqide: build coqide binary in developer mode"
 	@echo "  - check:  build all ML files as fast as possible"
 	@echo "  - test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]"
 	@echo "  - dunestrap: Generate the dune rules for vo files"
@@ -145,13 +146,16 @@ dunestrap: $(DUNE_FILES)
 states: dunestrap
 	dune build $(DUNEOPT) dev/shim/coqtop
 
-NONDOC_INSTALL_TARGETS:=coq-core.install coq-stdlib.install coqide-server.install coqide.install coq.install
+MAIN_TARGETS:=coq-core.install coq-stdlib.install coqide-server.install coq.install
 
 world: dunestrap
-	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS)
+	dune build $(DUNEOPT) $(MAIN_TARGETS)
+
+coqide:
+	dune build $(DUNEOPT) coqide.install
 
 watch:
-	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w
+	dune build $(DUNEOPT) $(MAIN_TARGETS) -w
 
 check:
 	dune build $(DUNEOPT) @check
diff --git a/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst b/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst
new file mode 100644
index 0000000000000..d23e128dffde6
--- /dev/null
+++ b/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  when building Coq, the makefile's `world` target and `dune build`'s default target do not build coqide anymore.
+  Use `make world coqide` or `dune build @default coqide.install` to build what they respectively used to build
+  (`#19378 <https://github.com/coq/coq/pull/19378>`_,
+  by Gaëtan Gilbert).
diff --git a/dune b/dune
index 6d1e7c7d6407e..88502230d32d9 100644
--- a/dune
+++ b/dune
@@ -21,7 +21,7 @@
 
 (alias
  (name default)
- (deps coq-core.install coq-stdlib.install coqide-server.install coqide.install))
+ (deps coq-core.install coq-stdlib.install coqide-server.install))
 
 (install
  (section lib)