[isabelle-dev] Two problems

[Makarius]

On Mon, 3 Dec 2012, Jasmin Christian Blanchette wrote:

> I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP 
> (40ecbad14077).
>
> 1. In Proof General:
>
>    theory Scratch
>    imports
>      "$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe"
>      "~~/src/HOL/Proofs/Lambda/StrongNorm"
>    begin
>
> nondeterministically gives either
>
>    *** Undeclared type constructor: "vname" (line 12 of "/Users/blanchet/afp/thys/Jinja/Common/Decl.thy")
>    *** Failed to parse type
>    *** in type abbreviation "fdecl"
>    *** At command "type_synonym" (line 11 of "/Users/blanchet/afp/thys/Jinja/Common/Decl.thy")
>
> or
>
>    *** Inner lexical error at: ⟪i:U⟫ ⊢ t : T ⟹
>    ***     IT u ⟹ e ⊢ u : U ⟹ IT (t[u/i]) (line 91 of "~~/src/HOL/Proofs/Lambda/StrongNorm.thy")
>    *** Failed to parse proposition
>    *** At command "lemma" (line 90 of "~~/src/HOL/Proofs/Lambda/StrongNorm.thy")
>
> but each of them loads fine on its own.

Proof General uses the theory loader of the TTY, and that has certain 
"features".  There used to be a toplevel load path, with directories 
searched in a certain order, and the first fit was taken.  Later that was 
found useful in the imports part as well, but it causes odd effects until 
today: your imports are somehow non-authentic and non-compositional. 
Having theory "Type" via one part of the import graph already, it is not 
imported again just because some file happens to be around in a different 
directory.

In recent years I've worked towards sorting out many such odd effects. 
The "master directory" instead of "load path" was already some 
improvement.


In your observations above, are you sure that "nondeterministically" means 
physical nondeterminism, say due to parallel loading of theories?  Or 
theories that you have visited before in Proof General, before starting 
the above one?

My hope and expectation for the classic theory loader is that it first 
explores the whole graph as specified in the imports list.  Then it starts 
loading in parallel.  Shuffling imports a little may change the order of 
theory discovery and loading, but with given struture specified in the 
theory sources it should be deterministic (although sometimes surprising).


Note that Isabelle/jEdit handles this a bit differently.  The full master 
path is taken into account for theory source identification.  Later there 
is the classic check of consistent naming that produces this error in the 
above example:

exception THEORY raised (line 325 of "context.ML"):
Inconsistent theory versions
{..., Nitpick, Main, Lambda, ListApplication, Type}
{..., Predicate_Compile, Nitpick, Main, Aux, Type}

Testing a bit further, I've actually discovered a dropout stemming from 
Dec-2008: clashes on the imports list itself were not rejected like that. 
This is now addressed in Isabelle/955c4aa44f60.  (Luckily the externally 
visible names are not relevant for the integrity of the "nano kernel", 
only the internal ids.)


 	Makarius