| Age | Commit message (Collapse) | Author |
|---|
|
|
|
E.g.
Coq options are:
-I dir look for ML files in dir
-include dir (idem)
[...]
-h, --help print this list of options
With the flag '-toploop coqidetop' these extra option are also available:
--help-XML-protocol print the documentation of the XML protocol used by CoqIDE
|
|
|
|
The code for the module was moved from Tacinterp. We still expose partially
the implementation of the Ftactic.t type, for the sake of simplicity. It may
be dangerous if used improperly though.
|
|
|
|
|
|
Instead of having a version of unpackers for each level, we use a dummy argument
to force unification of types.
|
|
All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
|
|
|
|
|
|
The rationale for its use comes from OCaml weak maps, and is justified by the
fact that Weak.get may prevent its return value to be collected by the GC during
the next slice even though nobody points to it. In our case, this is vastly
irrelevant because hashconsed values are not expected to be collected whatsoever
(save for exceptional cases). But Weak.get_copy is rather costly actually, at
least strictly more than the plain Weak.get.
Experimentally, I observe diminution of compilation time and even diminution
of memory consumption (!) after this patch, so I assume it is a net gain.
|
|
For better efficiency, we try to preserve the shape of mutually recursive
trees.
|
|
|
|
|
|
This reverts commit 062d07eb5446c1032fda232b9a09e20e5410dd92.
|
|
Following Bruno's suggestion, we check if the tree expected for the recursive
argument is included in the one which is inferred. This check is probably
not necessary in the current state of affairs, but might become so after
further extensions of the guard condition.
|
|
|
|
instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.
|
|
|
|
|
|
|
|
|
|
backtracks, print time spent in each of successive calls.
|
|
|
|
|
|
This is useful if a UI does not support that
|
|
LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
|
|
|
|
|
|
These are now sufficient to implement PIDE
|
|
Experimenting with PIDE I discovered that yield is not sufficient
to have a rescheduling, hence the delay.
|
|
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
|
|
|
|
|
|
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
|
|
|
|
|
|
These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
|
|
by the printing options (i.e. when "Print Universes" is set).
|
|
the checker, and it was not used before that anyway.
|
|
|
|
This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.
|
|
|
|
|
|
|
|
|
|
|
