Email Gateway (Aug 22 2022 at 12:13): Email Gateway (Aug 22 2022 at 12:13):From: bnord <bnord01@gmail.com>
Dear Isabelle developers,
as the Isabelle/jEdit folding feature has no support for folding proofs
based on proof structure I used to use indentation based folding in
jEdit. In 2016-RC1 this seems to be broken and I get very wired folding
that doesn't correspond to my indentation. I enabled "fold mode: indent"
in the global editing options.
Example:
lemma x
proof
have y proof
(stuff)
qed
have z sorry proof
(stuff)
qed
qed
folding at the first proof in line 2 used to yield
lemma x
proof [6 lines]
qed
with 2016-RC1 it yields
lemma x
proof [3 lines]
have z sorry proof
(stuff)
qed
qed
and awkwardly moving the proof from line 2 to line 1 and folding there
folds the hole proof as expected.
Best
Benedikt
Email Gateway (Aug 22 2022 at 12:17):From: Makarius <makarius@sketis.net>
On Wed, 20 Jan 2016, bnord wrote:
as the Isabelle/jEdit folding feature has no support for folding proofs based
on proof structure I used to use indentation based folding in jEdit.
That approach was already obsolete in Isabelle2015, see this old NEWS
entry:
* Prover IDE -- Isabelle/Scala/jEdit *
In 2016-RC1 this seems to be broken and I get very wired folding that
doesn't correspond to my indentation. I enabled "fold mode: indent" in
the global editing options.Example:
[...]
I think there are 3 mistakes here:
1) Isabelle2016-RC1 has indeed a problem with the fold depth for
proof-qed parentheses, which were not counted as blocks in
Isabelle2015 at all. This should work better with the next release
candidate.
2) Your example has one 'sorry' too much for proper nesting of proof
structure. Or is this part of the bad situation?
3) I guess that in the experiment, the fold mode was actually "isabelle"
and not "indent".
I don't really know how "indent" fold mode works: if there is a change in
that respect from Isabelle2015 to Isabelle2016-RC1 it might be an issue of
jedit-5.2.0 vs. jedit-5.3.0.
Or there might be a problem of jEdit selecting the fold mode that you've
had in mind.
Makarius
Email Gateway (Aug 22 2022 at 12:18):From: bnord <bnord01@gmail.com>
Am 24.01.16 um 20:57 schrieb Makarius:
I don't really know how "indent" fold mode works: if there is a change
in that respect from Isabelle2015 to Isabelle2016-RC1 it might be an
issue of jedit-5.2.0 vs. jedit-5.3.0.
It worked by folding up to the next line with same or less indentation,
thereby giving the user full control over what needs to be folded away.
In particular it allowed one to fold away cases such that even in a
deeply nested proof with many cases one could have all assumptions made
before on screen at the same time. I.e. folding from a proof to the
"next" statement.
That approach was already obsolete in Isabelle2015, see this old NEWS
entry:
I wouldn't call it obsolete if it had useful features that the new
method didn't have.
I think there are 3 mistakes here:1) Isabelle2016-RC1 has indeed a problem with the fold depth for
proof-qed parentheses, which were not counted as blocks in
Isabelle2015 at all. This should work better with the next release
candidate.
Yes I just tried out the RC2 version, folding from proof to qed works
now fine, which is very nice, but I still can't fold away a case i.e.
to the "next" statement. I could start making case distinctions like
"proof cases assume a show ?case proof - ... qed" but its additional
boilerplate code.
2) Your example has one 'sorry' too much for proper nesting of proof
structure. Or is this part of the bad situation?
Yes sorry, messed that up but it wouldn't have made a difference for
folding by indentation.
3) I guess that in the experiment, the fold mode was actually
"isabelle"
and not "indent".
I double checked the fold mode was set to indent, I also switched it
back and forth.
Or there might be a problem of jEdit selecting the fold mode that
you've had in mind.
Yes, it seems like the setting is ignored or somehow overwritten to
isabelle folding. Even if I select "none" I still get Isabelle folding.
By the way, after updating to RC2 (I need do mention that I'm working of
the isabelle-release repository because I have my bsup/esub display
patch running on top) the jEdit window wouldn't start up after building
HOL and I had to kill and restart the process. Afterwards it started
fine but there was no output panel anywhere, but this might be a side
effect of my old configuration where it was a floating instance.
(Running on OS X by the way)
Best
Benedikt
Email Gateway (Aug 22 2022 at 12:18):From: bnord <bnord01@gmail.com>
Ignore this, just downloaded the genuine RC2 from the website, works
fine there.
Last updated: Apr 24 2024 at 20:16 UTC