Merge PR #6857: [build] Preliminary support for building with `dune`.

61 files changed, 1004 insertions, 20 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 5be434c8b7..65c971ce76 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -256,6 +256,15 @@
 
 /theories/Vectors/        @herbelin
 
+########## Dune  ##########
+
+/Makefile.dune         @ejgallego
+/tools/coq_dune*       @ejgallego
+/dune*                 @ejgallego
+/coq.opam              @ejgallego
+/ide/coqide.opam       @ejgallego
+# Secondary maintainer @Zimmi48
+
 ########## Tools ##########
 
 /tools/coqdoc/         @silene
diff --git a/.gitignore b/.gitignore
index 0e41d6a778..8fc3c802ad 100644
--- a/.gitignore
+++ b/.gitignore
@@ -183,3 +183,10 @@ plugins/ssr/ssrvernac.ml
 # ocaml dev files
 .merlin
 META.coq
+
+# Files automatically generated by Dune.
+plugins/*/dune
+theories/*/dune
+theories/*/*/dune
+theories/*/*/*/dune
+*.install
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3e08aa58bb..7f770feded 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -88,6 +88,20 @@ after_script:
 
     - set +e
 
+.dune-template: &dune-template
+  stage: build
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build/
+    expire_in: 1 week
+  script:
+    - set -e
+    - echo 'start:coq.dune'
+    - make -f Makefile.dune world
+    - echo 'end:coq.dune'
+    - set +e
+
 # every non build job must set dependencies otherwise all build
 # artifacts are used together and we may get some random Coq. To that
 # purpose, we add a spurious dependency `not-a-real-job` that must be
@@ -203,6 +217,11 @@ build:edge+flambda:
     COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts "
     COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"
 
+build:egde:dune:
+  <<: *dune-template
+  variables:
+    OPAM_SWITCH: edge
+
 windows64:
   <<: *windows-template
   variables:
diff --git a/Makefile.build b/Makefile.build
index c100eda400..0faa18b059 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -317,13 +317,11 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
 	cd $(dir $(LIBCOQRUN)) && \
 	$(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(notdir $(BYTERUN))
 
-kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
-	sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
-               -e '/^}/q' $< $(TOTARGET)
+kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h kernel/byterun/make_jumptbl.sh
+	kernel/byterun/make_jumptbl.sh $< $@
 
-kernel/copcodes.ml: kernel/byterun/coq_instruct.h
-	tr -d "\r" < $< | sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' | \
-	awk -f kernel/make-opcodes $(TOTARGET)
+kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/make-opcodes
+	kernel/make_opcodes.sh $< $@
 
 %.o: %.c
 	$(SHOW)'OCAMLC    $<'
diff --git a/Makefile.dune b/Makefile.dune
new file mode 100644
index 0000000000..6056151c0d
--- /dev/null
+++ b/Makefile.dune
@@ -0,0 +1,39 @@
+# -*- mode: makefile -*-
+# Dune Makefile for Coq
+
+.PHONY: help voboot states world apidoc
+
+# use DUNEOPT=--display=short for a more verbose build
+# DUNEOPT=--display=short
+
+BUILD_CONTEXT=_build/default
+
+help:
+	@echo "Welcome to Coq's Dune-based build system. Targets are:"
+	@echo "  - states: build a minimal functional coqtop"
+	@echo "  - world:  build all binaries and libraries"
+	@echo "  - clean:  remove build directory and autogenerated files"
+	@echo "  - help:   show this message"
+
+voboot:
+	dune build $(DUNEOPT) @vodeps
+	dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d
+
+states: voboot
+	dune build $(DUNEOPT) theories/Init/Prelude.vo
+
+world: voboot
+	dune build $(DUNEOPT) @install
+
+clean:
+	dune clean
+
+# Other common dev targets
+#
+# dune build coq.install
+# dune build ide/coqide.install
+
+# Packaging / OPAM targets:
+#
+# dune -p coq @install
+# dune -p coqide @install
diff --git a/checker/dune b/checker/dune
new file mode 100644
index 0000000000..d918f853dd
--- /dev/null
+++ b/checker/dune
@@ -0,0 +1,26 @@
+(rule (copy %{project_root}/kernel/names.ml names.ml))
+(rule (copy %{project_root}/kernel/names.mli names.mli))
+(rule (copy %{project_root}/kernel/esubst.ml esubst.ml))
+(rule (copy %{project_root}/kernel/esubst.mli esubst.mli))
+
+(library
+ (name checker)
+ (public_name coq.checker)
+ (synopsis "Coq's Standalone Proof Checker")
+ (modules values analyze names esubst)
+ (wrapped false)
+ (libraries coq.lib))
+
+(executable
+ (name main)
+ (public_name coqchk)
+ (modules :standard \ votour values analyze names esubst)
+ (modules_without_implementation cic)
+ (libraries coq.checker))
+
+(executable
+ (name votour)
+ (public_name votour)
+ (modules votour)
+ (libraries coq.checker))
+
diff --git a/clib/dune b/clib/dune
new file mode 100644
index 0000000000..689a955ab7
--- /dev/null
+++ b/clib/dune
@@ -0,0 +1,8 @@
+(library
+ (name clib)
+ (synopsis "Coq's Utility Library [general purpose]")
+ (public_name coq.clib)
+ (wrapped false)
+ (modules_without_implementation cSig)
+ (libraries threads str unix dynlink))
+
diff --git a/config/dune b/config/dune
new file mode 100644
index 0000000000..30faf1233e
--- /dev/null
+++ b/config/dune
@@ -0,0 +1,13 @@
+(library
+ (name config)
+ (synopsis "Coq Configuration Variables")
+ (public_name coq.config)
+ (wrapped false))
+
+; Dune doesn't use configure's output, but it is still necessary for
+; some Coq files to work; will be fixed in the future.
+(rule
+ (targets coq_config.ml)
+ (mode fallback)
+ (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run)
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -local -warn-error yes -native-compiler yes))))
diff --git a/coq.opam b/coq.opam
new file mode 100644
index 0000000000..7f577dd8be
--- /dev/null
+++ b/coq.opam
@@ -0,0 +1,22 @@
+opam-version: "1.2"
+maintainer: "The Coq development team <coqdev@inria.fr>"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "https://github.com/coq/coq.git"
+license: "LGPL-2.1"
+
+available: [ ocaml-version >= "4.02.3" ]
+
+depends: [
+  "dune"      { build }
+  "ocamlfind" { build }
+  "num"
+  "camlp5"
+]
+
+build: [
+  [ "dune" "build" "@vodeps" ]
+  [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ]
+  [ "dune" "build" "-p" package "-j" jobs ]
+]
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index fd425ef4ff..1648167a27 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -181,7 +181,7 @@ let print_fun fmt (vars, body) =
   in
   let () = fprintf fmt "fun@ " in
   let () = List.iter iter vars in
-  (** FIXME: use Coq locations in the macros *)
+  (* FIXME: use Coq locations in the macros *)
   let () = fprintf fmt "loc ->@ @[%s@]" body.code in
   ()
 
diff --git a/coqpp/dune b/coqpp/dune
new file mode 100644
index 0000000000..24b9b9184b
--- /dev/null
+++ b/coqpp/dune
@@ -0,0 +1,8 @@
+(ocamllex coqpp_lex)
+(ocamlyacc coqpp_parse)
+
+(executable
+ (name coqpp_main)
+ (public_name coqpp)
+ (modules coqpp_ast coqpp_lex coqpp_parse coqpp_main)
+ (modules_without_implementation coqpp_ast))
diff --git a/dev/ci/README.md b/dev/ci/README.md
index b4ea6838bf..95892ebe0a 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -156,6 +156,9 @@ Currently available artifacts are:
   architecture and OCaml version used to build Coq:
   https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
 
+  Additionally, an experimental Dune build is provided:
+  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune
+
 - the Coq documentation, built in the `doc:*` jobs. When submitting
   a documentation PR, this can help reviewers checking the rendered result:
 
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index d22b9c8f7c..1a9a26843c 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -14,6 +14,6 @@ else
    COQLIB="$COQBIN/../"
 fi
 
-( cd "${CI_BUILD_DIR}/pidetop" && jbuilder build @install )
+( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install )
 
 echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index abba13428f..b0a2b04121 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -1,5 +1,3 @@
-
-
 HISTORY:
 -------
 
@@ -35,13 +33,41 @@ HISTORY:
   grammar.cma (and q_constr.cmo) directly, no need for a separate
   subcall to make nor awkward include-failed-and-retry.
 
-    
----------------------------------------------------------------------------
+* February - September 2018 (Emilio Jesús Gallego Arias)
+
+  Dune support added.
+
+  The build setup is mostly vanilla for the OCaml part, however the
+  `.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper
+  that will generate the necessary `dune` files.
+
+  As a developer, you should not have to deal with Dune configuration
+  files on a regular basis unless adding a new library or plugin.
 
+  The vanilla setup declares all the Coq libraries and binaries [we
+  must respect proper containment/module implementation rules as to
+  allow packing], and we build custom preprocessors (based on `camlp5`
+  and `coqpp`) that will process the `ml4`/`mlg` files.
+
+  This suffices to build `coqtop` and `coqide`, all that remains to
+  handle is `.vo` compilation.
+
+  To teach Dune about the `.vo`, we use a small utility `coq_dune`,
+  that will generate a `dune` file for each directory in `plugins` and
+  `theories`. The code is pretty straightforward and declares build
+  and install rules for each `.v` straight out of `coqdep`. Thus, our
+  build strategy looks like this:
+
+  1. Use `dune` to build `coqdep` and `coq_dune`.
+  2. Use `coq_dune` to generate `dune` files for each directory with `.v` files.
+  3. ?
+  4. Profit! [Seriously, at this point Dune has all the information to build Coq]
+
+---------------------------------------------------------------------------
 
-This file documents internals of the implementation of the build
-system. For what a Coq developer needs to know about the build system,
-see build-system.txt .
+This file documents internals of the implementation of the make-based
+build system. For what a Coq developer needs to know about the build
+system, see build-system.txt and build-system.dune.md .
 
 .ml4 files
 ----------
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
new file mode 100644
index 0000000000..0b3e414513
--- /dev/null
+++ b/dev/doc/build-system.dune.md
@@ -0,0 +1,92 @@
+This file documents what a Coq developer needs to know about the
+Dune-based build system. If you want to enhance the build system
+itself (or are curious about its implementation details), see
+build-system.dev.txt, and in particular its initial HISTORY section.
+
+Dune
+====
+
+Coq can now be built using
+[Dune](https://github.com/ocaml/dune). Contrary to other systems,
+Dune, doesn't use a global`makefile` but local build files named
+`dune` that are later composed to form a global build.
+
+As a developer, Dune should take care of all OCaml-related build tasks
+including library management, merlin files, and link order. You are
+are not supposed to modify the `dune` files unless you are adding a
+new binary, library, or plugin.
+
+The current Dune setup also doesn't require a call to `configure`. The
+auto-generated configuration files are properly included in the
+dependency graph so it will be automatically generated by Dune with
+reasonable developer defaults. You can still override the defaults by
+manually calling `./configure`, but note that some configure options
+such as install paths are not used by Dune.
+
+Dune uses a separate directory `_build` to store build artifacts; it
+will generate an `.install` file so artifacts in the build can be
+properly installed by package managers.
+
+## Targets
+
+The default dune target is `dune build` (or `dune build @install`),
+which will scan all sources in the Coq tree and then build the whole
+project, creating an "install" overlay in `_build/install/default`.
+
+You can build some other target by doing `dune build $TARGET`.
+
+In order to build a single package, you can do `dune build
+$PACKAGE.install`. Dune also provides targets for documentation and
+testing, see below.
+
+## Compositionality, developer and release modes.
+
+By default [in "developer mode"], Dune will compose all the packages
+present in the tree and perform a global build. That means that for
+example you could drop the `ltac2` folder under `plugins` and get a
+build using `ltac2`, that will use the current Coq version.
+
+This is very useful to develop plugins and Coq libraries as your
+plugin will correctly track dependencies and rebuild incrementally as
+needed.
+
+However, it is not always desirable to go this way. For example, the
+current Coq source tree contains two packages [Coq and CoqIDE], and in
+the OPAM CoqIDE package we don't want to build CoqIDE against the
+local copy of Coq. For this purpose, Dune supports the `-p` option, so
+`dune build -p coqide` will build CoqIDE against the system-installed
+version of Coq libs.
+
+## Stanzas
+
+`dune` files contain the so-called "stanzas", that may declare:
+
+- libraries,
+- executables,
+- documentation, arbitrary blobs.
+
+The concrete options for each stanza can be seen in the Dune manual,
+but usually the default setup will work well with the current Coq
+sources. Note that declaring a library or an executable won't make it
+installed by default, for that, you need to provide a "public name".
+
+## Workspaces and Profiles
+
+Dune provides support for tree workspaces so the developer can set
+global options --- such as flags --- on all packages, or build Coq
+with different OPAM switches simultaneously [for example to test
+compatibility]; for more information, please refer to the Dune manual.
+
+## Documentation and test targets
+
+The documentation and test suite targets for Coq are still not
+implemented in Dune.
+
+## Planned and Advanced features
+
+Dune supports or will support extra functionality that may result very
+useful to Coq, some examples are:
+
+- Cross-compilation.
+- Automatic Generation of OPAM files.
+- Multi-directory libraries.
diff --git a/dune b/dune
new file mode 100644
index 0000000000..2a77d62a16
--- /dev/null
+++ b/dune
@@ -0,0 +1,15 @@
+(rule
+ (targets .vfiles.d)
+ (deps
+  (source_tree theories)
+  (source_tree plugins))
+ (action (with-stdout-to .vfiles.d (system "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`"))))
+
+(alias
+ (name vodeps)
+ (deps tools/coq_dune.exe .vfiles.d))
+  ; (action (run coq_dune .vfiles.d))))
+
+; Add custom flags here. Default developer profile is `dev`
+(env
+ (dev (flags :standard -rectypes -w -9-27-50)))
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000000..b98bfa1013
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 1.0)
+
+(name coq-devel)
diff --git a/engine/dune b/engine/dune
new file mode 100644
index 0000000000..e2b7ab9c87
--- /dev/null
+++ b/engine/dune
@@ -0,0 +1,6 @@
+(library
+ (name engine)
+ (synopsis "Coq's Tactic Engine")
+ (public_name coq.engine)
+ (wrapped false)
+ (libraries library))
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 970bf67732..a9666e4f90 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -532,7 +532,7 @@ module Goal : sig
 
   (** Compatibility: avoid if possible *)
   val goal : t -> Evar.t
-  val print : t -> Goal.goal Evd.sigma
+  val print : t -> Evar.t Evd.sigma
 
 end
 
diff --git a/grammar/dune b/grammar/dune
new file mode 100644
index 0000000000..90847e7fb6
--- /dev/null
+++ b/grammar/dune
@@ -0,0 +1,41 @@
+(library
+ (name grammar)
+ (synopsis "Coq Camlp5 Grammar Extensions for Plugins")
+ (public_name coq.grammar)
+ (wrapped false)
+ (flags (:standard -w -58))
+ (libraries camlp5))
+
+; Custom camlp5! This is a net speedup, and a preparation for using
+; Dune's preprocessor abilities.
+(rule
+ (targets coqmlp5)
+ (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx -o coqmlp5)))
+
+(rule
+ (targets coqp5)
+ (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5)))
+
+(install
+ (section bin)
+ (files coqp5 coqmlp5))
+
+(rule
+ (targets q_util.ml)
+ (deps (:mlp-file q_util.mlp))
+ (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
+
+(rule
+ (targets argextend.ml)
+ (deps (:mlp-file argextend.mlp))
+ (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
+
+(rule
+ (targets tacextend.ml)
+ (deps (:mlp-file tacextend.mlp))
+ (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
+
+(rule
+ (targets vernacextend.ml)
+ (deps (:mlp-file vernacextend.mlp))
+ (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
diff --git a/ide/coqide.opam b/ide/coqide.opam
new file mode 100644
index 0000000000..1b46efdee2
--- /dev/null
+++ b/ide/coqide.opam
@@ -0,0 +1,19 @@
+opam-version: "1.2"
+maintainer: "The Coq development team <coqdev@inria.fr>"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "https://github.com/coq/coq.git"
+license: "LGPL-2.1"
+
+available: [ocaml-version >= "4.02.3"]
+
+depends: [
+  "dune"      { build }
+  "ocamlfind" { build }
+  "num"
+  "camlp5"
+  "coq"
+]
+
+build: [ [ "dune" "build" "-p" package "-j" jobs ] ]
diff --git a/ide/dune b/ide/dune
new file mode 100644
index 0000000000..bceb981ed0
--- /dev/null
+++ b/ide/dune
@@ -0,0 +1,21 @@
+(executable
+ (name idetop)
+ (public_name coqidetop.opt)
+ (package coqide)
+ (modules idetop)
+ (libraries coq.toplevel coqide.protocol)
+ (link_flags -linkall))
+
+(rule
+ (targets coqide_main.ml)
+ (deps (:ml4-file coqide_main.ml4))
+ (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets})))
+
+(executable
+ (name coqide_main)
+ (public_name coqide)
+ (package coqide)
+ (modules (:standard \ idetop))
+ (libraries threads str lablgtk2.sourceview2 coq.lib coqide.protocol))
+
+(ocamllex utf8_convert config_lexer coq_lex)
diff --git a/ide/dune-project b/ide/dune-project
new file mode 100644
index 0000000000..948dc59000
--- /dev/null
+++ b/ide/dune-project
@@ -0,0 +1,3 @@
+(lang dune 1.0)
+
+(name coqide-devel)
diff --git a/ide/protocol/dune b/ide/protocol/dune
new file mode 100644
index 0000000000..9ce4559940
--- /dev/null
+++ b/ide/protocol/dune
@@ -0,0 +1,7 @@
+(library
+ (name protocol)
+ (public_name coqide.protocol)
+ (wrapped false)
+ (libraries coq.lib))
+
+(ocamllex xml_lexer)
diff --git a/interp/dune b/interp/dune
new file mode 100644
index 0000000000..e9ef7ba99a
--- /dev/null
+++ b/interp/dune
@@ -0,0 +1,6 @@
+(library
+ (name interp)
+ (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
+ (public_name coq.interp)
+ (wrapped false)
+ (libraries pretyping))
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
new file mode 100644
index 0000000000..3a714a8a59
--- /dev/null
+++ b/kernel/byterun/dune
@@ -0,0 +1,10 @@
+(library
+ (name byterun)
+ (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
+ (public_name coq.vm)
+ (c_names coq_fix_code coq_memory coq_values coq_interp))
+
+(rule
+ (targets coq_jumptbl.h)
+ (deps (:h-file coq_instruct.h))
+ (action (run ./make_jumptbl.sh %{h-file} %{targets})))
diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh
new file mode 100755
index 0000000000..eacd4daac8
--- /dev/null
+++ b/kernel/byterun/make_jumptbl.sh
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2}
diff --git a/kernel/dune b/kernel/dune
new file mode 100644
index 0000000000..011af9c28c
--- /dev/null
+++ b/kernel/dune
@@ -0,0 +1,15 @@
+(library
+ (name kernel)
+ (synopsis "The Coq Kernel")
+ (public_name coq.kernel)
+ (wrapped false)
+ (modules_without_implementation cinstr nativeinstr)
+ (libraries clib config lib byterun))
+
+(rule
+ (targets copcodes.ml)
+ (deps (:h-file byterun/coq_instruct.h) make-opcodes)
+ (action (run ./make_opcodes.sh %{h-file} %{targets})))
+
+(documentation
+ (package coq))
diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh
new file mode 100755
index 0000000000..bb8aba2f07
--- /dev/null
+++ b/kernel/make_opcodes.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+script_dir="$(dirname "$0")"
+tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' | awk -f "$script_dir"/make-opcodes > "${2}"
diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000000..232c208aa6
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1,7 @@
+(library
+ (name lib)
+ (synopsis "Coq's Utility Library [coq-specific]")
+ (public_name coq.lib)
+ (wrapped false)
+ (modules_without_implementation xml_datatype)
+ (libraries threads coq.clib coq.config))
diff --git a/library/dune b/library/dune
new file mode 100644
index 0000000000..344fad5a75
--- /dev/null
+++ b/library/dune
@@ -0,0 +1,9 @@
+(library
+ (name library)
+ (synopsis "Coq's Loadable Libraries (vo) Support")
+ (public_name coq.library)
+ (wrapped false)
+ (libraries kernel))
+
+(documentation
+ (package coq))
diff --git a/parsing/dune b/parsing/dune
new file mode 100644
index 0000000000..b70612a52b
--- /dev/null
+++ b/parsing/dune
@@ -0,0 +1,20 @@
+(library
+ (name parsing)
+ (public_name coq.parsing)
+ (wrapped false)
+ (libraries proofs))
+
+(rule
+ (targets cLexer.ml)
+ (deps (:ml4-file cLexer.ml4))
+ (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets})))
+
+(rule
+ (targets g_prim.ml)
+ (deps (:mlg-file g_prim.mlg))
+ (action (run coqpp %{mlg-file})))
+
+(rule
+ (targets g_constr.ml)
+ (deps (:mlg-file g_constr.mlg))
+ (action (run coqpp %{mlg-file})))
diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/plugin_base.dune
new file mode 100644
index 0000000000..6a024358c3
--- /dev/null
+++ b/plugins/btauto/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name btauto_plugin)
+ (public_name coq.plugins.btauto)
+ (synopsis "Coq's btauto plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/plugin_base.dune
new file mode 100644
index 0000000000..2a92996d2a
--- /dev/null
+++ b/plugins/cc/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name cc_plugin)
+ (public_name coq.plugins.cc)
+ (synopsis "Coq's congruence closure plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/plugin_base.dune
new file mode 100644
index 0000000000..ba9cd595ce
--- /dev/null
+++ b/plugins/derive/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name derive_plugin)
+ (public_name coq.plugins.derive)
+ (synopsis "Coq's derive plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/plugin_base.dune
new file mode 100644
index 0000000000..037b0d5053
--- /dev/null
+++ b/plugins/extraction/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name extraction_plugin)
+ (public_name coq.plugins.extraction)
+ (synopsis "Coq's extraction plugin")
+ (libraries num coq.plugins.ltac))
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune
new file mode 100644
index 0000000000..bcbb99d9fc
--- /dev/null
+++ b/plugins/firstorder/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name ground_plugin)
+ (public_name coq.plugins.ground)
+ (synopsis "Coq's first order logic solver plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/fourier/plugin_base.dune b/plugins/fourier/plugin_base.dune
new file mode 100644
index 0000000000..8cc76f6f9e
--- /dev/null
+++ b/plugins/fourier/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name fourier_plugin)
+ (public_name coq.plugins.fourier)
+ (synopsis "Coq's fourier plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
new file mode 100644
index 0000000000..002eb28eea
--- /dev/null
+++ b/plugins/funind/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name recdef_plugin)
+ (public_name coq.plugins.recdef)
+ (synopsis "Coq's functional induction plugin")
+ (libraries coq.plugins.extraction))
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
new file mode 100644
index 0000000000..5611f5ba16
--- /dev/null
+++ b/plugins/ltac/plugin_base.dune
@@ -0,0 +1,13 @@
+(library
+ (name ltac_plugin)
+ (public_name coq.plugins.ltac)
+ (synopsis "Coq's LTAC tactic language")
+ (modules :standard \ tauto)
+ (libraries coq.stm))
+
+(library
+ (name tauto_plugin)
+ (public_name coq.plugins.tauto)
+ (synopsis "Coq's tauto tactic")
+ (modules tauto)
+ (libraries coq.plugins.ltac))
diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune
new file mode 100644
index 0000000000..0ae0e6855d
--- /dev/null
+++ b/plugins/micromega/plugin_base.dune
@@ -0,0 +1,7 @@
+(library
+ (name micromega_plugin)
+ (public_name coq.plugins.micromega)
+ ; be careful not to link the executable to the plugin!
+ (modules (:standard \ csdpcert))
+ (synopsis "Coq's micromega plugin")
+ (libraries num coq.plugins.ltac))
diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/plugin_base.dune
new file mode 100644
index 0000000000..9da5b39972
--- /dev/null
+++ b/plugins/nsatz/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name nsatz_plugin)
+ (public_name coq.plugins.nsatz)
+ (synopsis "Coq's nsatz solver plugin")
+ (libraries num coq.plugins.ltac))
diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/plugin_base.dune
new file mode 100644
index 0000000000..f512501c78
--- /dev/null
+++ b/plugins/omega/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name omega_plugin)
+ (public_name coq.plugins.omega)
+ (synopsis "Coq's omega plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/quote/plugin_base.dune b/plugins/quote/plugin_base.dune
new file mode 100644
index 0000000000..323906acb2
--- /dev/null
+++ b/plugins/quote/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name quote_plugin)
+ (public_name coq.plugins.quote)
+ (synopsis "Coq's quote plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/romega/plugin_base.dune b/plugins/romega/plugin_base.dune
new file mode 100644
index 0000000000..49b0e10edf
--- /dev/null
+++ b/plugins/romega/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name romega_plugin)
+ (public_name coq.plugins.romega)
+ (synopsis "Coq's romega plugin")
+ (libraries coq.plugins.omega))
diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/plugin_base.dune
new file mode 100644
index 0000000000..233845ae0f
--- /dev/null
+++ b/plugins/rtauto/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name rtauto_plugin)
+ (public_name coq.plugins.rtauto)
+ (synopsis "Coq's rtauto plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune
new file mode 100644
index 0000000000..101246e28f
--- /dev/null
+++ b/plugins/setoid_ring/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name newring_plugin)
+ (public_name coq.plugins.setoid_ring)
+ (synopsis "Coq's setoid ring plugin")
+ (libraries coq.plugins.quote))
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune
new file mode 100644
index 0000000000..de9053f1a0
--- /dev/null
+++ b/plugins/ssr/plugin_base.dune
@@ -0,0 +1,6 @@
+(library
+ (name ssreflect_plugin)
+ (public_name coq.plugins.ssreflect)
+ (synopsis "Coq's ssreflect plugin")
+ (modules_without_implementation ssrast)
+ (libraries coq.plugins.ssrmatching))
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune
new file mode 100644
index 0000000000..06f67c3774
--- /dev/null
+++ b/plugins/ssrmatching/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name ssrmatching_plugin)
+ (public_name coq.plugins.ssrmatching)
+ (synopsis "Coq ssrmatching plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
new file mode 100644
index 0000000000..bfdd480fe9
--- /dev/null
+++ b/plugins/syntax/plugin_base.dune
@@ -0,0 +1,35 @@
+(library
+ (name numeral_notation_plugin)
+ (public_name coq.plugins.numeral_notation)
+ (synopsis "Coq numeral notation plugin")
+ (modules g_numeral numeral)
+ (libraries coq.plugins.ltac))
+
+(library
+ (name r_syntax_plugin)
+ (public_name coq.plugins.r_syntax)
+ (synopsis "Coq syntax plugin: reals")
+ (modules r_syntax)
+ (libraries coq.vernac))
+
+(library
+ (name ascii_syntax_plugin)
+ (public_name coq.plugins.ascii_syntax)
+ (synopsis "Coq syntax plugin: ASCII")
+ (modules ascii_syntax)
+ (libraries coq.vernac))
+
+(library
+ (name string_syntax_plugin)
+ (public_name coq.plugins.string_syntax)
+ (synopsis "Coq syntax plugin: strings")
+ (modules string_syntax)
+ (libraries coq.plugins.ascii_syntax))
+
+(library
+ (name int31_syntax_plugin)
+ (public_name coq.plugins.int31_syntax)
+ (synopsis "Coq syntax plugin: int31")
+ (modules int31_syntax)
+ (libraries coq.vernac))
+
diff --git a/plugins/xml/README b/plugins/xml/README
deleted file mode 100644
index 3128189929..0000000000
--- a/plugins/xml/README
+++ /dev/null
@@ -1,4 +0,0 @@
-The xml export plugin for Coq has been removed from the sources.
-A backward compatible plug-in will be provided as a third-party plugin.
-For more informations, contact
-Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>.
diff --git a/pretyping/dune b/pretyping/dune
new file mode 100644
index 0000000000..6609b4e328
--- /dev/null
+++ b/pretyping/dune
@@ -0,0 +1,6 @@
+(library
+ (name pretyping)
+ (synopsis "Coq's Type Inference Component (Pretyper)")
+ (public_name coq.pretyping)
+ (wrapped false)
+ (libraries camlp5.gramlib engine))
diff --git a/printing/dune b/printing/dune
new file mode 100644
index 0000000000..3392342165
--- /dev/null
+++ b/printing/dune
@@ -0,0 +1,6 @@
+(library
+ (name printing)
+ (synopsis "Coq's Term Pretty Printing Library")
+ (public_name coq.printing)
+ (wrapped false)
+ (libraries parsing proofs))
diff --git a/proofs/dune b/proofs/dune
new file mode 100644
index 0000000000..679c45f6bf
--- /dev/null
+++ b/proofs/dune
@@ -0,0 +1,6 @@
+(library
+ (name proofs)
+ (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure")
+ (public_name coq.proofs)
+ (wrapped false)
+ (libraries interp))
diff --git a/stm/dune b/stm/dune
new file mode 100644
index 0000000000..c369bd00fb
--- /dev/null
+++ b/stm/dune
@@ -0,0 +1,6 @@
+(library
+ (name stm)
+ (synopsis "Coq's Document Manager and Proof Checking Scheduler")
+ (public_name coq.stm)
+ (wrapped false)
+ (libraries vernac))
diff --git a/tactics/dune b/tactics/dune
new file mode 100644
index 0000000000..908dde5253
--- /dev/null
+++ b/tactics/dune
@@ -0,0 +1,6 @@
+(library
+ (name tactics)
+ (synopsis "Coq's Core Tactics [ML implementation]")
+ (public_name coq.tactics)
+ (wrapped false)
+ (libraries printing))
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
new file mode 100644
index 0000000000..c89c78c8ec
--- /dev/null
+++ b/tools/coq_dune.ml
@@ -0,0 +1,283 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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 "@;"
+
+  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 *)
+  module Legacy = struct
+
+    (* 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
+
+    (* Available in OCaml >= 4.04 *)
+    let split_on_char sep s =
+      let open String in
+      let r = ref [] in
+      let j = ref (length s) in
+      for i = length s - 1 downto 0 do
+        if unsafe_get s i = sep then begin
+          r := sub s (i + 1) (!j - i - 1) :: !r;
+          j := i
+        end
+      done;
+      sub s 0 !j :: !r
+  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
+
+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"; }
+  ]
+
+  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 | ML4 of string | 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 *)
+
+(* 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
+
+let gen_sub n =
+  (* Move to List.init once we can depend on OCaml >= 4.06.0 *)
+  String.concat "/" (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
+
+(* 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 "", ["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 -> sdir ^ s) (edep @ vo.deps) in
+  (* The source file is also corrected as we will call coqtop from the top dir *)
+  let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in
+  (* The final build rule *)
+  let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in
+  pp_rule fmt [vo.target] deps action
+
+let pp_ml4_dep _dir fmt ml =
+  let target = Filename.(remove_extension ml) ^ ".ml" in
+  let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in
+  pp_rule fmt [target] [ml] ml4_rule
+
+let pp_mlg_dep _dir fmt ml =
+  let target = Filename.(remove_extension ml) ^ ".ml" in
+  let ml4_rule = "(run coqpp %{pp-file})" in
+  pp_rule fmt [target] [ml] ml4_rule
+
+let pp_dep dir fmt oo = match oo with
+  | VO vo -> pp_vo_dep dir fmt vo
+  | ML4 f -> pp_ml4_dep dir fmt f
+  | MLG f -> pp_mlg_dep dir fmt f
+
+let out_install fmt dir ff =
+  let itarget = String.concat "/" dir in
+  let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in
+  let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (itarget^"/"^tg) in
+  fprintf fmt "(install@\n @[(section lib)@\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 = String.concat "/" d in
+  if Sys.file_exists sd && Sys.is_directory sd then
+    let out = open_out (sd^"/dune") in
+    let fmt = formatter_of_out_channel out in
+    if List.nth d 0 = "plugins" 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 choose_ml4g_form f =
+  if Filename.check_suffix f ".ml4" then ML4 f
+  else MLG f
+
+let scan_mlg4 m d =
+  let dir = ["plugins"; d] in
+  let m = DirMap.add dir [] m in
+  let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg"))
+                   Array.(to_list @@ readdir String.(concat "/" dir))) in
+  List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4
+
+let scan_plugins m =
+  let dirs = Sys.(List.filter (fun f -> is_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in
+  List.fold_left scan_mlg4 m dirs
+
+(* 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
+      Some (Legacy.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 ic = open_in Sys.argv.(1) in
+    (try f ic with _ -> close_in ic)
+  | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1
+
+let _ =
+  exec_ifile (fun ic ->
+      let map = scan_plugins DirMap.empty in
+      let map = read_vfiles ic map in
+      out_map map)
diff --git a/tools/dune b/tools/dune
new file mode 100644
index 0000000000..2ba0e3fe8a
--- /dev/null
+++ b/tools/dune
@@ -0,0 +1,31 @@
+(executable
+ (name coqc)
+ (public_name coqc)
+ (modules coqc)
+ (libraries coq.toplevel))
+
+(executable
+ (name coq_makefile)
+ (public_name coq_makefile)
+ (modules coq_makefile)
+ (libraries coq.lib))
+
+(executable
+ (name coqdep)
+ (public_name coqdep)
+ (modules coqdep_lexer coqdep_common coqdep)
+ (libraries coq.lib))
+
+(ocamllex coqdep_lexer)
+
+(executable
+ (name coq_tex)
+ (public_name coq_tex)
+ (modules coq_tex)
+ (libraries str))
+
+(executable
+ (name coq_dune)
+ (public_name coq_dune)
+ (modules coq_dune)
+ (libraries str))
diff --git a/topbin/dune b/topbin/dune
new file mode 100644
index 0000000000..e89f6c4b13
--- /dev/null
+++ b/topbin/dune
@@ -0,0 +1,25 @@
+(executable
+ (name coqtop_bin)
+ (public_name coqtop)
+ (package coq)
+ (modules coqtop_bin)
+ (libraries coq.toplevel)
+ (link_flags -linkall))
+
+(executable
+ (name coqtop_byte_bin)
+ (public_name coqtop.byte)
+ (package coq)
+ (modules coqtop_byte_bin)
+ (libraries compiler-libs.toplevel coq.toplevel)
+ (modes byte)
+ (link_flags -linkall))
+
+; Workers
+(executables
+ (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin)
+ (public_names coqqueryworker.opt coqtacticworker.opt coqproofworker.opt)
+ (package coq)
+ (modules :standard \ coqtop_byte_bin coqtop_bin)
+ (libraries coq.toplevel)
+ (link_flags -linkall))
diff --git a/toplevel/dune b/toplevel/dune
new file mode 100644
index 0000000000..f51e50aaa3
--- /dev/null
+++ b/toplevel/dune
@@ -0,0 +1,13 @@
+(library
+ (name toplevel)
+ (public_name coq.toplevel)
+ (synopsis "Coq's Interactive Shell [terminal-based]")
+ (wrapped false)
+ (libraries num coq.stm))
+; Coqlevel provides the `Num` library to plugins, we could also use
+; -linkall in the plugins file, to be discussed.
+
+(rule
+ (targets g_toplevel.ml)
+ (deps (:mlg-file g_toplevel.mlg))
+ (action (run coqpp %{mlg-file})))
diff --git a/vernac/dune b/vernac/dune
new file mode 100644
index 0000000000..45b567d631
--- /dev/null
+++ b/vernac/dune
@@ -0,0 +1,16 @@
+(library
+ (name vernac)
+ (synopsis "Coq's Vernacular Language")
+ (public_name coq.vernac)
+ (wrapped false)
+ (libraries tactics parsing))
+
+(rule
+ (targets g_proofs.ml)
+ (deps (:mlg-file g_proofs.mlg))
+ (action (run coqpp %{mlg-file})))
+
+(rule
+ (targets g_vernac.ml)
+ (deps (:mlg-file g_vernac.mlg))
+ (action (run coqpp %{mlg-file})))