Email Gateway (Jul 18 2023 at 17:08): Email Gateway (Jul 18 2023 at 17:08):From: Fabian Immler <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
The output of "results" has changed (already in Isabelle2022), and I don't think this behavior is desirable:
With "results", I mean some output of commands, e.g.,
- "definition c = ..." outputs the result "consts c :: ..."
- "lemmas thm_name" outputs the theorem statement of thm_name
- "lemma ... by ..." outputs the theorem statement
Isabelle2021-1 (and earlier) used to always output "results" to the Output panel.
In Isabelle2023-RC1 (also already in Isabelle2022), "results" only appear in the Output panel when the "Proof state" checkbox is enabled.
I don't think this is desirable, because "results" have nothing to do with the notion of "Proof state".
I do want to keep the proof state (in the State panel) separate from the Output panel.
Moreover, I believe there is a reason that "Proof state" is disabled by default (performance?).
A closely related thread:
[isabelle] Automatic theorem/definition printing appears not work in interactive mode
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2023-05/msg00045.html
Best wishes,
Fabian
—
Fabian Immler
fimmler@apple.com <mailto:fimmler@apple.com>
SEG Formal Verification
Email Gateway (Jul 26 2023 at 14:13):From: Makarius <makarius@sketis.net>
On 18/07/2023 18:07, Fabian Immler (via cl-isabelle-users Mailing List) wrote:
The output of "results" has changed (already in Isabelle2022), and I don't
think this behavior is desirable:
The first thing to do in such a situation is to provide some "proof from the
history", to see where the change has happened (and maybe what its intentions
have been). "hg bisect" can easily do that; there is no need to understand the
sources for that.
The result is as follows:
changeset: 75840:f8c412a45af8
user: wenzelm
date: Sat Aug 13 14:29:59 2022 +0200
summary: more accurate treatment of option "editor_output_state", e.g.
when changed via Isabelle/jEdit Plugin Options panel;
Isabelle2021-1 (and earlier) used to always output "results" to the Output panel.
In Isabelle2023-RC1 (also already in Isabelle2022), "results" only appear in
the Output panel when the "Proof state" checkbox is enabled.
Some further digging into the history shows that such "result messages" have
been counted as "state output" already since 2014:
changeset: 56897:c668735fb8b5
user: wenzelm
date: Wed May 07 13:55:16 2014 +0200
files: src/Pure/Isar/obtain.ML src/Pure/Isar/proof.ML
src/Pure/Isar/proof_display.ML src/Pure/Isar/specification.ML
src/Pure/Isar/toplevel.ML
description:
print results as "state", to avoid intrusion into the source text;
print new local theory (again);
With a bit more browsing and reasoning over the history, it becomes apparent
that f8c412a45af8 is more correct concerning "state messages" than before.
(But it also shows more clearly that "toplevel results" might be better
treated differently.)
I will skip further details of the reasoning due to lack of time at this stage
of the release process. The proper time for such discussions is usually before
the release process actually start, e.g. the now traditional "RC0" preview.
I don't think this is desirable, because "results" have nothing to do with the
notion of "Proof state".
I do want to keep the proof state (in the State panel) separate from the
Output panel.
I will make a quick experiment this afternoon to use the regular
Output.writeln channel instead of Output.state, and a quick adhoc decision if
it goes into Isabelle2023-RC2.
We then still have a final change to revert it for Isabelle2023-RC3 in < 2
weeks. (In violation of all good manners for a release.)
Moreover, I believe there is a reason that "Proof state" is disabled by
default (performance?).
Yes, there is a long standing track record of problems stemming from
over-ambitios printing of such state information. (It is particularly bad for
"tracing", where people often think it does not matter, and later find that
99% time is spent printing.)
Thus any kind of proof state (or result) output needs to be done with extra
care. The NEWS for Isabelle2021-1 have an example for that:
Configuration option "show_results" controls output of final results
in commands like 'definition' or 'theorem'. Output is normally enabled
in interactive mode, but it could occasionally cause unnecessary
slowdown. It can be disabled like this:
context notes [[show_results = false]]
begin
definition "test = True"
theorem test by (simp add: test_def)
end
A closely related thread:
[isabelle] Automatic theorem/definition printing appears not work in
interactive mode
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2023-05/msg00045.html
I had seen that, but ignored it at that point because there was no attempt for
provide "proof from the history" via "hg bisect".
Makarius
Email Gateway (Jul 26 2023 at 21:40):From: Makarius <makarius@sketis.net>
The result of the "quick experiment" in now in Isabelle2023-RC2:
https://isabelle.sketis.net/repos/isabelle-release/rev/53b59fa42696
We have time until Isabelle2023-RC3 to figure out if it is a good idea or bad
idea. (This assumes that actual testing starts now, not after the final release.)
Makarius
Last updated: Apr 29 2024 at 04:18 UTC