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



I found the following workaround to this problem:

Just place symbolic links to the ML-files at the places where 
isabelle build -l
seems to expect them, according to the error message. This blows up your
directory structure, creating meaningless directories, but at least
listing of dependencies seems to work, the symbolic links do not even
occur in the dependencies listing.

--
  Peter

On Mi, 2014-05-21 at 12:30 +0200, Peter Lammich wrote:
> 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






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