[dune] [doc] Remove the quick targets in favor of the shims.

These targets are redundant with the shims.

We also improve the documentation quite a bit.

1 files changed, 26 insertions, 40 deletions

diff --git a/Makefile.dune b/Makefile.dune
index efdea2ab85..9e1747a4c3 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -2,48 +2,57 @@
 # Dune Makefile for Coq
 
 .PHONY: help states world watch check                 # Main developer targets
-.PHONY: coq coqide coqide-server                      # Package targets
-.PHONY: quickbyte quickopt quickide                   # Partial / quick developer targets
 .PHONY: refman-html refman-pdf stdlib-html apidoc     # Documentation targets
-.PHONY: test-suite release install                    # Accessory targets
+.PHONY: test-suite
 .PHONY: fmt ocheck ireport clean                      # Maintenance targets
-.PHONY: voboot                                        # Added just not to break old scripts
+.PHONY: voboot release install                        # Added just not to break old scripts
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
 
 help:
-	@echo "Welcome to Coq's Dune-based build system. Common targets are:"
+	@echo "Welcome to Coq's Dune-based build system. Common developer targets are:"
 	@echo ""
 	@echo "  - states: build a minimal functional coqtop"
 	@echo "  - world:  build all public binaries and libraries"
 	@echo "  - watch:  build all public binaries and libraries [continuous build]"
 	@echo "  - check:  build all ML files as fast as possible"
+	@echo "  - test-suite: run Coq's test suite"
 	@echo ""
-	@echo " Targets to build Coq in developer mode:"
+	@echo "  Note: these targets produce a developer build,"
+	@echo "        not suitable for distribution to end-users"
 	@echo ""
-	@echo "  - coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]"
-	@echo "  - coqide-server: build package coqide-server [XML protocol language server]"
-	@echo "  - coqide: build package CoqIDE [gtk application]"
+	@echo " Documentation targets:"
 	@echo ""
-	@echo "  - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler"
-	@echo "  - quickopt:  build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler"
-	@echo "  - quickide:  build main IDE files [client + server + prelude] using the optimizing compiler"
-	@echo ""
-	@echo "  - test-suite:  run Coq's test suite"
 	@echo "  - refman-html: build Coq's reference manual [HTML version]"
 	@echo "  - refman-pdf:  build Coq's reference manual [PDF version]"
 	@echo "  - stdlib-html: build Coq's Stdlib documentation [HTML version]"
 	@echo "  - apidoc:      build ML API documentation"
 	@echo ""
+	@echo " Miscellaneous targets:"
+	@echo ""
 	@echo "  - fmt:     run ocamlformat on the codebase"
 	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
 	@echo "  - ireport: build with optimized flambda settings and emit an inline report"
 	@echo "  - clean:   remove build directory and autogenerated files"
 	@echo "  - help:    show this message"
 	@echo ""
-	@echo " To build Coq in release mode, use 'dune build -p package'."
-	@echo " To install Coq in release mode, use 'dune install -p package'."
+	@echo " To run an app \\in {coqc,coqtop,coqbyte,coqide}:"
+	@echo ""
+	@echo "  - use 'dune exec -- dev/shim/app-prelude args'"
+	@echo ""
+	@echo " Provided opam/dune packages are:"
+	@echo ""
+	@echo "  - coq: base Coq package, toplevel compilers, tools, stdlib, no GTK"
+	@echo "  - coqide-server: XML protocol language server"
+	@echo "  - coqide: CoqIDE gtk application"
+	@echo ""
+	@echo " To build a package, you can use:"
+	@echo ""
+	@echo "  - 'dune build package.install' : build package in developer mode"
+	@echo "  - 'dune build -p package' : build package in release mode"
+	@echo ""
+	@echo " Packages _must_ be installed using release mode, use: 'dune install -p package'"
 	@echo " See Dune documentation for more information."
 
 voboot:
@@ -57,36 +66,12 @@ NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install
 world:
 	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS)
 
-coq:
-	dune build $(DUNEOPT) coq.install
-
-coqide:
-	dune build $(DUNEOPT) coqide.install
-
-coqide-server:
-	dune build $(DUNEOPT) coqide-server.install
-
 watch:
 	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w
 
 check:
 	dune build $(DUNEOPT) @check
 
-COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc
-PLUGIN_FILES=$(wildcard plugins/*/*.mlpack)
-PRINTER_FILES=dev/top_printers.cma
-QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc
-QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe
-
-quickbyte:
-	dune build $(DUNEOPT) $(QUICKBYTE_TARGETS)
-
-quickopt:
-	dune build $(DUNEOPT) $(QUICKOPT_TARGETS)
-
-quickide:
-	dune build $(DUNEOPT) dev/shim/coqide-prelude
-
 test-suite:
 	dune runtest --no-buffer $(DUNEOPT)
 
@@ -103,6 +88,7 @@ apidoc:
 	dune build $(DUNEOPT) @doc
 
 release:
+	@echo "release target is deprecated, use dune directly"
 	dune build $(DUNEOPT) -p coq
 
 # We define this target as to override Make's built-in one