coq/config, 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.

Get rid of the compilation date from the binaries to make them more stable.

2021-02-16T08:02:37+00:00

Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".

Configure default value of -native-compiler

2020-11-20T18:07:42+00:00

This an implementation of point 2 of CEP coq/ceps#48
https://github.com/coq/ceps/pull/48

Option -native-compiler of the configure script now impacts the
default value of the option -native-compiler of coqc. The
-native-compiler option of the configure script is added an ondemand
value, which becomes the default, thus preserving the previous default
behavior.

The stdlib is still precompiled when configuring with -native-compiler
yes. It is not precompiled otherwise.

dune: pass -bin-annot to configure

2020-09-09T13:18:49+00:00

This ends up in coq_makefile's CAMLFLAGS so we need it to make merlin
work properly.

Avoid running configure when plugins/ modified

2020-08-18T13:43:16+00:00

We use an indirection, producing the sorted list of subdirectories of
plugins/, so that dune can recognize it hasn't changed and doesn't
rerun configure. Since configure regenerates a timestamp this avoids
recompiling the stdlib.

Fix #12750.

Implement a name-based representation for vo files.

2020-04-26T12:24:48+00:00

See CEP#44 for futher details.

Update headers in the whole code base.

2020-03-18T11:15:43+00:00

Add headers to a few files which were missing them.

[dune] Fix bug in auto-configure deps.

2020-03-04T02:38:42+00:00

`plugins` needs to be present to coq_makefile variables are properly
initialized.

[configure] [dune] Fix configure under Dune in 32bit builds.

2019-12-07T17:33:43+00:00

`dev/header.c` is not registered as a dependency, so the configure
step under dune fails in 32bit builds.

Note we don't detect the problem due to dubious code in configure
ignoring stderr messages on process calls.

Have only one dune rule calling configure

2019-11-11T16:43:23+00:00