Email Gateway (Aug 19 2022 at 15:54): 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
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
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
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: Nov 21 2024 at 12:39 UTC