[isabelle] Isabelle2016-RC0: Windows bootstrapping · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2016-RC0: Windows bootstrapping

Email Gateway (Aug 22 2022 at 12:26):

From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,

after testing RC0 some more, I can confirm that it works smoothly with
libisabelle on Linux and OS X. However, I'm running into bootstrapping
problems under Windows. Namely, recovering symlinks causes an exception.
This time, I could even reproduce the problem on my local machine.

The error message is:

java.nio.file.NoSuchFileException:
C:\Users\appveyor\AppData\Local\libisabelle\setups\Isabelle2016-RC0\.\contrib\cygwin\dev\fd

Some more context:

<https://ci.appveyor.com/project/larsrh/libisabelle/build/56/job/gcsrus017n6o6on0#L1092>

In Isabelle <=2015 I just ignored the symlinks and bootstrapping still
worked (by accident?). For 2016, you moved this routine from isabelle.Main
to Isabelle_System.init, which I appreciate. But I don't understand the
above error at all, given that the file appears to exists.

Steps to reproduce:

Install sbt:
https://dl.bintray.com/sbt/native-packages/sbt/0.13.9/sbt-0.13.9.msi
git clone --recursive https://github.com/larsrh/libisabelle.git
In the clone, using administrative prompt (!): sbt
In sbt: Run "publishLocal" followed by "appBootstrap/run --version
2016-RC0"

Cheers
Lars

Email Gateway (Aug 22 2022 at 12:26):

From: Lars Hupel <hupel@in.tum.de>
I think I found the cause.

I use native Java 7+ APIs to unpack the distribution tarballs. In
particular, I use Java's facilities to create symlinks if I encounter one
in the tarball.

Now, for some reason, "contrib\cygwin\dev\fd" (and others) are broken
symlinks (I need to figure out why). But since these files are being
overwritten anyway, my suggestion would be to delete the file in
"recover_symlinks" before a buffered writer is created for it. Makarius,
what do you think?

Cheers
Lars

Email Gateway (Aug 22 2022 at 12:26):

From: Makarius <makarius@sketis.net>
On Wed, 6 Jan 2016, Lars Hupel wrote:

The error message is:

java.nio.file.NoSuchFileException:
C:\Users\appveyor\AppData\Local\libisabelle\setups\Isabelle2016-RC0\.\contrib\cygwin\dev\fd

I think I found the cause.

I use native Java 7+ APIs to unpack the distribution tarballs. In
particular, I use Java's facilities to create symlinks if I encounter
one in the tarball.

What is the outcome of that on Windows? The result needs to be a Cygwin
symlink, which is a funny special file for Windows.

Now, for some reason, "contrib\cygwin\dev\fd" (and others) are broken
symlinks (I need to figure out why).

The links points to /proc/self which presumably makes sense only for
Cygwin processes, not for the java process.

Makarius

Email Gateway (Aug 22 2022 at 12:26):

From: Lars Hupel <hupel@in.tum.de>

What is the outcome of that on Windows? The result needs to be a Cygwin
symlink, which is a funny special file for Windows.

Apparently those are NTFS symlinks.

Regardless of the actual outcome, deleting the file beforehand should be
safe, because the code to recover Cygwin symlinks truncates the files
anyway, i.e. in the worst case it's a redundant operation.

Cheers
Lars

Email Gateway (Aug 22 2022 at 12:26):

From: Makarius <makarius@sketis.net>
Should this be done on my side or on your side? In principle, the
assumption of Isabelle_System.init is that the distribution has been
unpacked as plain files on Windows, without any special Unix things.

The Isabelle_windows.tar.gz with symblinks violates that in some sense, so
maybe links should be removed by the release build process? (What you
have called "Wurstfabrik").

Makarius

Email Gateway (Aug 22 2022 at 12:27):

From: Lars Hupel <hupel@in.tum.de>

Should this be done on my side or on your side? In principle, the
assumption of Isabelle_System.init is that the distribution has been
unpacked as plain files on Windows, without any special Unix things.

I would prefer on your side. I try to avoid changing the copies of the
official Isabelle/Scala sources in libisabelle.

I was suggesting this patch:

--- a/src/Pure/System/cygwin.scala Wed Jan 06 16:17:50 2016 +0100
+++ b/src/Pure/System/cygwin.scala Thu Jan 07 13:30:33 2016 +0100
@@ -46,6 +46,7 @@
case link :: content :: rest =>
val path = (new JFile(isabelle_root, link)).toPath

Files.delete(path)
val writer = Files.newBufferedWriter(path, UTF8.charset)
try { writer.write("!<symlink>" + content + "\u0000") }
finally { writer.close }

The Isabelle_windows.tar.gz with symblinks violates that in some sense,
so maybe links should be removed by the release build process? (What
you have called "Wurstfabrik").

Of course, that would also work. I didn't think of that, but it's
probably the proper solution.

Cheers
Lars

Email Gateway (Aug 22 2022 at 12:27):

From: Lars Hupel <hupel@in.tum.de>
I forgot to add: This would also mean that administrative privileges are
not required any more for unpacking the Windows tarball (mere users are
not allowed to create symlinks).

Email Gateway (Aug 22 2022 at 12:28):

From: Makarius <makarius@sketis.net>
OK, I have changed it trivially as follows:
http://isabelle.in.tum.de/repos/isabelle/rev/8d5f2e3e836d

Makarius

Last updated: Apr 26 2024 at 12:28 UTC