| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
parsing is plugged.
|
| | |
|
| |
|
|
|
|
| |
Serialize.ml spits out its own documentation. Not everything is
statically checked, so it risks to get outdated. Ideas on how
to statically/dynamically check that the doc is in sync are welcome.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
I chose n to be 10000 iterations. It might be big, but a slave, to check
for a termination request, has to pass the ball to the thread that
sends "regularly" Ticks to the master process. Thread.yield is a
system call, so we have to do it very rarely.
|
| |
|
|
|
|
|
|
| |
The code now passes a cleanup function that, if slave is not
killed, could be used to do some cleanup between two jobs.
ATM I don't know how to reuse the worker without having it
grow in space indefinitely. Running Gc.compact is too expensive.
|
| | |
|
| | |
|
| |
|
|
| |
provided tactic environment to handle open terms.
|
| |
|
|
|
|
|
|
| |
Since the new proof engine, Hiddentac has been essentially trivial.
Here is what happened to the functions defined there
- Aliases, or tactics that were trivial to inline were systematically inlined
- Tactics used only in tacinterp have been moved to tacinterp
- Other tactics have been moved to a new module Tactics.Simple.
|
| |
|
|
| |
In 0c7a77, I inadvertantly re-defined an is_section_variable function.
|
| |
|
|
|
|
| |
There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics.
I've changed some of them to explicitely take an environment and an evar_map instead.
|
| |
|
|
| |
Revealed by message on coq-club on 24/11/2013.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
Let's avoid the "if a=$(cmd ...)" since:
- unless being a shell expert, it's not obvious it's testing the exit code
of cmd.
- it's quite fragile, if you pipe cmd into a cmd2 you'll lose the
exit code of cmd.
Instead, we test the emptiness of the variable content afterwards
|
| | |
|
| |
|
|
|
|
|
|
| |
anomaly is raised. As there are very few tags defined in Coq code, this is
very unlikely to appear, and can be fixed by tweaking the name of the
dynamic argument.
This should be more efficient, as we did compare equal strings each time.
|
| |
|
|
|
|
|
| |
Keeping the earlier content of this variable is crucial for opam
(at least).
Thanks to François Bobot and Thomas Refis for this one...
|
| |
|
|
|
| |
- after piping with | tr -d, an exit code was lost
- suspicious use of " " inside a larger " ", we use ' ' now instead
|
| |
|
|
|
|
| |
Also add a 2 in an error message (it's gSourceView2, not gSourceView).
This closes bugs 3150, 3151, 3152, and 3153.
|
| | |
|
| | |
|
| |
|
|
| |
execution)
|
| |
|
|
| |
particular
|
| | |
|
| | |
|
| |
|
|
|
| |
In particular, this file allows to merge duplicated identities
of a same person. See man git shortlog for more details.
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17095 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17094 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17093 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Contrarily to my machine results, it seems that it tore down the performance of
Coq on benchmarks.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17091 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
multiple successes.
The semantics was a bit strange: an immediate failure of a branch would cause the pattern matching to backtrack, and failure after the match could cause the selected tactic to backtrack. However, the pattern matching process won't backtrack after it has selected a tactic with at least one success.
To avoid changing the semantics of pattern matching with single-success tactics, I made it so that it is impossible to backtrack into a pattern matching once done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17090 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
The implementation was partly based on IStream and partly on a control flow with exception. The latter does not mix well with the monadic tactics.
I've moved the algorithmic part of pattern-matching to a new file (tactics/tacticMatching.ml), in order to de-entangle the pattern-matching procedure from the interpretation. This shaves off 300 lines of code from Tacinterp, which is still over 2000 lines of code. It is a first step towards refactoring tacinterp. To be fair, part of what disapeared are lines which sent messages to the debugger. I was not too concerned with them because I understand people found the debugger much too fine-grain on Ltac's pattern matching. But conversely, there may be too few debugging hooks now. This is worth looking into.
In TacticMatching itself, I used a monadic style to express the pattern-matching procedure concisely. I implemented the monad in a fairly brute-force way, using the existing primitive of IStream. It may be worth experimenting with specialized primitive. I am less worried about the monadic style than about the number of allocation of list cells that the primitives entail.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17089 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
The comments were inaccurate after r16533.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
xclerc
Pierre-Marie Pédrot
Enrico Tassi
Arnaud Spiwack
Hugo Herbelin
Pierre Letouzey
Stephane Glondu
Jason Gross
Julien Forest
forest
letouzey
ppedrot
fbesson
aspiwack