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
original location.
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.
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
