| Age | Commit message (Collapse) | Author |
|---|
|
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
|
|
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
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
appveyor) and files
|
|
|
|
|
|
|
|
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.
|
|
Flags.univ_print
|
|
|
|
```
$ dev/tools/check-owners-pr.sh 6809 --show-patterns --owner '@MSoegtropIMC'
remote: Counting objects: 93, done.
remote: Compressing objects: 100% (3/3), done.
remote: Total 93 (delta 47), reused 50 (delta 47), pack-reused 43
Unpacking objects: 100% (93/93), done.
From github.com:coq/coq
* branch refs/pull/6809/head -> FETCH_HEAD
* branch master -> FETCH_HEAD
/dev/build/windows: @MSoegtropIMC
```
|
|
This removes the Flags.univ_print in the kernel, making it possible to
put the univ printing flag ownership back in Detyping.
The lazyness is because getting an explanation may be costly and we
may discard it without printing.
See benches
- with lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console
- without lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console
Notably without lazy mathcomp odd_order is +1.26% with some lines
showing significant changes, eg PFsection11 line 874 goes from 11.76s
to 13.23s (+12%).
(with lazy the same development has -1% overall and the same line goes
from 11.76s to 11.23s (-4%) which may be within noise range)
|
|
|
|
|
|
In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.
We move all the files in `intf` to the lowest place their dependencies
can accommodate:
- `Misctypes`: is used by Declaremod, thus it has to go in `library`
or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
could be fixed, as this module should be declared in `interp` which
is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.
Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...
|
|
|
|
|
|
|
|
This will catch things like
https://github.com/coq/coq/pull/7025#issuecomment-381424489
|
|
|
|
|
|
|
|
|
|
|
|
Having `--whitespace=` on all `git apply` in this script should make it
insensitive to user setup in `~/.gitconfig`, at least
`[apply] whitespace = fix`.
Note that even this way, this script remains hugely fragile and non mature,
and would better *not* be set by default for everybody.
|
|
This changed in https://github.com/coq/coq/commit/35961a4ff5a5b8c9b9786cbab0abd279263eb655
|
|
|
|
|
|
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
contains evars
|
|
|
|
|
|
This fulfils Gaetan's wish.
|
|
In case the local branch is ahead of upstream, we only print
a warning because it could be that we are merging several
PRs in a row.
|
|
As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
|
|
This should solve Emilio's problem.
|
|
In case the push URL has been overriden to make it fetch-only.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
