Re: [isabelle] Had a problem for last 2 weeks that have kept me from running isabelle



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.