Email Gateway (Aug 18 2022 at 15:57): Email Gateway (Aug 18 2022 at 15:57):From: "Jeffrey Smith (Faculty)" <smith_jeffrey@dwc.edu>
I am an Isabelle, first time, "almost user". I say almost because I can't get past step one. I get the same error that someone else also reported, which was,
Missing Proof General Installation (PROOFGENERAL_HOME)
The solution to this problem was reported to look at the system manual. This was not enough of a clue for me. The system manual says to "set PROOFGENERAL_HOME to $ISABELLE_HOME/contrib/ProofGeneral (I have directories ProofGen.1 and ProofGeneral-3.7.1.1 under $ISABELLE_HOME/contrib but not ProofGeneral)" no matter was I set PROOFGENERAL_HOME to I get the same error.
I need to get very specific. I need to know what to change to what to get this to work rather than just look at the system manual.
I am trying to do the install under cygwin, running on Linux. I installed all the cygwin packages recommended on the isabelle site.
ISABELLE_HOME is at /usr/local/Isabelle2009-2
Thanks in advance for your help.
Email Gateway (Aug 18 2022 at 15:57):From: Alexander Krauss <krauss@in.tum.de>
Dear Jeffrey,
I am an Isabelle, first time, "almost user". I say almost because I
can't get past step one. I get the same error that someone else also
reported, which was, Missing Proof General Installation
(PROOFGENERAL_HOME)
This error is reported when the setting PROOFGENERAL_HOME is not present
and Proof General was not found in its standard places.
The solution to this problem was reported to look at the system
manual. This was not enough of a clue for me. The system manual says
to "set PROOFGENERAL_HOME to $ISABELLE_HOME/contrib/ProofGeneral (I
have directories ProofGen.1 and ProofGeneral-3.7.1.1 under
$ISABELLE_HOME/contrib but not ProofGeneral)" no matter was I set
PROOFGENERAL_HOME to I get the same error.
Instead of "ProofGen.1" there should normally be a symlink named
"ProofGeneral" which points to "ProofGeneral-3.7.1.1".
Did you use cygwin's tar/gzip for unpacking the tarball, as pointed out
on the download page? This is most likely the source of the problem.
Setting PROOFGENERAL_HOME manually to some location is possible, but
should not be necessary with the prepackaged bundle. You can check if
the setting is present by runnning
isabelle getenv PROOFGENERAL_HOME
I need to get very specific. I need to know what to change to what to
get this to work rather than just look at the system manual.I am trying to do the install under cygwin, running on Linux.
??? So what is it? Cygwin (i.e., Windows + Unixoid additions) or Linux?
Alex
Email Gateway (Aug 18 2022 at 15:57):From: Makarius <makarius@sketis.net>
The above looks like a casualty caused by some Windows tool for unpacking
the Isabelle .tar.gz --- ProofGeneral should be a symlink to
ProofGeneral-3.7.1.1 according to the Cygwin interpretation of the file
space. Use tar from the Cygwin command line exclusively.
Makarius
Email Gateway (Aug 18 2022 at 15:58):From: Jeff Smith <smith_jeffrey@dwc.edu>
thank you both
Last updated: Apr 19 2024 at 20:15 UTC