| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
This has been around for at least 16 years, with the comment
"this won't last long I hope".
https://github.com/coq/coq/commit/12965209478bd99dfbe57f07d5b525e51b903f22#diff-1a3a6f7bd5b2cf1bc6dd43ee04bbc3eaR112
|
| |\
| |
| |
| | |
hypotheses.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
Four modes currently supported to deal with clashes:
1. Failing in case of clash
2. Renaming the most recent one
3. Renaming the previous hypothesis of same name if not a section variable
4. Renaming the previous hypothesis of same name even if a section variable
The current mode is 3. Keeping it active by default
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |/ / / / / |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Toplevels may want to modify for example the Stm flags,
which after #1108 are handled in a functional way.
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | |
|
| | |_|_|/ / / / / / / / /
|/| | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | |
|
| | | | | | |_|_|/ / / / / /
| | | | |/| | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | | |
`apply.whitespace = fix`
|
| | | | | | |/ / / / / / / / |
|
| |/ / / / / / / / / / / /
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
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.
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |/ / / / / / / / / / / / |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |/ / / / / / / / / / / / |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | |
|
| |\| | | | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
Like circle CI we install every opam package in opam-boot jobs (one
per switch).
This should be more reliable with less issues from outdated cache.
Also avoid messing with symlinks through OPAMROOT (we can't
cache/artifact files outside the coq directory).
Avoid using "system" compiler (no risk of getting an upgrade through
the base image).
|
| | | | | | | | | | | | | | | | | |
|
| | |_|_|_|_|/ / / / / / / / / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
- BUILD_TARGET not used
- Put elpi's FINDLIB_VER="" at the end of the environment for nicer
display in the travis UI.
|
| | |/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | |
|
Jasper Hugunin
Pierre-Marie Pédrot
Hugo Herbelin
Emilio Jesus Gallego Arias
Jason Gross
Anton Trunov
Maxime Dénès
Enrico Tassi
Vincent Laporte
Ralf Jung
Théo Zimmermann
Gaëtan Gilbert
Pierre Letouzey