[isabelle-dev] Mirabelle and load path

Makarius makarius at sketis.net
Fri Mar 4 12:36:32 CET 2011

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.


More information about the isabelle-dev mailing list