[isabelle-dev] Confusion aroung master path of theory
makarius at sketis.net
Fri Jul 20 22:06:15 CEST 2012
On Fri, 20 Jul 2012, Florian Haftmann wrote:
> cs. http://isabelle.in.tum.de/repos/isabelle/rev/3a5a5a992519 was an
> attempt to make results of `export_code` with relative file path more
> predictable. There my assumption was that Thy_Load.master_directory
> would point to an absolute path, particulary the location of the current
> theory, but this was a guess. Now I see that in most cases it just
> points to `.`, which contradicts my previous understanding that the
> master directory concept would make the notion of current working
> directory obsolete.
This depends on some side-conditions. I guess that you have run "isabelle
tty" or "isabelle-process" here. This implicitly requires to cd to the
session directory, just as usedir does before running the tty process.
The Isabelle/Scala document model is in a transitory state where the
master_directory works in fully stateless manner in most situations. So
in Isabelle/jEdit Thy_Load.master_directory should work.
Proof General has its own traditional way to "cd" along with the files
being processed, which it has been upgraded at some point to use the
master directory as well, so it should also work.
> So, to lift my confusion, two questions:
> a) Is there a way to interpret a given relative path as relative to the
> (absolute) location of the current theory?
File.pwd () gives you an absolute path, and you can just use Path.append
as usual. Note that the Path algebra does the right thing when two
absolute paths are appended: the first one is ignored.
> b) If the »master directory« is not the concept to achieve this, what is
> it then supposed to be?
The master directory is basically correct, modulo some fine points.
One potential snag is that the master directory might not be writable at
all, because it is some URL obtained via the IDE front-end, or since the
prover is not on the same file-system as the front-end. This touches an
open question that is beyond the small issues at the moment, and it is not
fully active right now.
More information about the isabelle-dev