Email Gateway (Aug 22 2022 at 12:47): Email Gateway (Aug 22 2022 at 12:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
I've noticed with Isabelle2016-RC3 that the bar on the right hand side of the main text
area (in which errors are marked with red lines, warnings with yellow ones, and
unprocessed parts in light red) seems not to be updated synchronously with the processing
of the theory file.
When I change something a large theory file (more than 8000 lines) somewhere in the
beginning, I then normally jump to the end of the file to have it reprocessed. As soon as
an error occurs (indicated by a red bar in the theory panel), I then would like to click
on the red line in the bar on the right of the main text area to immediately jump to the
error and make the necessary adaptations. Unfortunately, in Isabelle2016-RC3, the bar does
not seem to get updated as regularly as in Isabelle2015, the update only happens if
processing approaches the end of my theory (which can take a while). If there is an error
fairly at the beginning, then after having fixed this, I again have to wait until most of
it is processed until I find the next error. Is there some configuration to have the bar
updated more frequently?
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:47):From: Christian Sternagel <c.sternagel@gmail.com>
It doesn't answer your question, but I usually observe the "Theory"
panel while loading big theories (I think errors are marked there as
soon as they "happen").
cheers
chris
Email Gateway (Aug 22 2022 at 12:48):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Chris,
I also watch the theories panel, but I cannot click in the theories panel to take me to
the location of the error. For that I need the bar of the main text area.
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 12:49):From: Makarius <makarius@sketis.net>
This is indeed a bit odd. The text overview column has been reworked
significantly for Isabelle2016, but a few fine points still need to be
polished further.
Presently there is
https://bitbucket.org/isabelle_project/isabelle-release/commits/8bf765c9c2e
to improve this: less CPU requirements, more reactivity.
The next Isabelle2016-RC will be published officially within a few days.
Makarius
Email Gateway (Aug 22 2022 at 12:49):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
I'll try again after the next RC will have been published and let you know whether things
have improved.
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:50):From: Rafal Kolanski <xs@xaph.net>
Hi Andreas,
We have large proofs too and often find ourselves "looking for the red
bit" while no red bit appears in the text overview. Additionally,
clicking with the mouse isn't super accurate. Please consider trying out
my hack to jump to the first error in the current theory file:
https://github.com/seL4/l4v/blob/master/misc/jedit/macros/goto-error.bsh
I have it bound to ctrl+shift+e and use it all the time.
Hopefully this will help a bit.
Raf.
Email Gateway (Aug 22 2022 at 12:51):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
In Isabelle2016-RC4, the text overview column is updated much more synchronous with the
theory panel. After my first few tests, it looks as if this works again.
Thanks,
Andreas
Email Gateway (Aug 22 2022 at 12:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Rafal,
Thanks for the pointer to the macro. This is really useful.
Andreas
Last updated: Apr 20 2024 at 08:16 UTC