[isabelle] $HOME, $USER_HOME, and how I call "bin/isabelle" commands with batch/bash files



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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.