Re: [isabelle] isabelle build -l, I/O error with ML-files on indirection through ROOTS file or -d option
On Wed, 21 May 2014, Peter Lammich wrote:
I have encountered the following undesired behaviour with
isabelle build -l, when I wanted to list the dependencies of a session
that depends on various other sessions. Here is a minimal example:
I have the following directory structure:
/tmp/ROOTS -- Contains A
/tmp/A/test.ML -- Arbitrary ML-file
/tmp/A/A.thy -- Contains ML_file "test.ML" command
/tmp/A/ROOT -- Declares session A = HOL + theories A
Inside /tmp folder, I do:
> isabelle build -d. -nl A
I/O error: A/A/test.ML (No such file or directory)
The error(s) above occurred in session "A" file "A/A/test.ML"
In Isabelle2013-2 this should work if you write "$PWD" instead of "." --
and it also works in the totally arbitrary repository version
2fdd5a0a1f9f, so for Isabelle2014 this should not happen again.
Generally note that the current working directory is a Unix command-line
concept, and in recent years it has mostly disappeared from Isabelle.
2 years ago we still had this odd Unix "make" setup, which does require to
"cd" around and causes many other problems related and unrelated to that.
The Isabelle/ML and Isabelle/Scala no longer change working directories,
but append directories explicitly. So the above might have been a
boundary case somewhere, although of little practical relevance, and
already gone for some unspecified time (I did not make a bisection when
This archive was generated by a fusion of
Pipermail (Mailman edition) and