| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When a proof is 're-opened', the Qed node does not change.
Still the STM has to install the old state (where only
the future proof has to be updated). This bit was missing.
Why was it working: the bug happens only if you
reopen the very last proof, i.e. there is no
sentence that stays valid after the Qed. If there
is such a sentence, its state was computed correctly
before, and is not changed. If it is the very last,
then the next state is based on the wrong one...
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
I think that a better place for the mutex would be the printing routine,
but I still hope we will get rid of threads in favor of coroutines.
So I keep all mutexes in Stm.
|
| |\ \
| |/
|/| |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
There was an "optimization", since Abort is an empty side effect.
But that optimization had an impact on the DAG shape.
Now a nested proof, no matter if it is kept or dropped, is handled the same.
|
| | |
| |
| |
| | |
Suggested by @ppedrot
|
| |/
|
|
|
|
|
| |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| |
|
|
|
|
|
|
|
|
| |
The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.
We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.
Lightly tested.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.
`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.
`par: abstract tac` runs abstract on the generated proof terms. Nested
abstract calls are not supported.
|
| |\
| |
| |
| | |
Add -o option to coqc
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Since this is really what they are.
Squashing this renaming back to the root of the feature branch is hard.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
By default we enable only {} and par: that are detectable in
a complete way.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Advantage: 0 cost if no error occurs
Disadvantage: a box *must* end with the error absorbing command
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
|
| | | | |
| | | |
| | | |
| | | | |
This paves the way to detecting error boundaries via indentation
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Dag extended to support arbitrary clusters, renamed to Property.
Vcs generalized to not impose the data hold by a Property.
Stm(VCS) names a property "a box" and imposes a topological invariant (no
overlap). It defines 2 kind of boxes: ProofTasks (the old cluster
notion) and ErrorBound (meant to confine errors to sub-proofs).
In the meanwhile more equations added to Make(..) functors in order to
have just one Stateid.Set module around.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
A state in the cache (document node) is now one of "Empty | Error | Valid".
This paves the way to commands/blocks-of-commands resilient-to/confining
errors: one can catch and "ignore" the exception obtained by reaching the
previous state and do something sensible, like running anyway the command
or skipping until the end of an error-confining block is reached.
Invalid states carry an enriched exception with the safe_id attached, so
that if one edits_at or observe them gets a safe place to land (CoqIDE
needs such piece of info).
Little API change in Stm.state_of_id now returning a `Error variant for
the new kind of state.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Serialization should be specific to each particular backend, so we let
the Stm clients choose how the send the nodes.
This should be quite safe to pull in. Test suite passes.
Related to #180
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The command line option is named:
- async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.
Example: b.v depending on a.v
coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo
coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
|
| |
|
|
|
|
|
| |
The "Classic" string is still hard coded here in there in the system, but
not in STM.
BTW, the use of an hard coded "Classic" value suggests nobody really uses
"Set Default Proof Mode" in .v files.
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
Patch by Matthieu, Enrico and myself.
|
| |\| |
|
| | |
| |
| |
| |
| | |
computed when not in debugging mode (especially those printing a
command).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
|
| | |
| |
| |
| |
| |
| | |
Instead of mangling the AST in order to interpret par: we remember the goal
position to focus on it first and evaluate then the underlying vernacular
expression.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Print and Extraction commands may pierce opacity: if the
task producing the proof term is not finished, we wait for
its completion.
In -quick mode no worker is going to process a task, since tasks
are simply stored to disk (and resumed later in -vio2vo mode).
This commit avoids coqc waits forever for a task in order to
Print/Extract the corresponding term. Bug reported privately
by Alec Faithfull.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
"Instance name : Type." is like "Lemma name : Type", i.e. it starts
a proof. Unfortunately sometimes it does not, so we say VtUnknown.
Still, if there is an open proof, we classify it as a regular Lemma,
i.e. the opacity depends only on the terminator.
This makes CoqIDE and PIDE based UI way more responsive when processing
files containing Instance that are proved by tactics, since they are now
correctly delegated to workers. Bug reported privately by Alec Faithfull.
|
| |\ \ |
|
| |\ \ \
| | |/
| |/| |
|
Pierre-Marie Pédrot
Enrico Tassi
Emilio Jesus Gallego Arias
Pierre Letouzey
Maxime Dénès
Hugo Herbelin
Matej Kosik