[isabelle] isabelle build -l, I/O error with ML-files on indirection through ROOTS file or -d option



Hi all,

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"

The same error occurs without a ROOTS file and the command:
  > isabelle build -d A -nl A


Note that the very same command works as expected inside /tmp/A folder.
Also note that "isabelle build -d. A" verifies the session without
complaints inside both /tmp, and /tmp/A.


I have attached the minimal example from above.

Is there any way/workaround how I can get the list of files that my
session depends on in a setting with multiple ROOT-files (e.g. the AFP)?

--
  Peter

Attachment: tmp.tgz
Description: application/compressed-tar



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