Re: [isabelle] Isabelle 2014 and proof general



On Thu, 4 Sep 2014, Vadim Zaliva wrote:

I just installed Isabelle 2014 and started in a way I was starting previous version:

/Applications/Isabelle2014.app/Isabelle/bin/isabelle emacs -p /Applications/Aquamacs.app/Contents/MacOS/Aquamacs &

and I got the error:

Unknown Isabelle tool: emacs

Does it mean 2014 version is no longer support emacs/Proof General?

As a general principle, the Isabelle NEWS file is of prime importance to
document the "history of user-relevant changes". It is easily accessible
in many spots, including the main Isabelle web page. Isabelle/jEdit also
provides a minimal "IDE" to navigate the NEWS file with some tree
structure via SideKick, and hypersearch helps to find relevant keywords.

Users who want to be up-to-date wrt. the current state-of-the-art of
Isabelle should study the NEWS file whenever a new release comes out, to
see how things are done better in the new version, in contrast to old
ones. At least when there is some unexpected behaviour, the NEWS file
should be consulted for explanation. Doing that here yields:

  * 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 http://isabelle.in.tum.de/components/.  Note that
  the "system" manual provides general explanations about add-on
  components, especially those that are not bundled with the release.


I am old time Emacs User (20+ years) and for that reason I was preferring Proof General to JEdit.

See the "jedit" manual for the proper terminology of Isabelle/jEdit as
standard application of the PIDE (Prover IDE) framework. It does not
make any sense to make a parallel of "Proof General" vs. "jEdit": jEdit
is the underlying editor, so it would correspond to Emacs here. The name
of the integrated application is "Isabelle/jEdit", and that is just an
example of other Isabelle/PIDE applications, such as Isabelle/Eclipse or
Clide.

Apart from proper names an concepts, we are back to the canonical
question: Are there any remaining uses of Proof General?

Just being stuck out of habit over decades is no good reason. The word
"reason" is related "ratio" or "rational", but sticking blindly to
habits is rather irrational. This natural inertia has sucked up a lot of
resources over the years. It is better to spend resources now to figure
out how close we are to the final disposal of Isabelle Proof General --
after more than 5 years of Isabelle/PIDE development.

That is a serious topic, but some hard facts need to be put on the
table, not just "I don't want to change habits".


	Makarius




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