Re: [isabelle] Isabelle2014 and ProofGeneral

On Fri, 12 Sep 2014, Ian Zimmerman wrote:

Can Isabelle2014 work with ProofGeneral at all?  The NEWS file says:

Proof General with its traditional helper scripts is now an optional
Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle
component repository  Note that
the "system" manual provides general explanations about add-on
components, especially those that are not bundled with the release.

So I unpacked the PG tarball.  Within it is the directory isar and files
isar/interface and isar/README.  And the latter says:

The script `interface' and file 'interface-setup.el' are used
internally to start Isabelle Proof General via the 'isabelle' shell
command.  This is the default way to invoke Proof General from the
Isabelle perspective; it enables Isabelle to provide a consistent
process and file-system environment, including the all-important
isar-keywords.el file.

How about actually reading the "system" manual concerning Isabelle components?

Alternatively, you can get some additional explanations on the parallel thread "Isabelle 2014 and proof general".

I now regret that I made Proof General optional in Isabelle2014. It should have been deleted outright, without further comments.

Nonetheless, there is always the possibility to put genuine reasons for remaining uses of Proof General on the table for discussion, but excluding anything that is isomorphic to "I don't want to change my habits".


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