Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Automatic theorem/definition printing appears ...


view this post on Zulip Email Gateway (Mar 21 2023 at 04:53):

From: Rafal Kolanski <xs@xaph.net>
Hi,

most likely in the Isabelle 2022 update, the automatic printing of
theorems and definitions stopped working for me while in jEdit.

I have the state and output split into separate buffers. Normally I'd
expect:

lemma blah:
"something" (* prints goal state in proof state buffer *)
apply (simp ...) (* prints goal state in proof state buffer *)
done (* prints proved lemma in output buffer *)

This was especially useful for figuring out what transformed lemmas were
generated without modifying the buffer, e.g.

lemmas corres_underlying_gets_pre_rhs =
corres_symb_exec_r[OF _ _ gets_inv no_fail_pre[OF no_fail_gets TrueI]]

This is probably related to the relatively recent feature of turning on
these outputs when not in interactive mode (show_states/show_results).

I initially thought this line in proof_display.ML was causing the
decision whether to print or not:

fun no_print int ctxt = not (Config.get (Config.put interactive int
ctxt) show_results);

but it is clear I don't really comprehend the implications here.

Can anyone offer some insight?

Raf.

view this post on Zulip Email Gateway (May 24 2023 at 04:09):

From: Rafal Kolanski <xs@xaph.net>
I have finally figured out what the regression is. The
"editor_output_state" setting has conflated two concepts when moving to
Isabelle 2022:

Ideally, one would want to control these separately:

This can be worked around by changing the following in
src/Tools/jEdit/src/output_dockable.scala :

val new_output =
if (restriction.isEmpty || restriction.get.contains(command))

The situation might make sense if output_messages filtered out only
proof state messages when its output_state argument is false, but it
seems that:

Perhaps the filtering in output_messages is supposed to filter state
messages into "states" and results messages into "other", but it
doesn't. I don't have any more time for code decryption.

Raf.

view this post on Zulip Email Gateway (Jul 26 2023 at 14:40):

From: Makarius <makarius@sketis.net>
We have a long and complex history, especially for interaction with Isabelle:
historically ProofGeneral Emacs (some of its legacy is still there), now PIDE
with Isabelle/jEdit or Isabelle/VSCode or "isabelle server" as front-ends.

All that needs to be taken into account when sorting out such fine points.
Moreover, it is important to look into the formal Mercurial (not git) history,
e.g. using "hg bisect".

That was missing on this thread: I did not have time to do your homework.

Just for the historical record, here are a few relevant changesets:

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;

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);

changeset: 74156:ecf80e37ed1a
user: wenzelm
date: Wed Aug 18 23:04:58 2021 +0200
files: NEWS src/Pure/Isar/attrib.ML src/Pure/Isar/proof_display.ML
description:
support configuration options "show_results";

If something still emerges from that for Isabelle2023-RC2 depends how other
details work out.

Makarius


Last updated: Mar 29 2024 at 08:18 UTC