| Age | Commit message (Collapse) | Author |
|---|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
No diff to sources (luckily), see release notes at
https://discuss.ocaml.org/t/ann-ocamlformat-0-14-0/5435 for more
information.
|
|
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
It is unfortunate that we cannot install coqide and Dune 2.5.0 in < 4.07.0
|
|
Cf. #12049.
|
|
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
|
|
|
|
The idea is very simple: use the list in the release branch to know
which changelog entries to include, but do the work of removing these
entries and consolidating the released changelog in the master branch
(so that it is applied both to the master branch and to the release
branch following the backporting process).
|
|
Auto-generated files like the Makefile have recently been removed from
the sources (cf. coq-community/corn#88). Calling ./configure.sh is
now required.
|
|
Reviewed-by: JasonGross
|
|
Reviewed-by: ejgallego
|
|
Ack-by: Matafou
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
- problem with metacoq overlay ; it expects to send a non-ground
constant to the kernel, now it fails at prepare.
Record Sigma (A : Type) (B : A -> Type) : Type :=
{ fst : A ; snd : B fst }.
Arguments fst {A B}.
Arguments snd {A B}.
Quote Recursively Definition foo := (fst, snd).
There is a hack on the overlay, we need to discuss it a bit more.
|
|
Fix #11967
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
I believe a recent commit to master broke it, and now that it's no
longer tested as part of fiat-crypto-legacy, I think it's time to add
it.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
Thanks to `.ocamlformat-ignore`, we can call ocamlformat blindly but
only the non-ignored files will be affected.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
We include the `version=0.13.0` field that should help users not to
use the wrong version. `disable=true` still seems a noop with `dune`.
There are some minor changes in the way comments are formatted; I'm
unsure if this is due to the `wrap-comments` option; as always; tweaks
to the config are most welcome.
|
|
There is a lot of check overhead in the code, we will try to provide a
more convenient API for manipulation of remaining obligations.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: herbelin
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
That release includes non trivial changes related C compilers, in
particular due to `-fno-common` support.
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
|
|
|
|
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
|
|
10.13 is deprecated as an azure VM
Close #11449
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
