Email Gateway (Aug 19 2022 at 14:32): Email Gateway (Aug 19 2022 at 14:32):From: Peter Lammich <lammich@in.tum.de>
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)?
tmp.tgz
Email Gateway (Aug 19 2022 at 14:32):From: Peter Lammich <lammich@in.tum.de>
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.
Email Gateway (Aug 19 2022 at 14:32):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 14:32):From: Makarius <makarius@sketis.net>
Using symlinks with the JVM (i.e. the substrate below Isabelle/Scala) can
have surprising effects.
Before Java 7 there was no symlink support -- they were dereferenced.
After Java 7 the situation has improved, but it merely means there are new
programming interfaces in addition to the old ones that did not change, so
one cannot rely on that with existing JVM tools and applications.
On Windows there are traditionally no symlinks at all, although Windows 7
introduced that, at least in theory. To get a taste for Isabelle/Scala
cross-platform system programming here is an operation to make a symlink
for Cygwin:
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2013-2/src/Pure/Tools/main.scala#l190
Makarius
Last updated: Apr 20 2024 at 04:19 UTC