| Age | Commit message (Collapse) | Author |
|---|
|
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
|
We call configure to properly regenerate the Makefile and its dependencies.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In the original Travis CI setup, the per-job time limit was an
issue. However, Gitlab has much improved this problem due to
a) Coq not being built for each contrib,
b) user-configurable time limit.
We thus disable the expensive builds from Travis:
`fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`,
`math-comp`, `unimath`, `vst`
and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`]
in full.
We also update the `math-comp` script as the `odd-order` theorem lives
in a separate repository and it is a key CI case.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We use a specific runner on Inria CloudStack. This allows us to have the
same build infrastructure setup for signed and unsigned binary packages.
The main Coq repository on Gitlab will produce unsigned binaries, using
a runner without secret. On my repository, a one-click operation will
sign the packages, making this part of the release process smoother.
|
|
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't
miss anything.
|
|
We also introduce a bit more systematic job naming: `base/edge`.
In order to make the flambda switch selectable we update the Docker
image so all the dependencies are installed in that one.
Note the extra quote rule for the flambda parameters, but unless we
can assign arrays to Gitlab variables there is not a good way to do
this I'm afraid.
With this patch we are getting close to being able to remove most
builds from Travis.
|
|
This should help #6808.
|
|
We provide a custom `Dockerfile` for Coq's CI system, based on
`ubuntu:bionic`. The image includes the required set of packages and
OPAM switches.
This greatly simplifies the Gitlab and Circle scripts, at the cost of
having to push a Docker build for them to depend on.
Travis is not included in this PR as it requires significant more
refactoring due to lack of native Docker support.
This is work in progress but ready, a build hook is used so the image
is properly tagged in the Docker autobuilder.
We need to improve the autobuilder setup but this last point requires
some design on how to trigger it.
Fixes #7383
|
|
|
|
|
|
This is closer to what we mean than reproducing the default target
without progs.
|
|
This is due to our CI script relying on their makefile internals,
unfortunately we still have to do this to avoid timeouts.
|
|
|
|
|
|
|
|
This will catch things like
https://github.com/coq/coq/pull/7025#issuecomment-381424489
|
|
|
|
|
|
|
|
|
|
|
|
|
|
contains evars
|
|
|
|
|
|
Morally, `library` should not depend on the vernacular
definition. This will also create problems when trying to modularize
the codebase due to the cycle [vernacs depend for example on
constrexprs].
The fix is fortunately easy.
|
|
|
|
We solve some modularity and type duplication problems by moving types
to a better place. In particular:
- We move tactics types from `Misctypes` to `Tactics` as this is their
proper module an single user [with LTAC].
- We deprecate aliases in `Tacexpr` to such tactic types.
cc: #6512
|
|
We forbid calling `EConstr.to_constr` on terms that are not evar-free,
as to progress towards enforcing the invariant that `Constr.t` is
evar-free. [c.f. #6308]
Due to compatibility constraints we provide an optional parameter to
`to_constr`, `abort` which can be used to overcome this restriction
until we fix all parts of the code.
Now, grepping for `~abort:false` should return the questionable
parts of the system.
Not a lot of places had to be fixed, some comments:
- problems with the interface due to `Evd/Constr` [`Evd.define` being
the prime example] do seem real!
- inductives also look bad with regards to `Constr/EConstr`.
- code in plugins needs work.
A notable user of this "feature" is `Obligations/Program` that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.
|
|
|
|
|
|
Unfortunately, mli-only files cannot be included in packs, so we have
the weird situation that the scope for `Tacexpr` is wrong. So we
cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the
global namespace instead.
This creates problem when using other modular build/packing strategies
[such as #6857] This could be indeed considered a bug in the OCaml
compiler.
In order to remedy this situation we face two choices:
- leave the module out of the pack (!)
- create an implementation for the module
I chose the second solution as it seems to me like the most sensible
choice.
cc: #6512.
|
|
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
|
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
|
|
|
|
|
|
