Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help with configuring Cygwin Home


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

From: "Pasupuleti, Vijay" <V.S.Pasupuleti@warwick.ac.uk>
Hi,

I am trying (but failing) to use Isabelle in conjunction with another tool, Symphony. My system runs Windows 7 OS. Let me just add that I could run Isabelle from the jEdit interface, on the ToyList example from the tutorial.
In order to do the above, I need to have write permissions to my Isabelle heaps directory, which is a subdirectory of the following location.

$USER_HOME/.isabelle

The directory $USER_HOME is nothing but the home directory as per Cygwin installation (that is what I gather, I could be wrong).
But this directory seems to be picked up from a network location, as the machine is part of a domain at the university.
I do not have write permissions to that directory, and would like to change it to a directory on my local drive.

Does anybody know how to do this? Thanks in anticipation.

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

From: Makarius <makarius@sketis.net>
On Wed, 16 Apr 2014, Pasupuleti, Vijay wrote:

I am trying (but failing) to use Isabelle in conjunction with another
tool, Symphony.

Can you say what Symphony is, and how it needs to be connected to
Isabelle? A quick web search gives the following
http://en.wikipedia.org/wiki/Symphony_%28software%29

I need to have write permissions to my Isabelle heaps directory, which
is a subdirectory of the following location.

$USER_HOME/.isabelle

The directory $USER_HOME is nothing but the home directory as per Cygwin
installation (that is what I gather, I could be wrong).

That is a bit odd. The separate $USER_HOME (instead of better known
$HOME) was introduced specifically for the purpose of Windows and Cygwin,
to refer to the normal Windows user home directory, not the one within the
Cygwin root.

We need to figure out where that $USER_HOME comes from. The default is
determined like this:

if [ -z "$USER_HOME" ]; then
USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
fi

This assumes that there is no other source for a different $USER_HOME and
that "$HOMEDRIVE\\$HOMEPATH" refer to the correct location.

But this directory seems to be picked up from a network location, as the
machine is part of a domain at the university. I do not have write
permissions to that directory, and would like to change it to a
directory on my local drive.

Does that mean Isabelle is installed centrally on a network drive? That
is basically OK -- it used to be done like that often in the past -- but
in recent years it came out of use since people usually have their private
machines.

Makarius


Last updated: Nov 21 2024 at 12:39 UTC