[isabelle-dev] Isabelle/CTT

[Makarius]

On 01/09/2022 20:09, Lawrence Paulson wrote:
> 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.

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