Email Gateway (Sep 02 2022 at 06:17): Email Gateway (Sep 02 2022 at 06:17):From: Lawrence Paulson <lawrencecpaulson@icloud.com>
I was just checking something and noticed that Isabelle/CTT seems to hang if you try e.g.
isabelle jedit -l CTT ex/Synthesis.thy
On the other hand,
isabelle jedit -l Pure ex/Synthesis.thy
works perfectly.
Another thing: with schematic_goal, the display of the proof state really needs to include the schematic goal itself, because it’s getting modified. Obviously this can’t be a priority, but if we’re lucky, the relevant code is still there.
Larry
Email Gateway (Sep 09 2022 at 14:17):From: Makarius <makarius@sketis.net>
I am now ready to answer some questions (both explicit and implicit ones).
(1) Isabelle/jEdit appears to "hang": this is because the CTT session already
contains the example (there used to be separate sessions CTT and CTT-ex many
years ago). We used to have a minimalistic PIDE error message "Cannot update
finished theory", but that was lost in 2019 (changeset cceb10dcc9f9).
I have amended that as follows:
changeset: 76046:507c65cc4332
user: wenzelm
date: Sat Sep 03 17:20:35 2022 +0200
files: src/Pure/PIDE/resources.ML src/Pure/PIDE/resources.scala
description:
back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant
for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error
"Cannot update finished theory CTT.Elimination";
I have also added a few more changes to the tension of logical theory names
(e.g. HOL-Library.Multiset) vs. file-system path names more robust, for example:
changeset: 76050:f1dc3d9d5164
user: wenzelm
date: Sat Sep 03 22:25:22 2022 +0200
files: src/Pure/PIDE/resources.ML src/Pure/PIDE/resources.scala
description:
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";
In the next round of refinements (after the release), I will make finished
theories load their PIDE markup from the build database and display that.
Moreover there should be better GUI feedback about the status of read-only
browsing of already loaded theories vs. editable theories.
(2) Schematic goals and main goal state. In the depths of time, goal states
were directly shown to the user, notably the main conclusion (as a reminder on
the TTY and to see the current instantiation). This came out of use, because
it was a waste of screen space and time to print it. The option show_main_goal
is still there to get this old behaviour, but it is a bit ugly, because the
goal package treats the main goal as private property that is not shown to
users: it may contain funny markers and auxiliary goals to ensure that
schematic goal instances can be determined reliably.
It is still possible to enable show_main_goal for a theory context, e.g.
HOL-Prolog.HOHH at this point in history
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/Prolog/HOHH.thy;922e3f9251a$13
(from 08-Sep-2022). Applications of HOL-Prolog will then show the full goal
state as in 1989.
I have discontinued this nostalgic mode only 1h later:
changeset: 76094:4dec713d3bc9
user: wenzelm
date: Thu Sep 08 22:59:21 2022 +0200
files: src/HOL/Prolog/HOHH.thy
description:
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient,
even for final results;
For CTT it is up to you: either use the new "goal instantiation" display,
which is there by default, or enable the old show_main_goal option in theory CTT.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 19 2024 at 16:20 UTC