[dune] [doc] Tweaks

Close #12167

1 files changed, 28 insertions, 7 deletions

diff --git a/Makefile.dune b/Makefile.dune
index b002c7709d..c2899dcaba 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,7 +1,7 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: help states world watch check                 # Main developer targets
+.PHONY: help help-install states world watch check    # Main developer targets
 .PHONY: refman-html refman-pdf stdlib-html apidoc     # Documentation targets
 .PHONY: test-suite
 .PHONY: fmt ocheck ireport clean                      # Maintenance targets
@@ -11,6 +11,7 @@
 # DUNEOPT=--display=short
 
 help:
+	@echo ""
 	@echo "Welcome to Coq's Dune-based build system. Common developer targets are:"
 	@echo ""
 	@echo "  - states: build a minimal functional coqtop"
@@ -19,8 +20,15 @@ help:
 	@echo "  - check:  build all ML files as fast as possible"
 	@echo "  - test-suite: run Coq's test suite"
 	@echo ""
-	@echo "  Note: these targets produce a developer build,"
-	@echo "        not suitable for distribution to end-users"
+	@echo "  Note: running ./configure is not recommended,"
+	@echo "        see dev/doc/build-system.dune.md for more info"
+	@echo "  Note: these targets produce a developer build, not suitable"
+	@echo "        for distribution to end-users or install"
+	@echo ""
+	@echo " To run an \$$app \\in {coqc,coqtop,coqbyte,coqide}:"
+	@echo ""
+	@echo "  - use 'dune exec -- dev/shim/\$$app-prelude args'"
+	@echo "    Example: 'dune exec -- dev/shim/coqc-prelude file.v'"
 	@echo ""
 	@echo " Documentation targets:"
 	@echo ""
@@ -37,9 +45,14 @@ help:
 	@echo "  - clean:   remove build directory and autogenerated files"
 	@echo "  - help:    show this message"
 	@echo ""
-	@echo " To run an app \\in {coqc,coqtop,coqbyte,coqide}:"
+	@echo " Type 'make help-install' for installation instructions"
+
+help-install:
+	@echo ""
+	@echo "The Dune-based Coq build is split in packages; see Dune and dev/doc"
+	@echo "documentation for more details. A quick install of Coq alone can done with"
 	@echo ""
-	@echo "  - use 'dune exec -- dev/shim/app-prelude args'"
+	@echo " ./configure -prefix <install_prefix> && dune build -p coq && dune install -p coq"
 	@echo ""
 	@echo " Provided opam/dune packages are:"
 	@echo ""
@@ -52,8 +65,16 @@ help:
 	@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."
+	@echo " Packages _must_ be installed using release mode, to install a package use: "
+	@echo ""
+	@echo "  - 'dune install -p package'"
+	@echo ""
+	@echo " Example: "
+	@echo ""
+	@echo "  - 'dune build -p coq,coqide-server,coqide && dune install -p coq coqide-server coqide'"
+	@echo ""
+	@echo " Note that building a package in release mode ignores other packages present in"
+	@echo " the worktree. See Dune documentation for more information."
 
 voboot:
 	@echo "This target is empty and not needed anymore"