| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.
With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.
To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.
|
|
Closes GH-557.
|
|
Backported those typos that were fixed only in the manual texi
sources and not in the doc strings, from which the text was
imported. Convert a few symbols quoted with curved unicode single
quotations to ascii, such that make magic recognizes them.
|
|
proof-state-change-pre-hook happens earlier than
proof-state-change-hook, i.e. before proof-done-advancing. This should
be used to register information in the currently processed span before
proof-done-advancing classifies it.
Historically PG design was to gather these information during
proof-done-advancing (or in its hook called at the end) by just
looking at the command statement. But it is often useful to look at
the output (messages and/or prompt) to gather more accurate
information. Some of this information may be needed DURING
proof-done-advancing. Hence this early hook.
|
|
|
|
|
|
|
|
This variable was still not used anywhere, but will soon.
|
|
Prover specific analyzis of the last prompt/output to determine if
there are open goals left.
|
|
|
|
I ended up using (in a slight devious way) the lemma dependency
mechanism of PG: the dependency information stored in the span is only
the ones suggested by coq: only the one that should appear in theproof
using annotation (and only when coq felt the need to suggest them.
|
|
This patch allows one to load the `coq-diffs' option at Coq startup,
provided the ambient Coq version is >= 8.10.
This additional "lambda" format is needed because [Set Diffs "on".] is neither:
- a boolean setting from Coq side (there are three possible values)
- a string setting from Emacs side (it is implemented as a radio/symbol option)
- a cross-version compatible Coq setting.
|
|
|
|
|
|
|
|
|
|
|
|
This hook was missing, it allows to send complete commands before
the (set of) command(s) sent by the user. It shall be used when
proof-shell-insert-hook cannot be used (because of multiple prompts
appearing).
|
|
Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of
= 24).
|
|
|
|
Added an option about that in proof-config.
To check: I adapted proof-treee regrexp accordingly.
|
|
coq-par-compile.el (must be activated via
coq-compile-parallel-in-background)
- items in the queue region are not necessarily in
proof-action-list any more! Require commands and the following
items are stored elsewhere until the compilation finishes.
Variable proof-second-action-list-active notifies the generic
machinery if queue items are stored elsewhere. In this case,
Proof General must neither release the proof shell lock nor
delete the queue span when proof-action-list is empty.
- to kill background processes as early as possible, the new hook
proof-shell-signal-interrupt-hook is used
|
|
to avoid Trac #453: http://proofgeneral.inf.ed.ac.uk/trac/ticket/453
|
|
ignored junk (val it : goalstack =).
|
|
at *start* of proof-shell-start-goals-regexp.
|
|
- add support for proof-tree displays (currently Coq only)
- new file generic/proof-tree.el contains generic code
- Coq specific code has been added to coq/coq.el
Changes to existing Proof General functions:
- proof-shell-exec-loop and proof-shell-filter-manage-output call
proof-tree display functions, when the proof-tree display is on
- proof-shell-exec-loop returns t if proof-action-list is empty
_or_ contains only items for updating the proof-tree
- proof-shell-should-be-silent returns nil when the proof-tree
display is on
- coq-last-prompt-info, coq-last-prompt-info-safe return as
additional 4th element the name of the current proof
|
|
|
|
expected, see Trac #430
|
|
argument and allow nil setting for proof-shell-start-goals-regexp.
|
|
proof-shell-require-command-regexp
- TAGS updated to really flush them
|
|
|
|
45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384.
|
|
|
|
|
|
- add documentation for it
- add a test case demonstrating it in
coq/ex/test-cases/retract-completely-asserted
|
|
The following points are implemented already:
- recompile either via an external command (make) or let
ProofGeneral handle everything internally
- complete dependency tracking and recompilation for coq files in
internal mode
- support for extending the LoadPath: does almost work, even if
specified file-locally
- move back to clean state if recompilation fails
There are the following known problems:
- coq-load-path extensions are not retracted
- fails on partially qualified library names
|
|
|
|
|
|
|
|
|
|
of t (for safety, no ill behaviour observed)
|
|
about Solaris. Experiment using pipe instead of pty communication as
default now scomint buffer not intended for interactive input and runs
prover process directly.
|
|
proof-shell-interrupts-after-commit.
|
|
[experimental/temporary].
|
|
|
|
|
|
|
|
*fast* machine;
|
|
|
