| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
The OPAM 1.2 repository has been frozen, thus we must use OPAM 2.0 if
we want to get newer versions of packages / compilers.
For now we must perform a manual install of OPAM as no packages for
Ubuntu 18.04 exist.
Note that this means nothing about the installability of Coq itself,
whose OPAM repository should remain in 1.2 format for quite a long
period.
|
|
|
|
Don't zip artifacts but create an artifact folder structure
|
|
cleanup and stability and logging enhancements from v8.8
|
|
This is a hack to enable correct OPAM building, the medium-term plan
is to avoid having to set a prefix at configure time but instead using
a set of rules to locate the Coq library.
We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
|
|
The minimum required versions of the Sphinx-related (and ANTLR)
Python packages for Coq 8.10 were chosen as the lower bound
between what is currently in Debian Buster and in NixOS 18.09
Jellyfish (in practice the lower bound was always met by NixOS
18.09 Jellyfish).
These minimum required versions were documented.
In the docker image used by GitLab CI, we install these
Python packages through pip as this allows us to pin them
to these specific versions.
In Travis, we let them unspecified to always test the
latest versions.
Finally, we also add the new dependencies of the Sphinx
PDF manual.
|
|
unification.
|
|
|
|
|
|
We build the `@doc` target in the `dune` job:
- The documentation can be found in `_build/default/_doc/`
- We had to fix a couple of quoting problems.
|
|
- odoc: used to generate the ML API documentation by Dune's `@doc`
target.
- dune-release: Automatic OPAM package generation and release.
Both packages require OCaml >= 4.02 thus installing on edge switches
only.
|
|
|
|
[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
```
|
|
|
|
|
|
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.
Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.
Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.
cc: #7155
|
|
following #8348.
|
|
passed in the cache
|
|
|
|
The overlay for HoTT should be merged right after this PR.
|
|
|
|
|
|
|
|
This allows to use fixed commits and not just branches or tags.
We keep using git clone when $FORCE_GIT is set (for projects on
gforge.inria.fr and projects pulling dependencies through git submodules).
fiat-parsers also calls git submodule, but inside its own Makefile.
|
|
|
|
We'd like to use `(lang 1.1)` features. Elpi needs update as recent
`ppx_tools_versioned` changes broke it.
|
|
This tests the outputs of extraction, to some extent.
|
|
This has become mostly garbage since GitLab CI became our main CI platform.
|
|
There is the new pipeline, and the old pipeline. Most of what they
share in common is the (very large) library of lemmas about `Z`.
As per the discussion in
https://github.com/coq/coq/pull/8064#issuecomment-413474176 through
https://github.com/coq/coq/pull/8064#issuecomment-413793143
|
|
|
|
GitLab setup is quite stable these days thanks to the work of many
people and `coqbot`. We decided to keep CircleCI support for a while
as a safeguard in case something happened in the migration to GitLab,
but these days we are just wasting resources to them and to us. As I'm
afraid CircleCI won't scale for us, the time to remove it has arrived.
Still, CircleCI had some awesome functionality that GitLab's CI
doesn't offer yet, see the links at:
https://github.com/coq/coq/issues/6919#issuecomment-395885573
- https://gitlab.com/gitlab-org/gitlab-ce/issues/29347
- https://gitlab.com/gitlab-org/gitlab-ce/issues/35222
- https://gitlab.com/gitlab-org/gitlab-ce/issues/41947
- https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
|
|
|
|
errors
|
|
|
|
|
|
|
|
|
|
|
|
The changed QuestionMark structure breaks Coq-Equations.
Add an overlay to fix this.
|
|
|
|
|
|
|
|
- We update the OCaml version used in the base CI image.
- Windows / OSX image building is also updated to use newer OCaml.
- We also update Dune to 1.0.0.
|
|
|
|
|
|
|
|
with apt.
|
