[isabelle-dev] Confusion aroung master path of theory

[Makarius]

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. 
http://isabelle.in.tum.de/repos/isabelle/annotate/3ceccd415145/src/Pure/ProofGeneral/proof_general_emacs.ML#l254


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


 	Makarius