Email Gateway (Jul 28 2023 at 16:54): Email Gateway (Jul 28 2023 at 16:54):From: Fabian Immler <cl-isabelle-users@lists.cam.ac.uk>
Hi everyone,
We noticed that the semantics of print_theorems has changed.
In Isabelle2022 print_theorems behaves as described in isar-ref:
"print_theorems prints theorems of the background theory resulting from the last command"
Since Isabelle2023-RC0, print_theorems prints not just the theorems resulting from the last command but rather what looks like all theorems from the current theory.
Neither NEWS nor isar-ref indicate that the semantics of print_theorems was changed on purpose.
Below is a sequence of commands illustrating the changes.
Best wishes,
Fabian
Scratch.thy:
=========
theory Scratch
imports
Main
begin
definition "c1 = True"
print_theorems
(* Isabelle2022: c1_def *)
(* Isabelle2023-RC2: c1_def *)
definition "c2 = True"
print_theorems
(* Isabelle2022: c2_def *)
(* Isabelle2023-RC2: c1_def,c2_def *)
locale foo begin
print_theorems
(* Isabelle2022: *)
(* Isabelle2023-RC2: c1_def,c2_def *)
definition "c3 = True"
print_theorems
(* Isabelle2022: foo.c3_def *)
(* Isabelle2023-RC2: c1_def,c2_def,foo.c3_def *)
end
context foo begin
print_theorems
(* Isabelle2022: *)
(* Isabelle2023-RC2: c1_def,c2_def,foo.c3_def *)
definition "c4 = True"
print_theorems
(* Isabelle2022: foo.c4_def *)
(* Isabelle2023-RC2: c1_def,c2_def,foo.c3_def,foo.c4_def *)
end
end
—
Fabian Immler
fimmler@apple.com <mailto:fimmler@apple.com>
SEG Formal Verification
Email Gateway (Jul 29 2023 at 19:33):From: Makarius <makarius@sketis.net>
Why treat the system like a mysterious black-box?
The first thing to do in such a situation is to use "induction over the
history of the sources", i.e. "hg bisect".
(I am presently on travel and cannot really test anything.)
Makarius
Email Gateway (Jul 31 2023 at 07:44):From: Fabian Immler <cl-isabelle-users@lists.cam.ac.uk>
On 29. Jul 2023, at 21:33, Makarius <makarius@sketis.net> wrote:
Why treat the system like a mysterious black-box?
I would not phrase it that way. My first priority was to report this observation as soon as possible.
And get quick feedback on whether, e.g., this was changed on purpose.
In that case, further investigations would have been a waste of time.
The first thing to do in such a situation is to use "induction over the history of the sources", i.e. "hg bisect".
Thank you for the suggestion. "hg bisect" returned:
The first bad revision is:
changeset: 76813:92a547feec88
user: wenzelm
date: Thu Dec 29 13:00:16 2022 +0100
summary: tuned;
I don't see how this changeset introduces the observed change in behaviour of print_theorems.
Fabian
Email Gateway (Jul 31 2023 at 12:30):From: Peter Lammich <lammich@in.tum.de>
I'm getting a similar behavior for print_theorems as Fabian reports. The
output seems unrelated to the last statement that has been executed, but
seems to display everything in the current theory.
This is clearly a regression against 2022, and, imho, a quite annoying one.
Email Gateway (Aug 08 2023 at 10:42):From: Makarius <makarius@sketis.net>
Thanks for the bisection, and the test report in the first place.
It was a genuine accident that I have now amended here:
https://isabelle.sketis.net/repos/isabelle-release/rev/44ffc06187e0
changeset: 78487:44ffc06187e0
tag: tip
user: wenzelm
date: Tue Aug 08 12:35:14 2023 +0200
summary: proper prev_thy (amending 92a547feec88), notably for the sake of
'print_theorems', which is the only use of Toplevel.previous_theory_of;
NB: Isabelle2023-RC3 should appear within a few days.
Makarius
Last updated: Apr 29 2024 at 04:18 UTC