[dune] [stdlib] Build the standard library natively with Dune.

This completes a pure Dune bootstrap of Coq.

There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.

TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.

Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?

1 files changed, 37 insertions, 36 deletions

diff --git a/Makefile.dune b/Makefile.dune
index b77e78db69..efdea2ab85 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,27 +1,27 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: help voboot states world watch check          # Main developer targets
+.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                            # Accessory targets
+.PHONY: test-suite release install                    # Accessory targets
 .PHONY: fmt ocheck ireport clean                      # Maintenance targets
+.PHONY: voboot                                        # Added just not to break old scripts
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
 
-BOOT_DIR=_build_boot
-BOOT_CONTEXT=$(BOOT_DIR)/default
-
 help:
-	@echo "Welcome to Coq's Dune-based build system. Targets are:"
+	@echo "Welcome to Coq's Dune-based build system. Common targets are:"
 	@echo ""
 	@echo "  - states: build a minimal functional coqtop"
-	@echo "  - world:  build all binaries and libraries"
-	@echo "  - watch:  build all binaries and libraries [continuous build]"
+	@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 ""
+	@echo " Targets to build Coq in developer mode:"
+	@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]"
@@ -35,43 +35,41 @@ help:
 	@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 "  - release:     build Coq in release mode"
 	@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 " See Dune documentation for more information."
 
-# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work.
-plugins/ltac/dune:
-	@echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune
-
-voboot: plugins/ltac/dune
-	dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps
-	dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d
+voboot:
+	@echo "This target is empty and not needed anymore"
 
-states: voboot
+states:
 	dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude
 
 NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install
 
-world: voboot
+world:
 	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS)
 
-coq: voboot
+coq:
 	dune build $(DUNEOPT) coq.install
 
-coqide: voboot
+coqide:
 	dune build $(DUNEOPT) coqide.install
 
-coqide-server: voboot
+coqide-server:
 	dune build $(DUNEOPT) coqide-server.install
 
-watch: voboot
+watch:
 	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w
 
-check: voboot
+check:
 	dune build $(DUNEOPT) @check
 
 COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc
@@ -80,43 +78,46 @@ 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: voboot
+quickbyte:
 	dune build $(DUNEOPT) $(QUICKBYTE_TARGETS)
 
-quickopt: voboot
+quickopt:
 	dune build $(DUNEOPT) $(QUICKOPT_TARGETS)
 
-quickide: states
+quickide:
 	dune build $(DUNEOPT) dev/shim/coqide-prelude
 
-test-suite: voboot
+test-suite:
 	dune runtest --no-buffer $(DUNEOPT)
 
-refman-html: voboot
+refman-html:
 	dune build @refman-html
 
-refman-pdf: voboot
+refman-pdf:
 	dune build @refman-pdf
 
-stdlib-html: voboot
+stdlib-html:
 	dune build @stdlib-html
 
-apidoc: voboot
+apidoc:
 	dune build $(DUNEOPT) @doc
 
-release: voboot
+release:
 	dune build $(DUNEOPT) -p coq
 
-fmt: voboot
+# We define this target as to override Make's built-in one
+install:
+	@echo "To install Coq using dune, use 'dune install -p PACKAGE' where"
+	@echo "PACKAGE is any of the packages defined by opam files in the root dira"
+
+fmt:
 	dune build @fmt --auto-promote
 
-ocheck: voboot
+ocheck:
 	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
 
 ireport:
 	dune clean
-	dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps
-	dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d
 	dune build $(DUNEOPT) @install --profile=ireport
 
 clean: