| Age | Commit message (Collapse) | Author |
|---|
|
Broke the build.
This reverts commit ef6459b00999a29183edc09de9035795ff7912e9.
|
|
|
|
|
|
We passed the arc to be marked as visited to the functions pushing the
neighbours on the remaining stack, but this can be actually done before
pushing them, as the [process_le] and [process_lt] functions do not rely
on the visited flag. This exposes more clearly the invariants of the
algorithm.
|
|
A possible script breakage can occur if one has a notation
at level 11 that is also right associative (now 11 is left associative).
Thanks Georges for debugging that.
|
|
Since commit 2f521670fbd, the Require "file" syntax was not used anymore by
coqtop but the code handling it was still there in coqdep. We finish the work
by erasing the remnant code.
|
|
|
|
|
|
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
|
Tracing with gdb by Alec Faithfull
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
|
|
|
|
|
|
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
|
- Proper [family] implementation
- Use the tailor made hash function for Sorts.t in two places.
|
|
|
|
|
|
|
|
|
|
An .emacs-ready elisp snippet to parse location of Anomaly backtraces
and jump to them conveniently from the Emacs *compilation* output.
|
|
There are still two items I do not undertand fully (the last one about
-extra-phony, and the removal of external libraries at make clean time,
that I could not reproduce on a toy example.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This allows fatal_error to be used for printing anomalies at loading time.
|
|
|
|
They appear as axioms of the form `Foo is positive`.
|
|
the interfaces.
|
|
The syntax is `Assume [Positive]` Inductive/CoInductive/Record…`. The square brackets are used to delimit what is actually a list, so that other such flags can be passed in the future (universes, guard condition…).
|
|
Makes sure not to generate inductive schemes of assumed positive types.
|
|
The request for positivity to be assumed is honored.
|
|
The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
|
|
positivity is assumed.
|
|
I wasn't very creative: I just added a single test by failure case in the positivity checker (plus one success).
There should probably be tests with mutually inductives and co-inductives as well.
|
|
May still be wrong on Windows, though.
|
|
|
|
We lambda-lift by hand the graph traversal functions in Univ to allocate
less closures.
|
|
|
|
Fixes bug 3936
This closes #73
|
|
|
|
This interface is promoted by the operf-macro tool
https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.
Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
but in a Coq-implementation-defined format that is not suitable
for across-programs comparison
(also an environment variable allows to profile Coq runs on any .v,
in an non-intrusive way)
Note to the Github Robot:
This closes #75
|
