| Age | Commit message (Collapse) | Author |
|---|
|
This is likely to make nested proofs containing proof modes switch
broken, but fixes the problems Arnaud has in his branch.
It is possible that the classification function we have today
is not fine grained enough.
If a command that changes the proof mode has as the only global
effect changing the proof mode, then the current code is fine.
If it has a more global effect that persists after the proof is over
but has no impact on the proof itself, then the old code is fine.
As far as I can get, the proof mode switching commands have
a global effect (changing parser) but also a proof effect
(un/focusing). We don't have a classification for these.
Today a command having a global effect is played twice:
on the proof branch an on master. Of course if such command
cannot work on master (where there is no finished proof for
example) we need a special treatment for it.
|
|
|
|
It was detecting only the per-lemma Polymorphic flag,
but not the global one.
|
|
|
|
|
|
In PG there are shortcuts that perform on the fly "Set Printing
All"/"Unset Printing All" in pg. For example if you type C-u before
some shortcut for print (check/About/Show), it performs:
Set Printing All.
Print foo.
Unset Printing All.
But if the "Unset" prints a goal, then pg interprets the output of
Print as a command applied on a previous line, and thus hides it.
So for emacs mode I would prefer no goal printing when options are
set/unset. In the situation where this should be done (when setting
durably the option probably), I'd rather program a "Show" explicitely.
|
|
|
|
As happens in interactive mode.
|
|
When lauching ideslave without configuring the communication channels,
instead of raising an anomaly which is never caught by the main loop, we
rather exit the process with a relevant error message.
|
|
|
|
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
|
|
|
Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
|
|
|
|
This change fixes performance problems in PIDE based user interfaces
|
|
|
|
Only tactics are taken into account.
|
|
|
|
Of course such proofs cannot be processed asynchronously
|
|
Probably a regression introduced in some code refactoring.
Affects only PIDE based code.
|
|
coqtop mode.
|
|
|
|
|
|
Here nonsensical means a Qed/Defined without a Lemma.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Before this commit the worker was sending back a proof term
as built by tactics. The master receives the proof terms and
eventually (when one clicks on the gears in CoqIDE) check it
with the kernel. This meant that errors like the ones produced
by the "fix" tactics were discovered very late.
Now a worker checks with its kernel the proof term before sending it
back. The term is also checked by the master, eventually, but the
error is signaled early.
|
|
|
|
|
|
|
|
|
|
removing the need of thread creation in the interface.
|
|
|
|
|
|
|
|
|
|
This commits makes the concept of delegated and async more orthogonal.
A proof can be async but not delegated to a worker (if it is known
to be very small it is too much overhead to delegate to a worker).
A proof that is not async cannot be delegated to a worker.
An async proof that contains an error does not prevent Coq from continuing
the execution (interactive mode) and can be fixed without invalidating
the whole document (CoqIDE knows how to do that) even if it is processed
locally. It used to be the case only for delegated proofs, now it worker
for all the proofs that can be in principle delegated (doing it or not
is an implementation detail, an optimization).
|
|
|
|
|
|
Thanks the the previous patchset a worker can be asked to send
back "light" version of the system states. This is reasonably
efficient hence the idea of letting a worker hang around just to
hold system states for retrieval on demand is dropped.
|
|
|
|
|
|
|
|
|
|
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
