[isabelle-dev] Mirabelle and load path

[Makarius]

On Fri, 4 Mar 2011, Alexander Krauss wrote:

> 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.

In that case Mirablle can copy all sources to /tmp and then poke around.


 	Makarius