[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general eb468a9f8f 08/11: user doc, CHANGES: update
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general eb468a9f8f 08/11: user doc, CHANGES: update for prooftree |
Date: |
Fri, 23 Feb 2024 10:01:24 -0500 (EST) |
branch: elpa/proof-general
commit eb468a9f8f0b537afffbff4bee33d4479091e91d
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>
user doc, CHANGES: update for prooftree
---
CHANGES | 11 +++++++++--
doc/ProofGeneral.texi | 14 ++++++++------
2 files changed, 17 insertions(+), 8 deletions(-)
diff --git a/CHANGES b/CHANGES
index b84ed46067..1e29c5542e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,15 +8,22 @@ the Git ChangeLog, the GitHub repo
https://github.com/ProofGeneral/PG
** Generic changes
*** Improve the omit-proofs feature to handle a number of cases where
proofs must not be omitted.
+*** Renew support for proof-tree visualization via the external command
+ prooftree, see http://askra.de/software/prooftree and Section 7
+ "Graphical Proof-Tree Visualization" in the Proof General manual.
+ Proof-tree visualization is currently only supported for Coq. The
+ prooftree support has been substantially rewritten, making use of
+ the much better support since Coq version 8.11.
** Coq changes
-
*** support Coq 8.19
-
**** New option coq-compile-coqdep-warnings to configure the warning
command line argument (-w) of coqdep. The default of this option
is +module-not-found to let Proof General reliably detect missing
modules as coqdep error.
+*** Renew support for proof-tree visualization, see description in
+ generic changes above.
+
**** Fix issues #687 and #688 where the omit-proofs feature causes
errors on correct code.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 6ddf7638ae..c0158d63c1 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3172,12 +3172,14 @@ Query the prover about the identifier near mouse click
@var{event}.
@chapter Graphical Proof-Tree Visualization
@cindex proof-tree visualization
-Since version 4.2, Proof General supports proof-tree
+Since version 4.5, Proof General (again) supports proof-tree
visualization on graphical desktops via the additional program
-Prooftree. Currently, proof-tree visualization is only supported
-for the Coq proof assistant.
+Prooftree. Currently, proof-tree visualization is only supported for
+the Coq proof assistant. (Proof-tree visualization was already
+supported in version 4.2 but then discontinued in 2017 when Coq 8.7
+dropped the variant of @code{Show Goal} that prooftree relied on.)
-This version of Proof General requires Prooftree version 0.11.
+This version of Proof General requires Prooftree version 0.14.
Check the @uref{http://askra.de/software/prooftree/, Prooftree website},
to see if some later versions are also compatible. (Because of
the communication protocol, Proof General is always only
@@ -5349,8 +5351,8 @@ you want to save abbrevs; answer yes.
@section Proof-Tree Visualization
@cindex Proof-Tree visualization
-Starting with Proof General version 4.2 and Coq version 8.4, Coq
-Proof General has full support for proof-tree visualization,
+Starting with Proof General version 4.5 and Coq version 8.11, Coq
+Proof General has (again) full support for proof-tree visualization,
@pxref{Graphical Proof-Tree Visualization}. To find out which
versions of Prooftree are compatible with this version of Proof
General, @pxref{Graphical Proof-Tree Visualization} or the
- [nongnu] elpa/proof-general updated (4814efb366 -> 1f0724813a), ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 7aaca43e29 05/11: prooftree: wait for show-goal commands at proof end, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 5fbc5d3030 09/11: prooftree: fix single step undo, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 1f0724813a 11/11: proof-tree: protect against internal errors, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 1dc76dbb65 02/11: prooftree: complete evar info, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 5b10c7e1ea 04/11: prooftree: fix spurious undo recognition for show goal, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 0615eecc88 06/11: PG-adapting: delete some outdated prooftree information, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general b95c2087e9 03/11: prooftree: simplify evar printing management, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general b96927ed0f 10/11: prooftree: fix Unshelve and delete new layer recognition, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general eb468a9f8f 08/11: user doc, CHANGES: update for prooftree,
ELPA Syncer <=
- [nongnu] elpa/proof-general cef4d1cf12 07/11: prooftree: polish, ELPA Syncer, 2024/02/23
- [nongnu] elpa/proof-general 25c2d37376 01/11: prooftree: Update proof tree display support for Coq 8.10, ELPA Syncer, 2024/02/23