| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
They are much faster and should be as informative as their heavy counterparts.
I have been forgetting to do that for a long time already.
|
|
Reviewed-by: ppedrot
|
|
This focuses review requests to bench-maintainers instead of sharing
with ci-maintainers
|
|
On GitLab, we don't need to base the job info on the PR number, since
it ought to be available from the git repo. Removing the logic will
make the bench infrastructure more uniform.
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
Tests moved in https://github.com/whonore/Coqtail/pull/134.
|
|
Added user overlay for bignums
|
|
recognition.
Reviewed-by: mattam82
|
|
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
|
|
For convenience
|
|
Reviewed-by: SkySkimmer
Ack-by: silene
|
|
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
|
|
|
|
Reviewed-by: ejgallego
|
|
Otherwise gitlab stops logging somewhere in the middle.
Also pass -o because we can.
|
|
|
|
Reviewed-by: ejgallego
|
|
We make it compatible by expanding "[0-9]\+" into "[0-9][0-9]*".
|
|
- don't `set -x` while loading overlays, non-verbose untaring
- ls _build_ci to help figure out artifact download issues
|
|
|
|
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: proux01
Ack-by: silene
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
|
|
|
|
|
