Email Gateway (Aug 22 2022 at 16:24): 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
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
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/settingsHere 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
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: Nov 21 2024 at 12:39 UTC