Email Gateway (Aug 22 2022 at 15:27): Email Gateway (Aug 22 2022 at 15:27):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi,
I tried to install Isabelle for Windows on a network drive -- so that I
wouldn't need to install it on several machines.
Upon extracting it ran correctly, even it opened the last file I visited
with my local install.
Upon subsequent running at first I got
'/etc/hosts' -> '/cygdrive/c/Windows/System32/drivers/etc/hosts'
'/etc/protocols' -> '/cygdrive/c/Windows/System32/drivers/etc/protocol'
'/etc/services' -> '/cygdrive/c/Windows/System32/drivers/etc/services'
'/etc/networks' -> '/cygdrive/c/Windows/System32/drivers/etc/networks'
find: 'setfacl': No such file or directory
find: 'setfacl': No such file or directory
xargs: chmod: No such file or directory
at second
/cygdrive/q/Hallgato/BG/Isabelle/Isabelle2016-1/bin/isabelle: sor: 57:
/cygdrive/q/Hallgato/BG/Isabelle/Isabelle2016-1/bin/isabelle: Permission
denied
/cygdrive/q/Hallgato/BG/Isabelle/Isabelle2016-1/bin/isabelle: 57. sor: exec:
/cygdrive/q/Hallgato/BG/Isabelle/Isabelle2016-1/bin/isabelle: nem hajtható
végre: Permission denied
and at third
/usr/bin/env: "bash": No such file or directory
Is this a planned use case for Isabelle?
For the second error message I fired my local 2016-1 cygwin terminal, it
said
gbuday@sztge3124 /cygdrive/q/Hallgato/BG/Isabelle/Isabelle2016-1/bin
$ ls -l
total 9
-rwxrwx---+ 1 Unknown+User Unknown+Group 1176 Dec 12 15:03 isabelle
-rwxrwx---+ 1 Unknown+User Unknown+Group 1962 Dec 12 15:03 isabelle_java
-rwxrwx---+ 1 Unknown+User Unknown+Group 503 Dec 12 15:03
isabelle_scala_script
As I am not an adminsitrator for the network drive, I could not modify the
owner of the Isabelle files.
Background information: I mount the network drive for writing as a different
user than my login user.
Is there an easy solution for this problem?
Email Gateway (Aug 22 2022 at 15:27):From: Lawrence Paulson <lp15@cam.ac.uk>
Hi Gergely,
Quite apart from your issues, I should mention that the last time I tried this, the use of a network drive caused a huge performance hit (three times slower). That was using NFS under Linux. Maybe things are better now.
Best,
Larry Paulson
Email Gateway (Aug 22 2022 at 15:27):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Prof. Paulson,
that matters, yes, for serious development,
but this would be classroom use where this was the easiest way of
installation
and I would run the most basic examples which could work well even in this
setting.
Email Gateway (Aug 22 2022 at 15:27):From: Makarius <makarius@sketis.net>
On 10/05/17 09:50, Gergely Buday wrote:
I tried to install Isabelle for Windows on a network drive -- so that I
wouldn't need to install it on several machines.
I use Windows network shares myself routinely in a limited testing
environment: Virtualbox running Windows 7 and various directories
mounted via SMB. So in principle it should work, but there are other
variations on Windows networking that cause problems.
Upon extracting it ran correctly, even it opened the last file I visited
with my local install.Upon subsequent running at first I got
'/etc/hosts' -> '/cygdrive/c/Windows/System32/drivers/etc/hosts'
'/etc/protocols' -> '/cygdrive/c/Windows/System32/drivers/etc/protocol'
'/etc/services' -> '/cygdrive/c/Windows/System32/drivers/etc/services'
'/etc/networks' -> '/cygdrive/c/Windows/System32/drivers/etc/networks'
find: 'setfacl': No such file or directory
find: 'setfacl': No such file or directory
xargs: chmod: No such file or directory
This belongs to the Cygwin.init operation that should only run once,
when the Isabelle application is started for the first time -- usually
right after extracting the 7zip sfx installer. You can see the details here
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2016-1/src/Pure/System/cygwin.scala#l18
with isabelle/postinstall at the bottom, see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/Admin/Windows/Cygwin/isabelle/postinstall
To avoid such complications with file system permissions on Windows, you
could first unpack to a local directory -- and also ensure that the
logic image is built properly (plus any other logic image that the users
might need later, e.g. via "isabelle build -b -s" in the Isabelle Cygwin
Terminal).
Then you copy the whole Isabelle directory to the network share: it is
used strictly read-only afterwards.
Makarius
Last updated: Apr 25 2024 at 01:08 UTC