Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] distributed installation + sledgehammer file w...


view this post on Zulip Email Gateway (Aug 19 2022 at 15:54):

From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hi,

I use Isabelle for teaching and it was installed by an adjustment to the web-distribution for our Linux machines.
Now, I will need to use a lab running on Window, s and that created a few issues I couldn’t help our support team much.

1) distributed config setup:
Is there any suggested / configuration-setup for distributed installations of Isabelle (Linux or Windows)? The support
guy said, for example, the the Window installation asking for a directory would be a problem for an administered install.

In the end, I extracted the .exe and built HOL heaps and use that as a starting point to be shared (i.e. in the way Windows
lab is setup, that means running a shared copy of Isabelle remotely as local installations aren’t viable).

2) sledgehammer file write access:

This worked to a degree, but say, sledgehammer fails saying SysErr because of a file-write problem. Where is it SH is trying to write to?
Or in general, what would you suggest to make a distributed Windows installation viable for a teaching lab?

This is for Isabelle2014 on Windows 8.1

Many thanks.

Best,
Leo
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 15:54):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Leo,

By default, Sledgehammer should be trying to write to

ML {* getenv "ISABELLE_TMP" *}

a subdirectory that is created at startup and removed upon exit. Since this is used not only by Sledgehammer, but also by other Isabelle subsystems, I would recommend trying to find out what goes wrong there. I am not very familiar with Windows or Cygwin, but I presume the Isabelle's System manual ("isabelle doc system") would be a good starting point for investigations.

As a workaround for Sledgehammer, It is possible to specify another directory by adding

declare [[sledgehammer_atp_dest_dir = "/foo/bar/baz"]]

to the top of your theory file, or in an imported theory. If you already have a theory file with some basic setup for the students, this could go there.

Regards,

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 15:55):

From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hi Jasmin,

Many thanks for this, very helpful.

I had looked at the etc/settings file before, but not for Windows. I think the change to ISABELLE_TMP_PREFIX and ISABELLE_HOME_USER to a suitable directory for CS-support will suffice. Many thanks for pointing it out.

PS:
the whole thing came about because locally they had a last-minute change from a ready Linux-setup to what a new-Windows environment panic!
As I divorced myself from windows a while ago, was just in a helpless situation to advice support on what to do on short notice.

Thanks again.

Best,
Leo
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 15:55):

From: Makarius <makarius@sketis.net>
On Thu, 25 Sep 2014, Leo Freitas wrote:

I had looked at the etc/settings file before, but not for Windows. I
think the change to ISABELLE_TMP_PREFIX and ISABELLE_HOME_USER to a
suitable directory for CS-support will suffice.

These are indeed the two main Isabelle settings for user-specific material
that is written at run-time. The central ISABELLE_HOME/etc/settings may
be tweaked to change them.

Note that there is also USER_HOME as a platform-independent version of
HOME known from Unix.

the whole thing came about because locally they had a last-minute change
from a ready Linux-setup to what a new-Windows environment panic! As I
divorced myself from windows a while ago, was just in a helpless
situation to advice support on what to do on short notice.

In Isabelle2014 the default USER_HOME is based on HOMEDRIVE and HOMEPATH,
and ISABELLE_TMP_PREFIX is within the Cygwin /tmp (i.e. within the
installation directory). Both might need further refinements for
multi-user environments.

What we could need is some advice from a genuine Windows expert, to tell
where the canonical locations are in a networked environment.

Makarius


Last updated: Mar 28 2024 at 16:17 UTC