| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We update the instructions a bit providing the name of the Debian
packages, we also mention Nix and add to .gitignore a
Sphinx-autogenerated file.
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.
Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.
Closes #6689.
|
| | |_|_|/ /
|/| | | | |
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We move gitlab runners to Ubuntu 18.04 "Bionic"; this allows us to
install most base dependencies using APT, and opens up the door to
saving quite a bit of time by creating a custom docker image
[c.f. #7383]
This change comes with an update of dependencies; we tweak them. Also:
- we add a more precise cache `key` constraint; this is still done
manually, we should develop an automated way in another PR. The
format is "$image-v$date-$hour-$minute"
- we export DEBIAN_FRONTEND=noninteractive as to avoid problems with
package installs that ask for interactive input.
- we install Sphinx Python packages using `apt` save for
python3-antlr4, which is still unpackaged [see
https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=897129]
|
| |\ \ \ \ |
|
| |/ / / /
| | | |
| | | |
| | | | |
AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Newer versions don't have the latex packages we want.
see eg https://gitlab.com/SkySkimmer/coq/-/jobs/65498131
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| |_|/ / / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| | | |/ / / / |
|
| | |/ / / /
|/| | | |
| | | | |
| | | | | |
It begs things to break when the cache is out of sync with the system packages.
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
of evars
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Flags.univ_print
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| | |_|_|_|_|_|/ /
|/| | | | | | | |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \
| |_|_|_|_|/ / / /
|/| | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
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)
|
| | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \
| |_|_|/ / / / / /
|/| | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \
| |_|_|_|_|/ / / /
|/| | | | | | | |
| | | | | | | | | |
indirect uses of tactic `clear`.
|
| |\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
come, misc improvements
|
| |\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
hypotheses.
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| | |_|_|/ / / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
- Be more precise when trying to clear an hypothesis which
occurs implicitly in a global constant.
- Warns if destruct/induction cannot clear an hypothesis occurring
implicitly in a global.
In the first case, the change in situation
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a.
is:
- before: "a is used in conclusion"
- after: "a is used implicitly in b in conclusion"
In the second case:
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a.
produces a warning: "Cannot remove a, it is used implicitly in b".
|
| | |/ / / / / / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
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...
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | |
|
| | | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
NB: I made .aux be cleaned only with distclean imitating the main Makefile.
|
| | | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
ie you might see
make
TEST bugs/closed/1337.v
TEST bugs/closed/3263.v
TEST bugs/closed/7777.v
FAILED bugs/closed/3263.v.log
TEST bugs/opened/1.v
...
report: 3263 failed (should be closed)
|
| | |_|_|_|/ / / / / / /
|/| | | | | | | | | | |
|
| | |_|_|_|_|_|/ / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Warnings are just too hard to see. Also there is no point keeping a
noop option except to point people at the replacement, which does not
require configure to succeed.
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| | |/ / / / / / / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
This will catch things like
https://github.com/coq/coq/pull/7025#issuecomment-381424489
|
Emilio Jesus Gallego Arias
Théo Zimmermann
Pierre-Marie Pédrot
Maxime Dénès
Gaëtan Gilbert
Enrico Tassi
Hugo Herbelin
Beta Ziliani
Kazuhiko Sakaguchi
Jason Gross