John Beattie (Dec 20 2023 at 12:58): John Beattie (Dec 20 2023 at 12:58):Hi,
Is prooftree (https://askra.de/software/prooftree/) still supported by proof general for coq?
When prooftree is turned on and I request the next step in the script, coqtop goes into a tight loop. The current proof step is highlighted to show action but it never completes. I get this emacs error in Messages:
error in process filter: Symbol’s value as variable is void: proof-info
There is no error nor any new output in the proof-tree window.
My setup is linux Mint 21; coq 8.17.1, installed via opam; proofgeneral 4.5 installed via ELPA.
I added prooftree by building it from https://askra.de/software/prooftree/releases/prooftree-0.13.tar.gz.
The build appears to be successful. I can run prooftree from the commandline and I can see its options window and its man pages.
I had a look in the proof general code for the proof-info symbol. I found it and the coq-specific function which populates it but have made no further progress.
I guess the basic question is whether prooftree is supported and the follow-up would be what to investigate or to change.
Thanks for any help.
John Beattie
Pierre Courtieu (Dec 21 2023 at 10:14):Hi. @Hendrik Tews can you say if @John Beattie should fill a bug report please?
Hendrik Tews (Dec 22 2023 at 22:46):Hi,
prooftree 0.13 and the current support in Proof General are for Coq 8.5 and 8.6. Please don't try try this. For Coq >=8.11 please use the head of https://github.com/hendriktews/proof-tree/ together with the prooftree update patches at https://github.com/ProofGeneral/PG/pull/439 or at https://github.com/hendriktews/PG/tree/prooftree-updates . This works for me with 8.16 and 8.17. I apologize for not keeping prooftree up-to-date, but nobody was interested in it for decades!
If you have questions, please ask! Preferably via email or github issues.
John Beattie (Dec 23 2023 at 16:07):Thanks for the responses.
Is there some other standard way to generate proof trees? It does seem like a useful feature.
Notification Bot (Dec 23 2023 at 22:02):Hendrik Tews has marked this topic as unresolved.
Hendrik Tews (Dec 23 2023 at 22:08):Unresolve, because I have a comment: There is no standard way to generate proof trees, because it depends on what you want. prooftree aims to support interactive proof development. Other tools aim, eg., at post-processing proofs for better human understanding. See "The Coq Proof Script Visualiser (coq-psv)" by Mario Frank (https://www.uni-potsdam.de/de/thi/mitarbeiter/frank) for some links.
Last updated: Oct 13 2024 at 01:02 UTC