Email Gateway (Aug 18 2022 at 13:54): Email Gateway (Aug 18 2022 at 13:54):From: Temesghen Kahsai <csteme@swansea.ac.uk>
Hi all,
I am using Isabelle2009 and ProofGeneral version 4.0pre090526.
On the command line (Isabelle findlogics) I can find all my heaps;
however when I try to select the logic from the emacs (Isabelle ->
Logics) I don't find my logics. Any clue why this is happening?
I attached a screenshot of what I see when I try to select a logic.
Cheers,
Teme
Picture 4.png
Email Gateway (Aug 18 2022 at 13:55):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Hi Teme,
I have no solution, but the "isabelle findlogics" command called by
ProofGeneral seems to return:
| Unknown logic "findlogics"
| no heap file found in:
| /Users/Teme/.isabelle/heaps/Isabelle2009/...
| /usr/local/Isabelle2009/...
Which is strange as the paths are Isabelle2009, but the called
"isabelle" executable seems to be of an older version. Is there an older
version of Isabelle installed which is executed by ProofGeneral?
Besides, are you sure the "Isabelle"-command calls the Isabelle 2009
version? Here the command should be all lower-case "isabelle", but this
could be accepted by the HFS-filesystem in Mac OS X.
Hope this helps,
Johannes
Email Gateway (Aug 18 2022 at 13:55):From: Makarius <makarius@sketis.net>
David Aspinall has produced a new snapshot now, which is available from
http://proofgeneral.inf.ed.ac.uk/devel
If there are any further problems, the Proof General tracker will absorb
them, see http://proofgeneral.inf.ed.ac.uk/trac/
Makarius
Last updated: May 03 2024 at 08:18 UTC