search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 87 forks source link

Proof General with Isabelle 2005 #186

Open GergelyBuday opened 7 years ago

GergelyBuday commented 7 years ago

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?

cpitclaudel commented 7 years ago

Please explain what you mean "Proof General did not load.". (As a side note, we don't have anyone on the team actively using Isabelle, AFAICT — in part because Isabelle dropped Emacs support in Isabelle 2015)

cpitclaudel commented 7 years ago

Try running isar-mode explicitly after opening your file?