| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Makes sure not to generate inductive schemes of assumed positive types.
|
|
The first part only contains the summary of the library, while the second
one contains the effective content of it.
|
|
Hence we reuse the ones in master.
|
|
|
|
|
|
|
|
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
|
|
|
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
|
|
|
|
|
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
|
|
|
|
When a worker sends back a system state to master, it tries to
just send a delta. If the command is a simple tactic, then only
the proof state changes.
Now, what is a simple tactic?
1. a tactic
2. that does not change the environment
Check 1. was surely incomplete. Now it is:
VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _
Is it complete?
|
|
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.
|
|
|
|
|
|
|
|
|
