Email Gateway (Aug 19 2022 at 15:51): Email Gateway (Aug 19 2022 at 15:51):From: Thomas Sewell <thomas.sewell@nicta.com.au>
A week or two ago, Makarius asked us the canonical question:
"Are there any remaining uses of Proof General?"
I take it Makarius is inquiring whether there are any applications left
that require ProofGeneral as opposed to one of the PIDE implementations.
It happens that earlier in the year, I used ProofGeneral to do some
surgery on the "Fastpath" proof. This is the largest and worst of the
proofs about the C code of seL4. At the time I felt that Isabelle/jEdit
was unworkable for this task. I investigated this again today.
I'm now convinced I can do further surgery on this proof using only
PIDE, although the process is currently slower and more painful than
using ProofGeneral.
Those who are interested in pathological uses of Isabelle can find the
proof I'm talking about on github https://github.com/seL4/l4v and the
relevant file here
https://github.com/seL4/l4v/blob/master/proof/crefine/Fastpath_C.thy
although there may be difficulty in building the proof. We're thinking
about simplifying the build process in the future.
It is very important to set the goal print limit to 1. Otherwise too
much CPU is lost attempting to print goals, and Isabelle/jEdit gives at
least the impression that it has broken down entirely. Once the goals
limit is set to 1, Isabelle/jEdit succeeds in reporting on all points in
the proof eventually.
I also set the goals limit to 1 in ProofGeneral. This was easier,
firstly because there is a menu option, and secondly because watching
the "blue region" makes it clear how much time is lost on printing.
In Isabelle/jEdit I had to declare [[goals_limit = 1]] explicitly in the
text. Unfortunately this requires backing up to a sensible place. After
some thought I've added "using [[goals_limit = 1]]" permanently to the
two worst proof scripts.
Is there any particular reason why the goals limit isn't a setting that
can be adjusted from a panel or the options in Isabelle/jEdit?
I also tried the "parallel_print" setting which Makarius added when I
last brought this up. This does more or less the opposite of what I
want. However, like ProofGeneral's blue region, it makes it easy to see
the problem. After moving the cursor down rapidly, the window "greys
out" for a while, and then returns to white one line at a time as the
goal states print in order. This process might take a minute or so.
This explains why Isabelle/jEdit seems so slow in these cases: the goal
states render in order, while the user waits for output where their
cursor actually is. In the parallel case the window goes white
immediately once the print tasks have forked, from which point there is
no indication of progress, giving the impression the system has just
given up.
Ideally I'd like to see some approximation ProofGeneral's behaviour, in
which many commands can be processed and only one goal state rendered.
Yes, my proofs are pathological, full of applications of fast
methods/tactics but with large complex goal states. I suspect, however,
that I'm not alone.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 15:52):From: Carst Tankink <carst.tankink@inria.fr>
On 09/18/2014 12:25 PM, Thomas Sewell wrote:
This explains why Isabelle/jEdit seems so slow in these cases: the goal
states render in order, while the user waits for output where their
cursor actually is.
I find this a bit curious, as it is my understanding that PIDE's
"perspective" mechanism should actually deliver the output to the user's
cursor. From Makarius' UITP-2014 paper:
"Activation or deactivation of PRINT tasks is subject to the document
perspective. The whole theory library that is edited might be big, but
only small parts are visible in the editor. PIDE document processing
takes the open text windows as indication where to invest resources for
continuous processing."
The perspective not only tells the underlying process which windows is
open, but also what command spans ('lines') are in view, and in our Coq
incarnation of PIDE, we use this fact: each individual proof is handled
by a separate worker process, and the proofs that are in the perspective
get priority of processing and printing: in our limited practice, we
have seen this gives a better feeling of responsiveness of the prover,
as the output is reported where the user's cursor is, even in
bigger/slower files.
Carst
In the parallel case the window goes white
immediately once the print tasks have forked, from which point there is
no indication of progress, giving the impression the system has just
given up.Ideally I'd like to see some approximation ProofGeneral's behaviour, in
which many commands can be processed and only one goal state rendered.
Yes, my proofs are pathological, full of applications of fast
methods/tactics but with large complex goal states. I suspect, however,
that I'm not alone.Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited
accepts no liability for any damage caused by this email or its
attachments.
Email Gateway (Aug 19 2022 at 16:00):From: Vadim Zaliva <vzaliva@cmu.edu>
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?
I am old time Emacs User (20+ years) and for that reason I was preferring Proof General to JEdit.
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 16:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Vadim,
Does it mean 2014 version is no longer support emacs/Proof General?
indeed, yes. There might still be some tricks to keep that alive (which
I anyway do not know about), but in the middle run there will be no
other way than to use Isabelle/JEdit.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:03):From: René Neumann <rene.neumann@in.tum.de>
I'm running Isabelle 2014 with PG here. But setting it up was quite a
hassle. The important thing I noted was: With Isabelle-dev it's
simple, with the releases it is not. Hence I use the setup from the
-dev version:
$ cat .isabelle/etc/settings
if [[ $ISABELLE_HOME = 2014 ]]; then
init_components "$USER_HOME/.isabelle/contrib"
"$USER_HOME/isabelle/Isabelle-dev/Admin/components/optional"
fi
smime.p7s
Email Gateway (Aug 19 2022 at 16:04):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 16:04):From: Ferdinand Vesely <csfvesely@swansea.ac.uk>
On Wed, 10 Sep 2014 12:25:48 +0200
René Neumann <rene.neumann@in.tum.de> wrote:
Am 10.09.2014 10:06, schrieb Florian Haftmann:
Hi Vadim,
Does it mean 2014 version is no longer support emacs/Proof
General?indeed, yes. There might still be some tricks to keep that alive
(which I anyway do not know about), but in the middle run there
will be no other way than to use Isabelle/JEdit.Cheers, Florian
I'm running Isabelle 2014 with PG here. But setting it up was quite a
hassle. The important thing I noted was: With Isabelle-dev it's
simple, with the releases it is not.
I'm using PG with the release version. Now I don't remember all the
details but I've took the ProofGeneral package from
http://isabelle.in.tum.de/components/ and unpacked it inside
Isabele2014/contrib (I think it can go anywhere as long as you set the
PROOFGENERAL_HOME environment var). Then I copied the 'emacs' script
from the previous release's 'lib/Tools' folder into the 2014's
'lib/Tools' folder. I think I've set the PROOFGENERAL_HOME environment
variable in my '.bashrc'. Now 'isabelle emacs' works as before.
The jEdit Prover IDE is great but it's greedy compared to the
ProofGeneral setup.
Best wishes,
Ferdinand
Hence I use the setup from the
-dev version:$ cat .isabelle/etc/settings
if [[ $ISABELLE_HOME = 2014 ]]; then
init_components "$USER_HOME/.isabelle/contrib"
"$USER_HOME/isabelle/Isabelle-dev/Admin/components/optional"
fi
Email Gateway (Aug 19 2022 at 16:05):From: Lars Noschinski <noschinl@in.tum.de>
There is no need to do all this manually. As Makarius mentioned, this is
prepared as an component and components are documented in the system manual:
Add the line
init_component "$SOME_DIR/ProofGeneral-4.2-2"
to your $ISABELLE_HOME_USER/etc/settings file, where $SOME_DIR refers to
the directory where you want to store the extension. ($USER_HOME/contrib
might be a good value for that, as that is the directory the repository
version stores its components by default).
Then execute
isabelle components -a
to automatically install the missing component. Afterwards,
isabelle emacs
should give you a Proof General, provided you have an appropriate emacs
installation around.
Email Gateway (Aug 19 2022 at 16:06):From: Vadim Zaliva <vzaliva@cmu.edu>
Let me put forward some arguments in defence of Proof General support in Isabelle.
For the purpose of this discussion the functionality of PIDE such as Proof General as
well as Isabelle/Jedit could be broadly split into 3 categories:
Basic functionality - basic editing functionality used in Isabelle mode as well as for other
modes. Here you have managing multiple buffers, windows, search, clipboard, completion, etc.
Isabelle specific interface.
Other functionality of the PIDE which is not strictly speaking is necessary for working with Isabelle.
For example integration with other languages (ML, LISP, Haskell), spell checker integration, etc.
I have limited experience with #2 but for my purposes both Proof General and Isabelle/JEdit were comparable.
(Some people might find Jedit/Isabelle asynchronous proving superior to Proof General's sequential mode but I
like the control Proof General gives me. One of the reasons is that some of my lemmas take a long time to prove and I do not want to to try prove them until I am ready to do so. For example when I am reorganizing my proofs and moving code around
I would not want it to rush and try prove things until I am finished.)
Most importantly in #1 I found jEdit (mind you, not Isabelle/jEdit but jEdit itself) lacking, compared to Emacs.
A couple of trivial examples: I-search and working with rectangular blocks in copy/paste.
Finally, although it is not directly related to Isabelle, I think in #3 emacs have much more to offer due to
the amount of code written for Emacs over the decades.
For example I am working with Haskell, LISP code and Isabelle proofs at the same time and now I am forced to run jEdit and Emacs concurrently. Emacs key binding in jEdit are not exactly the same as real Emacs on Mac so I am constantly struggling
when switching between the two. With Proof General I was easily editing all Isabelle, LISP and Haskell from the comfort
of the same familiar environment.
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 16:06):From: Makarius <makarius@sketis.net>
On Fri, 12 Sep 2014, Vadim Zaliva wrote:
Let me put forward some arguments in defence of Proof General support in
Isabelle.
In principle this discussion is 5-3 years late. Already 5 years ago,
Isabelle/PIDE development has started to become serious, and 3 years ago
there was the turning point for practical use of Isabelle/jEdit as the
main application of the PIDE framework.
Hardcore users of Proof General Emacs have chosen to ignore this over a
long time. In Isabelle2014 the tiny change to make Proof General
"optional" -- with proper documentation in NEWS and hardly any effort to
reactivate it based on information from the "system" manual -- seems to
have the effect that people actually do wake up.
For the purpose of this discussion the functionality of PIDE such as
Proof General as well as Isabelle/Jedit could be broadly split into 3
categories:
Basic functionality - basic editing functionality used in Isabelle
mode as well as for other modes. Here you have managing multiple
buffers, windows, search, clipboard, completion, etc.Isabelle specific interface.
Other functionality of the PIDE which is not strictly speaking is
necessary for working with Isabelle. For example integration with
other languages (ML, LISP, Haskell), spell checker integration, etc.
I have limited experience with #2 but for my purposes both Proof General
and Isabelle/JEdit were comparable.
This means you did not spend long enough with Isabelle/jEdit, to find out
what it really does (and what not yet). The "jedit" manual in
Isabelle2014 is once again updated and extended, and now rather long with
almost 50 pages. There is a lot to discover, but long-term Proof General
users need to unlearn quite a lot.
Some people might find Jedit/Isabelle asynchronous proving superior to
Proof General's sequential mode but I like the control Proof General
gives me.
The document-oriented approach with implicit checking is inherent in PIDE.
If you don't believe in it, you are welcome to start a project to
implement a PG-emulation using the official Isabelle protocol function
interface (not the old TTY loop, which is already legacy). This is
possible in user-space, using the current Isabelle/Scala infrastructure to
connect Isabelle to the outside world.
Most importantly in #1 I found jEdit (mind you, not Isabelle/jEdit but
jEdit itself) lacking, compared to Emacs. A couple of trivial examples:
I-search and working with rectangular blocks in copy/paste.
Both search and blocks work much better in jEdit than in Emacs. After 15
years of Emacs, I left it behind in 2006, and today I can't live without
jEdit quick-search / hyper-search and various advanced selection modes.
The two weeks I had invested in 2006 to unlearn Emacs key bindings and
learn a few jEdit tricks have paid off.
The general qualities of jEdit also convinced me in 2006/2007 to make it
the basis for the main example application of PIDE.
This does not mean all PIDE applications need to work with jEdit.
Isabelle/Eclipse and Clide have already been mentioned, and will hopefully
be updated soon to Isabelle2014.
Finally, although it is not directly related to Isabelle, I think in #3
emacs have much more to offer due to the amount of code written for
Emacs over the decades.
This can be accounted both on the positive and negative side. Tons of
existing material in Emacs makes it slow to move anywhere. Most of the
material is actually obsolete.
In contrast, jEdit has many useful plugins, while many things are missing,
but it is easy to improve on that. I have done quite something for
Isabelle/jEdit -- the "Isabelle" plugin has become a large assembly of
modules to augment jEdit in many ways, both specifically and
non-specifically to Isabelle.
jEdit is somewhere in the middle in project size and complexity, e.g.
compared to Emacs or Eclipse, and it is relatively easy to move it
onwards, with a little bit of enthusiam and energy.
For example I am working with Haskell, LISP code and Isabelle proofs at
the same time and now I am forced to run jEdit and Emacs concurrently.
Emacs key binding in jEdit are not exactly the same as real Emacs on Mac
so I am constantly struggling when switching between the two. With Proof
General I was easily editing all Isabelle, LISP and Haskell from the
comfort of the same familiar environment.
With "familiar environment" we are back to "I don't want to change
habits".
I don't see why an Isabelle front-end should specifically support Emacs,
apart from accidental side-conditions from the past. Why not vi instead?
The old debate of Emacs vs. vi has long been settled in favour of vi
anyway.
Makarius
Email Gateway (Aug 19 2022 at 16:06):From: Lars Noschinski <noschinl@in.tum.de>
Incremental search in jEdit is by default to "Alt+,"; rectangular
selection can be toggled by "Alt+#".
Last updated: Apr 19 2024 at 20:15 UTC