[build] Preliminary support for building Coq with `dune`.

[Dune](https://github.com/ocaml/dune) is a compositional declarative
build system for OCaml. It provides automatic generation of
`version.ml`, `.merlin`, `META`, `opam`, API documentation; install
management; easy integration with external libraries, test runners,
and modular builds.

In particular, Dune uniformly handles components regardless whether
they live in, or out-of-tree. This greatly simplifies cases where a
plugin [or CoqIde] is checked out in the current working copy but then
distributed separately [and vice-versa]. Dune can thus be used as a
more flexible `coq_makefile` replacement.

For now we provide experimental support for a Dune build. In order to
build Coq + the standard library with Dune type:

```
$ make -f Makefile.dune world
```

This PR includes a preliminary, developer-only preview of Dune for
Coq. There is still ongoing work, see
https://github.com/coq/coq/issues/8052 for tracking status towards
full support.

## Technical description.

Dune works out of the box with Coq, once we have fixed some modularity
issues. The main remaining challenge was to support `.vo` files.

As Dune doesn't support custom build rules yet, to properly build
`.vo` files we provide a small helper script `tools/coq_dune.ml`. The
script will scan the Coq library directories and generate the
corresponding rules for `.v -> .vo` and `.ml4 -> .ml` builds. The
script uses `coqdep` as to correctly output the dependencies of
`.v` files. `coq_dune` is akin to `coq_makefile` and should be able to
be used to build Coq projects in the future.

Due to this pitfall, the build process has to proceed in three stages:
1) build `coqdep` and `coq_dune`; 2) generate `dune` files for
`theories` and `plugins`; 3) perform a regular build with all
targets are in scope.

## FAQ

### Why Dune?

Coq has a moderately complex build system and it is not a secret that
many developer-hours have been spent fighting with `make`.

In particular, the current `make`-based system does offer poor support
to verify that the current build rules and variables are coherent, and
requires significant manual, error-prone. Many variables must be
passed by hand, duplicated, etc... Additionally, our make system
offers poor integration with now standard OCaml ecosystem tools such
as `opam`, `ocamlfind` or `odoc`. Another critical point is build
compositionality. Coq is rich in 3rd party contributions, and a big
shortcoming of the current make system is that it cannot be used to
build these projects; requiring us to maintain a custom tool,
`coq_makefile`, with the corresponding cost.

In the past, there has been some efforts to migrate Coq to more
specialized build systems, however these stalled due to a variety of
reasons. Dune, is a declarative, OCaml-specific build tool that is on
the path to become the standard build system for the OCaml ecosystem.

Dune seems to be a good fit for Coq well: it is well-supported, fast,
compositional, and designed for large projects.

### Does Dune replace the make-based build system?

The current, make-based build system is unmodified by this PR and kept
as the default option. However, Dune has the potential

### Is this PR complete? What does it provide?

This PR is ready for developer preview and feedback. The build system
is functional, however, more work is necessary in order to make Dune
the default for Coq.

The main TODOs are tracked at https://github.com/coq/coq/issues/8052

This PR allows developers to use most of the features of Dune today:

- Modular organization of the codebase; each component is built only
  against declared dependencies so components are checked for
  containment more strictly.
- Hygienic builds; Dune places all artifacts under `_build`.
- Automatic generation of `.install` files, simplified OPAM workflow.
- `utop` support, `-opaque` in developer mode, etc...
- `ml4` files are handled using `coqp5`, a native-code customized
  camlp5 executable which brings much faster `ml4 -> ml` processing.

### What dependencies does Dune require?

Dune doesn't depend on any 3rd party package other than the OCaml compiler.

### Some Benchs:

```
$ /usr/bin/time make DUNEOPT="-j 1000" -f Makefile.dune states
59.50user 18.81system 0:29.83elapsed 262%CPU (0avgtext+0avgdata 302996maxresident)k
0inputs+646632outputs (0major+4893811minor)pagefaults 0swaps

$ /usr/bin/time sh -c "./configure -local -native-compiler no && make -j states"
88.21user 23.65system 0:32.96elapsed 339%CPU (0avgtext+0avgdata 304992maxresident)k
0inputs+1051680outputs (0major+5300680minor)pagefaults 0swaps
```

60 files changed, 1004 insertions, 16 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/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})))