[isabelle-dev] Mirabelle and load path
krauss at in.tum.de
Fri Mar 4 12:33:07 CET 2011
>> 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
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.
More information about the isabelle-dev