Merge PR #11539: [dune] [stdlib] Build the standard library natively with Dune.

Reviewed-by: Zimmi48

28 files changed, 147 insertions, 410 deletions

diff --git a/.gitignore b/.gitignore
index b665b2f86d..adbf9dd189 100644
--- a/.gitignore
+++ b/.gitignore
@@ -184,11 +184,6 @@ plugins/ssr/ssrvernac.ml
 META.coq
 
 # Files automatically generated by Dune.
-plugins/*/dune
-theories/*/dune
-theories/*/*/dune
-theories/*/*/*/dune
-/user-contrib/Ltac2/dune
 *.install
 !Makefile.install
 
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index acbec54695..f1dc793ee7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,7 +18,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-03-27-V12"
+  CACHEKEY: "bionic_coq-V2020-03-11-V28"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/Makefile.dune b/Makefile.dune
index b77e78db69..9e1747a4c3 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,122 +1,109 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: help voboot states world watch check          # Main developer targets
-.PHONY: coq coqide coqide-server                      # Package targets
-.PHONY: quickbyte quickopt quickide                   # Partial / quick developer targets
+.PHONY: help states world watch check                 # Main developer targets
 .PHONY: refman-html refman-pdf stdlib-html apidoc     # Documentation targets
-.PHONY: test-suite release                            # Accessory targets
+.PHONY: test-suite
 .PHONY: fmt ocheck ireport clean                      # Maintenance targets
+.PHONY: voboot release install                        # 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 developer 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 "  - test-suite: run Coq's test suite"
 	@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 "  Note: these targets produce a developer build,"
+	@echo "        not suitable for distribution to end-users"
 	@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 " Documentation targets:"
 	@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 "  - release:     build Coq in release mode"
+	@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 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."
 
-# 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
-	dune build $(DUNEOPT) coq.install
-
-coqide: voboot
-	dune build $(DUNEOPT) coqide.install
-
-coqide-server: voboot
-	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
-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: voboot
-	dune build $(DUNEOPT) $(QUICKBYTE_TARGETS)
-
-quickopt: voboot
-	dune build $(DUNEOPT) $(QUICKOPT_TARGETS)
-
-quickide: states
-	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:
+	@echo "release target is deprecated, use dune directly"
 	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:
diff --git a/coq.opam b/coq.opam
index 39191c21d9..e46f9def60 100644
--- a/coq.opam
+++ b/coq.opam
@@ -22,13 +22,12 @@ version: "dev"
 
 depends: [
   "ocaml"     { >= "4.05.0" }
-  "dune"      { >= "2.0.0"  }
+  "dune"      { >= "2.5.0"  }
   "ocamlfind" { build }
   "num"
 ]
 
 build: [
   [ "./configure" "-prefix" prefix ]
-  [ "make" "-f" "Makefile.dune" "voboot" ]
   [ "dune" "build" "-p" name "-j" jobs ]
 ]
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 0c8733c75a..58677b8496 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-27-V12"
+# CACHEKEY: "bionic_coq-V2020-03-11-V28"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.10.2"
 
@@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.10.0" \
-    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0"
+    BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.13.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 0506216541..8b0bf216e3 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
 the make-based system.
 
-If you want to build the standard libraries and plugins you should
-call `make -f Makefile.dune voboot`. It is usually enough to do that
-once per-session.
-
 More helper targets are available in `Makefile.dune`, `make -f
 Makefile.dune` will display some help.
 
@@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and
 `coqide` in a fast build. In order to use them, do:
 
 ```
-$ make -f Makefile.dune voboot                # Only once per session
 $ dune exec -- dev/shim/coqtop-prelude
 ```
 
@@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors:
 
 ## Dropping from coqtop:
 
-After doing `make -f Makefile.dune voboot`, the following commands should work:
+The following commands should work:
 ```
 dune exec -- dev/shim/coqbyte-prelude
 > Drop.
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index b8a696ef21..fb84155392 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz";
-  sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w";
+  url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz";
+  sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p";
 })
diff --git a/dune b/dune
index d59346ed68..cf7221ce62 100644
--- a/dune
+++ b/dune
@@ -18,29 +18,10 @@
 ;
 ; (_ (flags :standard -rectypes)))
 
-; Rules for coq_dune
-(rule
- (targets .vfiles.d)
- (deps
-  (source_tree theories)
-  (source_tree plugins)
-  (source_tree user-contrib))
- (action
-  (with-stdout-to .vfiles.d
-   (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \
-          `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \
-          `find theories user-contrib -type f -name *.v`"))))
-
-(alias
- (name vodeps)
- (deps tools/coq_dune.exe .vfiles.d))
-  ; (action (run coq_dune .vfiles.d))))
-
 (install
  (section lib)
  (package coq)
- (files
-   revision))
+ (files revision))
 
 (rule
  (targets revision)
diff --git a/dune-project b/dune-project
index fa05f5fb41..873d03e8dd 100644
--- a/dune-project
+++ b/dune-project
@@ -1,11 +1,10 @@
-(lang dune 2.0)
+(lang dune 2.5)
 (name coq)
-(using coq 0.1)
+(using coq 0.2)
 
 (formatting
  (enabled_for ocaml))
 
-; We cannot set this to true until as long as the build is not
-; properly bootstrapped [that is, we remove the voboot target]
+; TODO
 ;
 ; (generate_opam_files true)
diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/dune
index 6a024358c3..d2f5b65980 100644
--- a/plugins/btauto/plugin_base.dune
+++ b/plugins/btauto/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.btauto)
  (synopsis "Coq's btauto plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_btauto))
diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/dune
index 2a92996d2a..f7fa3adb56 100644
--- a/plugins/cc/plugin_base.dune
+++ b/plugins/cc/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.cc)
  (synopsis "Coq's congruence closure plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_congruence))
diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/dune
index ba9cd595ce..1931339471 100644
--- a/plugins/derive/plugin_base.dune
+++ b/plugins/derive/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.derive)
  (synopsis "Coq's derive plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_derive))
diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/dune
index 037b0d5053..0c01dcd488 100644
--- a/plugins/extraction/plugin_base.dune
+++ b/plugins/extraction/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.extraction)
  (synopsis "Coq's extraction plugin")
  (libraries num coq.plugins.ltac))
+
+(coq.pp (modules g_extraction))
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/dune
index d88daa23fc..1b05452d8f 100644
--- a/plugins/firstorder/plugin_base.dune
+++ b/plugins/firstorder/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.firstorder)
  (synopsis "Coq's first order logic solver plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ground))
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/dune
index 6ccf15df29..e594ffbd02 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.funind)
  (synopsis "Coq's functional induction plugin")
  (libraries coq.plugins.extraction))
+
+(coq.pp (modules g_indfun))
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune
index 5611f5ba16..6558ecbfe8 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/dune
@@ -11,3 +11,5 @@
  (synopsis "Coq's tauto tactic")
  (modules tauto)
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules extratactics g_tactic  g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/dune
index 4153d06161..33ad3a0138 100644
--- a/plugins/micromega/plugin_base.dune
+++ b/plugins/micromega/dune
@@ -20,3 +20,5 @@
  (modules g_zify zify)
  (synopsis "Coq's zify plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_micromega g_zify))
diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/dune
index 9da5b39972..b921c9c408 100644
--- a/plugins/nsatz/plugin_base.dune
+++ b/plugins/nsatz/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.nsatz)
  (synopsis "Coq's nsatz solver plugin")
  (libraries num coq.plugins.ltac))
+
+(coq.pp (modules g_nsatz))
diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/dune
index f512501c78..0db71ed6fb 100644
--- a/plugins/omega/plugin_base.dune
+++ b/plugins/omega/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.omega)
  (synopsis "Coq's omega plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_omega))
diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/dune
index 233845ae0f..43efa0eca5 100644
--- a/plugins/rtauto/plugin_base.dune
+++ b/plugins/rtauto/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.rtauto)
  (synopsis "Coq's rtauto plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_rtauto))
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/dune
index d83857edad..60522cd3f5 100644
--- a/plugins/setoid_ring/plugin_base.dune
+++ b/plugins/setoid_ring/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.setoid_ring)
  (synopsis "Coq's setoid ring plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_newring))
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/dune
index a13524bb52..a117d09a16 100644
--- a/plugins/ssr/plugin_base.dune
+++ b/plugins/ssr/dune
@@ -5,3 +5,5 @@
  (modules_without_implementation ssrast)
  (flags :standard -open Gramlib)
  (libraries coq.plugins.ssrmatching))
+
+(coq.pp (modules ssrvernac ssrparser))
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/dune
index 06f67c3774..629d723816 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.ssrmatching)
  (synopsis "Coq ssrmatching plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ssrmatching))
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/dune
index 512752135d..b395695c8a 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/dune
@@ -32,3 +32,5 @@
  (synopsis "Coq syntax plugin: float")
  (modules float_syntax)
  (libraries coq.vernac))
+
+(coq.pp (modules g_numeral g_string))
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000000..b9af76d699
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,38 @@
+(coq.theory
+ (name Coq)
+ (package coq)
+ (synopsis "Coq's Standard Library")
+ (flags -q)
+ ; (mode native)
+ (boot)
+ ; (per_file
+ ;  (Init/*.v -> -boot))
+ (libraries
+   coq.plugins.ltac
+   coq.plugins.tauto
+
+   coq.plugins.cc
+   coq.plugins.firstorder
+
+   coq.plugins.numeral_notation
+   coq.plugins.string_notation
+   coq.plugins.int63_syntax
+   coq.plugins.r_syntax
+   coq.plugins.float_syntax
+
+   coq.plugins.btauto
+   coq.plugins.rtauto
+
+   coq.plugins.setoid_ring
+   coq.plugins.nsatz
+   coq.plugins.omega
+
+   coq.plugins.zify
+   coq.plugins.micromega
+
+   coq.plugins.funind
+
+   coq.plugins.ssreflect
+   coq.plugins.derive))
+
+(include_subdirs qualified)
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
deleted file mode 100644
index 472e6b4948..0000000000
--- a/tools/coq_dune.ml
+++ /dev/null
@@ -1,301 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license:
- *
- * Permission is hereby granted, free of charge, to any person obtaining a copy
- * of this software and associated documentation files (the "Software"), to deal
- * in the Software without restriction, including without limitation the rights
- * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
- * copies of the Software, and to permit persons to whom the Software is
- * furnished to do so, subject to the following conditions:
- *
- * The above copyright notice and this permission notice shall be included in all
- * copies or substantial portions of the Software.
- *
- * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
- * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
- * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
- * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
- * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
- * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
- * SOFTWARE.
- *)
-
-(* coq_dune: generate dune build rules for .vo files                    *)
-(*                                                                      *)
-(* At some point this file will become a Dune plugin, so it is very     *)
-(* important that this file can be bootstrapped with:                   *)
-(*                                                                      *)
-(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune     *)
-
-open Format
-
-(* Keeping this file self-contained as it is a "bootstrap" utility *)
-(* Is OCaml missing these basic functions in the stdlib?           *)
-module Aux = struct
-
-  let option_iter f o = match o with
-    | Some x -> f x
-    | None -> ()
-
-  let option_cata d f o = match o with
-    | Some x -> f x
-    | None -> d
-
-  let list_compare f = let rec lc x y = match x, y with
-      | [], [] -> 0
-      | [], _ -> -1
-      | _, [] -> 1
-      | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r
-    in lc
-
-  let rec pp_list pp sep fmt l = match l with
-    | []  -> ()
-    | [l] -> fprintf fmt "%a" pp l
-    | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs
-
-  let rec pmap f l = match l with
-    | []  -> []
-    | x :: xs ->
-      begin match f x with
-        | None -> pmap f xs
-        | Some r -> r :: pmap f xs
-      end
-
-  let sep fmt () = fprintf fmt "@;"
-
-  (* Creation of paths, aware of the platform separator. *)
-  let bpath l = String.concat Filename.dir_sep l
-
-  module DirOrd = struct
-    type t = string list
-    let compare = list_compare String.compare
-  end
-
-  module DirMap = Map.Make(DirOrd)
-
-  (* Functions available in newer OCaml versions *)
-  (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *)
-  module Legacy = struct
-
-
-    (* Fix once we move to OCaml >= 4.06.0 *)
-    let list_init len f =
-      let rec init_aux i n f =
-        if i >= n then []
-        else let r = f i in r :: init_aux (i+1) n f
-      in init_aux 0 len f
-
-    (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *)
-    let dirmap_update key f map =
-      match begin
-        try f (Some (DirMap.find key map))
-        with Not_found -> f None
-      end with
-      | None   -> DirMap.remove key map
-      | Some x -> DirMap.add key x map
-
-  end
-
-  let add_map_list key elem map =
-    (* Move to Dirmap.update once we require OCaml >= 4.06.0 *)
-    Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map
-
-  let replace_ext ~file ~newext =
-    Filename.(remove_extension file) ^ newext
-
-end
-
-open Aux
-
-(* Once this is a Dune plugin the flags will be taken from the env *)
-module Options = struct
-
-  type flag = {
-    enabled : bool;
-    cmd : string;
-  }
-
-  let all_opts =
-  [ { enabled = false; cmd = "-debug"; }
-  ; { enabled = false; cmd = "-native_compiler"; }
-  ; { enabled = true; cmd = "-w +default"; }
-  ]
-
-  let build_coq_flags () =
-    let popt o = if o.enabled then Some o.cmd else None in
-    String.concat " " @@ pmap popt all_opts
-end
-
-type vodep = {
-  target: string;
-  deps : string list;
-}
-
-type ldep = | VO of vodep | MLG of string
-type ddir = ldep list DirMap.t
-
-(* Filter `.vio` etc... *)
-let filter_no_vo =
-  List.filter (fun f -> Filename.check_suffix f ".vo")
-
-(* We could have coqdep to output dune files directly *)
-
-let gen_sub n =
-  (* Move to List.init once we can depend on OCaml >= 4.06.0 *)
-  bpath @@ Legacy.list_init n (fun _ -> "..")
-
-let pp_rule fmt targets deps action =
-  (* Special printing of the first rule *)
-  let ppl = pp_list pp_print_string sep in
-  let pp_deps fmt l = match l with
-    | [] ->
-      ()
-    | x :: xs ->
-      fprintf fmt "(:pp-file %s)%a" x sep ();
-      pp_list pp_print_string sep fmt xs
-  in
-  fprintf fmt
-    "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n"
-    ppl targets pp_deps deps pp_print_string action
-
-let gen_coqc_targets vo =
-  [ vo.target
-  ; replace_ext ~file:vo.target ~newext:".glob"
-  ; replace_ext ~file:vo.target ~newext:".vos"
-  ; "." ^ replace_ext ~file:vo.target ~newext:".aux"]
-
-(* Generate the dune rule: *)
-let pp_vo_dep dir fmt vo =
-  let depth = List.length dir in
-  let sdir = gen_sub depth in
-  (* All files except those in Init implicitly depend on the Prelude, we account for it here. *)
-  let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in
-  (* Coq flags *)
-  let cflag = Options.build_coq_flags () in
-  (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *)
-  let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in
-  (* The source file is also corrected as we will call coqtop from the top dir *)
-  let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in
-  (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *)
-  let libflag = "-coqlib %{project_root}" in
-  (* The final build rule *)
-  let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in
-  let all_targets = gen_coqc_targets vo in
-  pp_rule fmt all_targets deps action
-
-let pp_mlg_dep _dir fmt ml =
-  fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml)
-
-let pp_dep dir fmt oo = match oo with
-  | VO vo -> pp_vo_dep dir fmt vo
-  | MLG f -> pp_mlg_dep dir fmt f
-
-let out_install fmt dir ff =
-  let itarget = String.concat "/" dir in
-  let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in
-  let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in
-  fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n"
-    (pp_list pp_ispec sep) ff
-
-(* For each directory, we must record two things, the build rules and
-   the install specification. *)
-let record_dune d ff =
-  let sd = bpath d in
-  if Sys.file_exists sd && Sys.is_directory sd then
-    let out = open_out (bpath [sd;"dune"]) in
-    let fmt = formatter_of_out_channel out in
-    if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then
-      fprintf fmt "(include plugin_base.dune)@\n";
-    out_install fmt d ff;
-    List.iter (pp_dep d fmt) ff;
-    fprintf fmt "%!";
-    close_out out
-  else
-    eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd
-
-(* File Scanning *)
-let scan_mlg ~root m d =
-  let dir = [root; d] in
-  let m = DirMap.add dir [] m in
-  let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg"))
-                   Array.(to_list @@ readdir (bpath dir))) in
-  List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg
-
-let scan_dir ~root m =
-  let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
-  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in
-  List.fold_left (scan_mlg ~root) m dirs
-
-let scan_plugins m = scan_dir ~root:"plugins" m
-let scan_usercontrib m = scan_dir ~root:"user-contrib" m
-
-(* This will be removed when we drop support for Make *)
-let fix_cmo_cma file =
-  if String.equal Filename.(extension file) ".cmo"
-  then replace_ext ~file ~newext:".cma"
-  else file
-
-(* Process .vfiles.d and generate a skeleton for the dune file *)
-let parse_coqdep_line l =
-  match Str.(split (regexp ":") l) with
-  | [targets;deps] ->
-    let targets = Str.(split (regexp "[ \t]+") targets) in
-    let deps    = Str.(split (regexp "[ \t]+") deps)    in
-    let targets = filter_no_vo targets in
-    begin match targets with
-    | [target] ->
-      let dir, target = Filename.(dirname target, basename target) in
-      (* coqdep outputs with the '/' directory separator regardless of
-         the platform. Anyways, I hope we can link to coqdep instead
-         of having to parse its output soon, that should solve this
-         kind of issues *)
-      let deps = List.map fix_cmo_cma deps in
-      Some (String.split_on_char '/' dir, VO { target; deps; })
-    (* Otherwise a vio file, we ignore *)
-    | _ -> None
-    end
-  (* Strange rule, we ignore *)
-  | _ -> None
-
-let rec read_vfiles ic map =
-  try
-    let rule = parse_coqdep_line (input_line ic) in
-    (* Add vo_entry to its corresponding map entry *)
-    let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in
-    read_vfiles ic map
-  with End_of_file -> map
-
-let out_map map =
-  DirMap.iter record_dune map
-
-let exec_ifile f =
-  match Array.length Sys.argv with
-  | 1 -> f stdin
-  | 2 ->
-    let in_file = Sys.argv.(1) in
-    begin try
-      let ic = open_in in_file in
-      (try f ic
-       with exn ->
-         eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn);
-         close_in ic)
-      with _ ->
-        eprintf "Error: cannot open input file %s@\n%!" in_file
-    end
-  | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1
-
-let _ =
-  exec_ifile (fun ic ->
-      let map = scan_plugins DirMap.empty in
-      let map = scan_usercontrib map in
-      let map = read_vfiles ic map in
-      out_map map)
diff --git a/tools/dune b/tools/dune
index c0e4e20f72..d591bb0c37 100644
--- a/tools/dune
+++ b/tools/dune
@@ -49,8 +49,8 @@
 (ocamllex coqwc)
 
 (executables
- (names coq_tex coq_dune)
- (public_names coq-tex coq_dune)
+ (names coq_tex)
+ (public_names coq-tex)
  (package coq)
- (modules coq_tex coq_dune)
+ (modules coq_tex)
  (libraries str))
diff --git a/user-contrib/Ltac2/dune b/user-contrib/Ltac2/dune
new file mode 100644
index 0000000000..90869a46a0
--- /dev/null
+++ b/user-contrib/Ltac2/dune
@@ -0,0 +1,14 @@
+(coq.theory
+ (name Ltac2)
+ (package coq)
+ (synopsis "Ltac2 tactic language")
+ (libraries coq.plugins.ltac2))
+
+(library
+ (name ltac2_plugin)
+ (public_name coq.plugins.ltac2)
+ (synopsis "Ltac2 plugin")
+ (modules_without_implementation tac2expr tac2qexpr tac2types)
+ (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ltac2))