Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2023-RC2: Proof state not shown after ...

Email Gateway (Jul 30 2023 at 13:03):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,

after typedef or lift_definition, the proof state is not shown in the
"Output" panel (even with "Proof state" and "Auto update" activated).
However, in the "State" panel it is shown. Also, after applying a method
to the current goal (even if it fails), the proof state is shown in the
"Output" panel.

The attached theory illustrates this.

Best wishes,
Dominique.

Scratch.thy

Email Gateway (Jul 31 2023 at 17:06):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

it seems that also other commands show this effect, e.g.,

function foo :: "nat ⇒ nat" where
"foo x = (if x = 0 then 1 else foo (x - 1))"
(* no proof state shown *)
by pat_completeness auto

termination
(* no proof state shown *)
by lexicographic_order

Generalising this, it seems that definitional commands that produce a proof-obligation are affected.

Perhaps some change in local_theory_to_proof?

Best,
René

Email Gateway (Jul 31 2023 at 18:31):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
A bisection reveals that changeset 40a365360680 is the relevant one.
Unfortunately, the diff does not enlighten me why this change has such a dramatic effect.

Best,
René

Email Gateway (Jul 31 2023 at 19:39):

From: Makarius <makarius@sketis.net>
Thanks for the changeset ID.

I will look at this at the beginning of next week, shortly before the
next release candidate.

Makarius

Email Gateway (Aug 08 2023 at 15:56):

From: Makarius <makarius@sketis.net>
Thanks for reporting (and bisecting) it.

I have now addressed that here:
https://isabelle.sketis.net/repos/isabelle-release/rev/40d50936484c

changeset: 78488:40d50936484c
user: wenzelm
date: Tue Aug 08 17:17:42 2023 +0200
files: src/Pure/PIDE/document.ML
description:
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit
"print_state" for commands defined after Pure;

Without proper keywords, certain PIDE policies for scheduling commands and
print functions don't work.

Makarius

Last updated: Jan 04 2025 at 20:18 UTC