[isabelle-dev] Mirabelle and load path

Makarius makarius at sketis.net
Fri Mar 4 13:15:29 CET 2011

On Fri, 4 Mar 2011, Makarius wrote:

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

The included example theory shows how to embed transactions with generated 
position information.

-------------- next part --------------
theory A imports Main

Isabelle.command ("file"="A.thy", "line"="1") "definition \"foo = 0\""
Isabelle.command ("file"="A.thy", "line"="5") "definition \"bar = 1\""


More information about the isabelle-dev mailing list