coq/dune-project, branch master

[build] Split stdlib to it's own opam package.

2021-03-03T15:06:14+00:00

We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.

Merge PR #13640: Add ounit2 to with-test dependencies

2021-02-11T20:06:44+00:00

Reviewed-by: ejgallego

Add ounit2 to with-test dependencies

2020-12-16T08:38:03+00:00

Add build dependency of conf-ptyon-3 to coq-doc

2020-12-16T08:35:39+00:00

[dune] [opam] Disable dune subst in opam files until the upstream fix is propagated

2020-12-04T16:24:20+00:00

`dune subst` is broken on unicode files, see
https://github.com/ocaml/dune/pull/3879 and
https://github.com/ocaml/dune/pull/3879

This is a frequent problem, introduced by
https://github.com/coq/coq/pull/13374 , so disabling pending on dune
2.8 being released.

[dune] [opam] Generate opam files automatically using Dune.

2020-11-15T16:08:52+00:00

- closes #12376 : dune version is now consistent as suggested
- cc #12858 : coqide and coqide-server do no depend on ocamlfind
  when built this way.
- closes #13372 : more precision in the license identifier

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

2020-04-11T21:45:18+00:00

This completes a pure Dune bootstrap of Coq.

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

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

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

[fmt] [dune] Add ocamlformat configuration.

2019-12-13T13:15:36+00:00

For now we don't enable it in any source file, neither on dune files.

`lint-repository` has been updated so it will check `dune build @fmt`
returns 0.

[dune] Update to dune language version 2.0

2019-12-04T13:14:58+00:00

This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.

Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.

[dune] Move to Dune 1.10, use coq.pp directive.

2019-08-22T00:37:33+00:00

We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.

Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.

Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.

I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.