[isabelle-dev] Mirabelle and load path

[Alexander Krauss]

>> So I am wondering if the system could provide a variant of use_thy(s), 
>> which takes an explicit master path and basically interprets the given 
>> theory as if it would reside in that path. Probably, similar 
>> functionality is already available for PG interaction. Of course any 
>> other solution would be fine as well...
> 
> It should be sufficient to include the path in the use_thy invocation:
> 
>   use_thy "/tmp/A.thy";
> 
> Alternatively there is
> 
>   Thy_Info.use_thys_wrt: Path.T -> string list -> unit

You misunderstood my question. Finding theory A is not the problem, but 
finding its dependencies, which are not in /tmp: If theory A imports B 
(without explicit path), it will look for /tmp/B.thy, instead of the 
original location.

What I was asking for is a possibility to load a theory file A.thy from 
location X (here: the location of the modified theory file in /tmp) with 
a master path pointing to location Y (here: the original location of the 
theory file). Then, the dependencies of A will be found in path Y.

Currently, the only chance of running A.thy successfully (in batch mode) 
is to physically place it in the directory where its dependencies are. 
This is somewhat rigid and problematic for Mirabelle.

Alex