[isabelle-dev] Mirabelle and load path
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