| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Command line options to be dropped got outdated after vi -> vio renaming.
This made the par: goal selector do not work in conjunction with -quick.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Return the most appropriate evar_map for commands that can run on
non-focused proofs (like Check, Show and debug printers) so that
universes and existentials are printed correctly (they are global
to the proof). The API is backwards compatible.
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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!
|
| |\ \ \
| | | |
| | | |
| | | | |
into JasonGross-trunk-function_scope
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | | |
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The SIGINT sent to the master coqtop process was lost in a watchdog thread,
so that the STM resulted in an inconsistent state. This patch catches gracefully
the exception and kills the task as if it were normally cancelled. Note that
it probably won't work on non-POSIX architectures, but it does not really
matter because interrupt was already badly handled anyway.
|
| | | | | |
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | | |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
It used not to be the case when the proof contains Sideff, since
the code was picking the last known state and not necessarily the
first one. Because of side effects the last known state could be
the one corresponding to the side effect (that was executed to, say,
change the parser). This is also related to bug #4530
|
| | | | | | |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Originally, rel-context was represented as:
Context.rel_context = Names.Name.t * Constr.t option * Constr.t
Now it is represented as:
Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
| LocalDef of Names.Name.t * Constr.t * Constr.t
Originally, named-context was represented as:
Context.named_context = Names.Id.t * Constr.t option * Constr.t
Now it is represented as:
Context.Named.t = LocalAssum of Names.Id.t * Constr.t
| LocalDef of Names.Id.t * Constr.t * Constr.t
Motivation:
(1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
function which looked like this:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
Suppose that you do not know about rel-context and named-context.
(that is the case of people who just started to read the source code)
Merlin would tell you that the type of the value you are destructing
by "match" is:
'a * 'b option * Constr.t (* worst-case scenario *)
or
Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *)
To me, this is akin to wearing an opaque veil.
It is hard to figure out the meaning of the values you are looking at.
In particular, it is hard to discover the connection between the value
we are destructing above and the datatypes and functions defined
in the "kernel/context.ml" file.
In this case, the connection is there, but it is not visible
(between the function above and the "Context" module).
------------------------------------------------------------------------
Now consider, what happens when the reader see the same function
presented in the following form:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
to jump to the corresponding definition and learn more.
In this case, the connection is there, and it is directly visible
(between the function above and the "Context" module).
(2) Also, if we already have the concepts such as:
- local declaration
- local assumption
- local definition
and we describe these notions meticulously in the Reference Manual,
then it is a real pity not to reinforce the connection
of the actual code with the abstract description we published.
|
| |\| | | |
|
Enrico Tassi
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Matej Kosik