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:

Just place symbolic links to the ML-files at the places where isabelle build -l seems to expect them, according to the error message.

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




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