| Age | Commit message (Collapse) | Author |
|---|
|
These dependencies between files can be used by UIs to guide compilation
and reloading of files.
FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
|
|
|
|
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
|
|
|
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
|
|
- Optimize the removal of generalization when there is no dependency in
the generalized variable (see postprocess_dependencies, and the removal
of dependencies in the default type of impossible cases).
- Compute the onlydflt flag correctly (what allows automatic treatment
of impossible cases even when there is no clause at all).
|
|
The leafs of the XML trees are still pretty-printed strings, but this
could be refined later on.
|
|
|
|
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
|
|
|
|
|
|
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/
|
|
|
|
|
|
|
