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
 /tmp/ROOTS       -- Contains A
 /tmp/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

and get:
[...]
Session Unsorted/A
 A/A.thy
 A/test.ML
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 that happened).


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.