Email Gateway (Aug 19 2022 at 15:50): Email Gateway (Aug 19 2022 at 15:50):From: Makarius <makarius@sketis.net>
That is subsumed by "its traditional helper scripts". If you initialize
the mentioned "ProofGeneral-4.2-2" component in a standard way, it will
work out of the box.
Makarius
Email Gateway (Aug 19 2022 at 16:06):From: Ian Zimmerman <itz@buug.org>
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 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.
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.
But:
$ /opt/Isabelle2014/bin/isabelle
Usage: isabelle NAME [ARGS ...]
Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
Available tools:
browser - Isabelle graph browser
build - build and manage Isabelle sessions
codegen - issue code generation from shell
components - resolve Isabelle components
console - run Isabelle process with raw ML console and line editor
display - display document (in DVI or PDF format)
doc - view Isabelle documentation
document - prepare theory session document
env - run a program in a modified environment
getenv - get values from Isabelle settings environment
haskabelle - Haskabelle interface wrapper
install - install standalone Isabelle executables
java - invoke Java within the Isabelle environment
jedit - Isabelle/jEdit interface wrapper
keywords - generate keyword files for Emacs Proof General
latex - run LaTeX (and related tools)
logo - create an instance of the Isabelle logo
mirabelle - testing tool for automated proof tools
mkroot - prepare session root directory
mutabelle - mutant-testing for counterexample generators and automated tools
options - print Isabelle system options
scala - invoke Scala within the Isabelle environment
scalac - invoke Scala compiler within the Isabelle environment
tptp_graph - TPTP visualisation utility
tptp_isabelle - Isabelle tactics for TPTP competitive division
tptp_isabelle_hot - Isabelle tactics for TPTP demo division
tptp_nitpick - Nitpick for TPTP
tptp_refute - Refute for TPTP
tptp_sledgehammer - Sledgehammer for TPTP
tptp_translate - translate between TPTP formats
update_sub_sup - update Isabelle symbols involving sub/superscripts
version - display Isabelle version
yxml - simple XML to YXML converter
... no obvious way to start PG.
So, is this a miscommunication between the 2 projects, missing
documentation, or has PG interface simply been dropped altogether?
Email Gateway (Aug 19 2022 at 16:07):From: Makarius <makarius@sketis.net>
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".
Makarius
Email Gateway (Aug 19 2022 at 16:07):From: Ian Zimmerman <itz@buug.org>
Makarius <makarius@...> writes:
Makarius> How about actually reading the "system" manual concerning
Makarius> Isabelle components?
I had done so. I wouldn't presume to post here without doing so.
I should have mentioned this, sorry.
I added the unzipped PG location to the $ISABELLE_HOME/etc/components
file, as the system manual directed me. It didn't change anything.
Makarius> Alternatively, you can get some additional explanations on the
Makarius> parallel thread "Isabelle 2014 and proof general".
Makarius> I now regret that I made Proof General optional in
Makarius> Isabelle2014. It should have been deleted outright, without
Makarius> further comments.
Makarius> Nonetheless, there is always the possibility to put genuine
Makarius> reasons for remaining uses of Proof General on the table for
Makarius> discussion, but excluding anything that is isomorphic to "I
Makarius> don't want to change my habits".
I have read that thread now, thanks. I disagree with most of what you
say there, but I can see there's no changing your position, so I will
resist the urge to jump in.
Email Gateway (Aug 19 2022 at 16:07):From: Makarius <makarius@sketis.net>
This strange game around Proof General is already quite old. De-facto, I
am the only one who ever invested serious work in its Isabelle
connectivity, and there were many calls to action to continue that by
someone else after the start of PIDE in 2007/2008. Nothing has ever
happened, though. Proof General users are characterised by inactivity.
To disprove that, are you willing to do anything yourself? Today it would
mean doing a few reforms in the Emacs LISP implementation to work directly
with Isabelle process protocol functions, not the obsolete Isar TTY
toplevel anymore.
If there are no hard facts showing up to continue classic Proof General
Isabelle support one more season, it will be removed without further ado
in the next Isabelle release.
Makarius
Email Gateway (Aug 19 2022 at 16:07):From: Ian Zimmerman <itz@buug.org>
Makarius <makarius@...> writes:
Ian> I have read that thread now, thanks. I disagree with most of what
Ian> you say there, but I can see there's no changing your position, so
Ian> I will resist the urge to jump in.
Makarius> This strange game around Proof General is already quite old.
Makarius> De-facto, I am the only one who ever invested serious work in
Makarius> its Isabelle connectivity, and there were many calls to action
Makarius> to continue that by someone else after the start of PIDE in
Makarius> 2007/2008. Nothing has ever happened, though. Proof General
Makarius> users are characterised by inactivity.
I think what happened is that David A., the main PG developer, had a
conversion similar to yours (but in his case to eclipse rather than jedit).
Makarius> To disprove that, are you willing to do anything yourself?
Makarius> Today it would mean doing a few reforms in the Emacs LISP
Makarius> implementation to work directly with Isabelle process protocol
Makarius> functions, not the obsolete Isar TTY toplevel anymore.
I hope the "today" is not literal, but soon, Yes. I am here to help.
Makarius> If there are no hard facts showing up to continue classic
Makarius> Proof General Isabelle support one more season, it will be
Makarius> removed without further ado in the next Isabelle release.
By "classic" do you mean "TTY"? So if the new work is successful PG
lives on? Deal. I have a reservation, though: will this fundamentally
change the feel of Isabelle/PG? For instance, will it now start working
magically in the background instead of synchronously?
Now to return to my immediate problem, after I register the PG
component, do I still need the "emacs" script? I think this might be
the case from reading the other thread. If yes this would be a handy
bit of information to put in the NEWS file.
Email Gateway (Aug 19 2022 at 16:07):From: Makarius <makarius@sketis.net>
On Sat, 13 Sep 2014, Ian Zimmerman wrote:
Makarius> To disprove that, are you willing to do anything yourself?
Makarius> Today it would mean doing a few reforms in the Emacs LISP
Makarius> implementation to work directly with Isabelle process protocol
Makarius> functions, not the obsolete Isar TTY toplevel anymore.I hope the "today" is not literal, but soon, Yes. I am here to help.
Makarius> If there are no hard facts showing up to continue classic
Makarius> Proof General Isabelle support one more season, it will be
Makarius> removed without further ado in the next Isabelle release.By "classic" do you mean "TTY"?
Classic means the current "optional" Proof General component with its use
of the obsolete TTY loop. That is in the way for a long time, and it is
about to disappear soon.
So if the new work is successful PG lives on? Deal.
I am not even required in that deal.
The regular Isabelle process interface provides official ways to define
protocol functions, and thus implement front-ends in user-space without
the old TTY loop. Thus it should be relatively easy to re-implement old
PG interaction, although the relative weak Emacs LISP infrastructure might
require some tricks to make it work.
Anything else should be discussed on the proofgeneral-devel@inf.ed.ac.uk
For instance, will it now start working magically in the background
instead of synchronously?
It depends how this is done. Nothing of that is hard-wired into Isabelle.
Old-fashioned synchronous interaction can be implemented independently of
the PIDE interaction model.
Now to return to my immediate problem, after I register the PG
component, do I still need the "emacs" script? I think this might be
the case from reading the other thread. If yes this would be a handy
bit of information to put in the NEWS file.
The NEWS file provides all relevant entry points. On the other thread,
Lars Noschinski also provided concrete examples how to apply that
information in practice.
Isabelle components are well-documented, although this knowledge is not
required by default for regular Isabelle releases. In Isabelle2014 the
defaults have been changed such that Proof General users have to stand up
and do some tiny bit of work by themselves, just as a symbolic gesture.
Makarius
Email Gateway (Aug 19 2022 at 16:08):From: Makarius <makarius@sketis.net>
I don't think that "conversion" is the right word.
When we did Proof General many years ago, we were quite realistic about
the side-conditions that Emacs would impose on the project. There was
never the idea that Emacs would be the best editor ever, so that it had to
be used without question. Rather, there was no alternative: Emacs was the
only major editor at that time with arbitrary extensibility.
So we knew already about the inherent limitations, and moving forwards was
nothing revolutionary.
That is all long past ...
Makarius
Email Gateway (Aug 19 2022 at 16:08):From: Ian Zimmerman <itz@buug.org>
Makarius <makarius@...> writes:
Makarius> The NEWS file provides all relevant entry points.
I am sorry, but this is simply not true. The crucial fact that the
necessary script $ISABELLE_HOME/lib/Tools/emacs has been removed is not
mentioned.
Thanks for your other information, it will be very helpful if / when I
try to do the PG overhaul. I understand now that you don't want to be
involved in any way, and I respect your reasons.
Last updated: Apr 24 2024 at 01:07 UTC