[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
coq#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 coq#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
```

.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

.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

.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:

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    $<'

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

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))
+

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))
+

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))))

coq.opam

@@ -0,0 +1,22 @@
+opam-version: "1.2"
+maintainer: "The Coq development team <[email protected]>"
+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 ]
+]

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
   ()
 

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))

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:
 

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

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
 ----------

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.

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)))

dune-project

@@ -0,0 +1,3 @@
+(lang dune 1.0)
+
+(name coq-devel)

engine/dune

@@ -0,0 +1,6 @@
+(library
+ (name engine)
+ (synopsis "Coq's Tactic Engine")
+ (public_name coq.engine)
+ (wrapped false)
+ (libraries library))