Hi,

would it be possible to run current Proof General with Isabelle 2005? 

Proof General documentation, section 

        12 Isabelle Proof General 

writes in the first paragraph:

--
Isabelle provides its own way to invoke Proof General via the isabelle
command. Running
isabelle emacs starts an Emacs session with Isabelle Proof General.
--

My Isabelle 2005 installation says

$ ./isabelle emacs
Unknown logic "emacs" -- no heap file found in:
  /home/gbuday/isabelle/heaps/polyml-5.6_x86-linux
 
/home/gbuday/prooftheory/Isabelle2005-for-PolyML-5.6/heaps/polyml-5.6_x86-li
nux

Is "isabelle emacs" a later-than-2005 feature of Isabelle?

I tried the other way around, starting emacs and opening an Isabelle theory
file. I have the following .emacs:

(load "~/.emacs.d/lisp/PG/generic/proof-site")
(setq isabelle-program-name-override
"/home/gbuday/prooftheory/Isabelle2005-for-PolyML-5.6/bin/isabelle")

and I did the PG installation according to 

https://proofgeneral.github.io/ Quick Installation

Proof General did not load.

What do you recommend to make it work?

Best 

- Gergely

_______________________________________________
ProofGeneral mailing list
ProofGeneral@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral

Reply via email to