Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] $HOME, $USER_HOME, and how I call "bin/isabell...


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

From: gottfried.barrow@gmx.com
With Isabelle2011, I used $HOME to change my home folder for Cygwin, and
used $HOME to set the root path for $ISABELLE_HOME_USER.

Now, in Isabelle2012, $USER_HOME is used to set the path for
$ISABELLE_HOME_USER, as shown in system.pdf.

I finally figured out that $USER_HOME is used, but it wasn't obvious
that "Isabelle2012-RC3\contrib\cygwin-1.7.9" was using the $HOME folder
that I was setting it to. It is, so I don't have any questions now.

However, I'll show how I call "bin/isabelle" commands through a
combination of a batch file and a bash file, which I do so that I don't
have to start a Cygwin command window, and then type in something like
"isabelle jedit" in Cygwin.

This is also related to the fact that my Norton 360 anti-virus deletes
my "Isabelle2012-RC3\Isabelle.exe", though it's not a problem for me,
because I prefer to change my Isabelle home folder anyway.

To call jEdit, and change my home folders, I put this in
"isajedit-2012.bat":

set HOME=E:\E_main\02-p\pi\homewin
set USER_HOME=/cygdrive/e/E_main/02-p/pi/homewin
set ISAVERSION=Isabelle2012-RC3
set PATH=E:\E_main2\binp\%ISAVERSION%\bin;%PATH%
set CHERE_INVOKING=true
start /min
E:\E_main2\binp\%ISAVERSION%\contrib\cygwin-1.7.9\bin\bash --login -i
%HOME%\bin\isajedit.bash

The corresponding "isajedit.bash" that the batch file uses contains this:

#!/usr/bin/env bash
#
########################################################
# $ISAVERSION is set in the batch file that calls this.
########################################################
printenv
/cygdrive/e/E_main2/binp/$ISAVERSION/bin/isabelle jedit

In trying to figure out what path Isabelle was using for my home, I
created a similar batch file to the above, and I put this in
"isainfo.bash" for the batch file to use:

#!/usr/bin/env bash
#
########################################################
# $ISAVERSION is set in the batch file that calls this.
########################################################

ISASCRIPT="/cygdrive/e/E_main2/binp/$ISAVERSION/bin/isabelle"
printenv
$ISASCRIPT usedir --help
$ISASCRIPT getenv ISABELLE_USEDIR_OPTIONS
$ISASCRIPT getenv USER_HOME
$ISASCRIPT getenv ISABELLE_HOME_USER

Anyway, such batch file and bash file combinations may be useful to
someone using Cygwin.

--GB

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

From: Makarius <makarius@sketis.net>
You can also imitate what the Launch4j wrapper does, see the included
config file of it. With a fixed directory location one should be able to
turn the whole .exe into a plain Windows application alias.

The JVM entry point is src/Pure/System/main.scala and the init function in
src/Pure/System/isabelle_system.scala -- it basically redirects HOME to
user.home given by the JVM.

This hint is only for Isabelle2012 -- I might find new ways to makes
things simpler and more robust over time.

Makarius
isabelle.xml


Last updated: Apr 25 2024 at 04:18 UTC