Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ISABELLE_BROWSER_INFO

view this post on Zulip Email Gateway (Aug 22 2022 at 16:24):

From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
I am trying to change the directory where the browser info is generated.
I tried:

$ export ISABELLE_BROWSER_INFO=~
$ isabelle build -v -c -D .

and also

$ ISABELLE_BROWSER_INFO=~; isabelle build -v -c -D .

However the browser info is generated in the default directory:

~/.isabelle/Isabelle2017/browser_info/

I am using Isabelle2017 in Windows 10 (Cygwin-Terminal.bat)

The ROOT file contains:

chapter Test
session "Test" = "HOL" +
  options [browser_info, document = pdf, document_output = "output",
document_variants="document=-proof,-ML"]
  theories
     ...
  document_files
    "root.tex"

Best regards,

Viorel Preoteasa

view this post on Zulip Email Gateway (Aug 22 2022 at 16:25):

From: Makarius <makarius@sketis.net>
On 01/11/17 10:11, Viorel Preoteasa wrote:

I am trying to change the directory where the browser info is generated.
I tried:

$ export ISABELLE_BROWSER_INFO=~
$ isabelle build -v -c -D .

and also

$ ISABELLE_BROWSER_INFO=~; isabelle build -v -c -D .

Isabelle settings need to be changed inside the settings environment,
e.g. in $ISABELLE_HOME_USER/etc/settings

Here is an example:

ISABELLE_BROWSER_INFO="$USER_HOME/browser_info"

I am using Isabelle2017 in Windows 10 (Cygwin-Terminal.bat)

~ and $HOME are not well-defined here. $USER_HOME works for Isabelle on
all platforms.

An alternative is to pass a properly quoted '~' to Isabelle.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 16:26):

From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
On 11/2/2017 11:44 AM, Makarius wrote:

On 01/11/17 10:11, Viorel Preoteasa wrote:

I am trying to change the directory where the browser info is generated.
I tried:

$ export ISABELLE_BROWSER_INFO=~
$ isabelle build -v -c -D .

and also

$ ISABELLE_BROWSER_INFO=~; isabelle build -v -c -D .
Isabelle settings need to be changed inside the settings environment,
e.g. in $ISABELLE_HOME_USER/etc/settings

Here is an example:

ISABELLE_BROWSER_INFO="$USER_HOME/browser_info"
I would like to specify the ISABELLE_BROWSER_INFO for a specific
project, and if somebody else builds the project, then this setting
should be available without changing the Isabelle user settings. I used
~ (home) as an example. In fact I would like to specify the browser_info
relative to the location of the ROOT file. Similar to how 
document_output = "output" works when specified in the ROOT file.

Is this possible?

I am using Isabelle2017 in Windows 10 (Cygwin-Terminal.bat)
~ and $HOME are not well-defined here. $USER_HOME works for Isabelle on
all platforms.
As I said, I used ~ as an example. However if I do echo ~ it shows the
right path for me.

An alternative is to pass a properly quoted '~' to Isabelle.
How would I do this? As said I am interested in specifying a directory
relative to the location of the ROOT file, and I want to do be able to
do it for a specific project, not for all projects of a user. The main
goal is to have somebody else build the project, without modifying the
Isabelle user settings.

Viorel

view this post on Zulip Email Gateway (Aug 22 2022 at 16:27):

From: Makarius <makarius@sketis.net>
No. It will require another renovation of the whole setup, when HTML and
PDF documents are more unified.

Makarius

Last updated: Apr 19 2024 at 08:19 UTC