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

[stm] move par: implementation to vernac/comTactic and stm/partac

2020-10-09T15:09:02+00:00

The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).

This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.

Co-authored-by: Gaëtan Gilbert

Update headers in the whole code base.

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

Add headers to a few files which were missing them.

[exn] Forbid raising in exn printers, make them return Pp.t option

2020-02-24T17:24:40+00:00

Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.

We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.

[rfc] [mltop] Removal of dynamic loading of object and `.ml` files

2020-01-29T16:29:45+00:00

This seems seldom used and I think in general instrumentation this way
is pretty limited (usually better to use the build system to tweak)

It thus seems worth removing as to simplify `Mltop` a bit, but of
course comments are welcome.

[mltop] Remove error handling hacks in favor of default methods.

2020-01-16T19:00:03+00:00

We don't need to handle `Dynlink` errors specially anymore.

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

An even more uniform treatment of the -help option across executables.

2019-07-08T00:31:27+00:00

Incidentally fix some missing newline in coqc help, and give proper
help for coqidetop and the "coq*worker"s.

[dune] Enable optimization options in the compilation of the VM.

2019-06-21T11:02:19+00:00

So far we didn't setup optimization flags for the VM in the Dune
build, but time has come to experiment with such flags, we try -O3.

Enabling `-flto` in the final binary build would be great, however
this seems to break windows.

Update ml-style headers to new year.

2019-06-17T16:08:32+00:00