Qiyuan Xu (Mar 24 2025 at 06:59): Qiyuan Xu (Mar 24 2025 at 06:59):This is very confusing.
Execute the following shell script
export ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx64g -Xss64m"
isabelle getenv -b ISABELLE_TOOL_JAVA_OPTIONS
# the ISABELLE_TOOL_JAVA_OPTIONS is unchanged!
Let's try another way
ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx64g -Xss64m" isabelle getenv -b ISABELLE_TOOL_JAVA_OPTIONS
# It is still not changed!
It's very annoying. How can I change this stubborn environment variable?
Qiyuan Xu (Mar 24 2025 at 07:05):Okay, I see Isabelle's system.pdf
These variables are not in-
tended to be set directly from the shell, but are provided by Isabelle compo-
nents within their settings files, as explained below.
Sorry, but I must complain, this is really a terrible design. The reference manual admits, "okay, this is an environment variable" but a variable that is very unconventional and cannot changed from the shell environment.
Qiyuan Xu (Mar 24 2025 at 07:18):at least some warning or error message should be given because it is very easy to make mistakes here. But everything just silently works, and no one can realize, "oh damn, I didn't properly set the environment variable". No one could have imagined that Isabelle cannot support such conventional things.
Qiyuan Xu (Mar 24 2025 at 07:28):Okay, I tried to add a local settings file under the root path of my project
my-project/
|- etc
|- settings
|- ROOT
Now, if I directly run isabelle build -D. MY_PROJECT, etc/settings will not be loaded and the building process will not use any env var settings in the file.
Unless you add my-project into Isabelle's components, the etc/settings will not take effect.
This is also confusing and more like a bug because I did say -D. MY_PROJECT, which should reasonably load the etc/settings.
Mathias Fleury (Mar 24 2025 at 07:41):why would you ever set java options for a component and not globally?
Mathias Fleury (Mar 24 2025 at 07:42):~/.isabelle/etc/settings or ~/.isabelle/Isabelle2025/etc/settings is the place to put those settings
Qiyuan Xu (Mar 24 2025 at 07:42):because 4GB mem is too small. I'm working on some machine learning experiment (especially reinforcement learning) and it would be beneficial to make a heap image for the entire AFP. So, I'm using a supercomputer (200GB+ mem) to build a very large bunch of theories (~2.4k theories). In this case, the default 4GB Java mem is far for sufficiency
Mathias Fleury (Mar 24 2025 at 07:43):So far, while I have hit similar issues, it was only in places where I was like "Yeah, okay, this is something that I (as a expert want) but is too easy to misuse"
Mathias Fleury (Mar 24 2025 at 07:44):Qiyuan Xu said:
because 4GB mem is too small. I'm working on some machine learning experiment (especially reinforcement learning) and it would be beneficial to make a heap image for the entire AFP. So, I'm using a supercomputer (200GB+ mem) to build a very large bunch of theories (~2.4k theories). In this case, the default 4GB Java mem is far for sufficiency
… so the global etc/settings is what you want to have as sane option on that supercomputer
Qiyuan Xu (Mar 24 2025 at 07:44):Certainly you can put
them into ~/.isabelle/Isabelle2025/etc/settings globally, but this kind of setting should (ideally) be set locally only
Mathias Fleury (Mar 24 2025 at 07:45):… No, I don't think so.
Mathias Fleury (Mar 24 2025 at 07:45):whenever you are on this computer you want the more memory
Qiyuan Xu (Mar 24 2025 at 07:53):well, this session is the only huge one that requires a lot of Java mem. In other cases, I'd prefer to leave memory to Poly/ML. For this reason, we don't want the Java to consume too much memory right? and want its GC more eagle to save mem. Therefore, I cannot set this globally.
Anyway, where to put the setting file, this is really a small matter because I'm using some scripts and can always remove / reset the global setting.
The thing is, for almost 100% engineers, if you mention environment variables to them, they will want to change them by VAR=xxx command or export VAR = xxx; command. Certainly, it's okay to have some special design to use some setting files, but the env var settings from the shell environment should also take effect because this is what is conventional and engineers would expect. If you want to introduce some unconventional things, it would be definitely appreciated if you warn users when they make mistakes.
Fabian Huch (Mar 24 2025 at 08:33):Qiyuan Xu said:
In other cases, I'd prefer to leave memory to Poly/ML. For this reason, we don't want the Java to consume too much memory right?
No, Poly/ML is optimized for 16GB of heap memory max. Unless you explicitly change the ML system, it won't even be able to use more than that due to how values are represented.
Fabian Huch (Mar 24 2025 at 08:33):And be aware that changing this can have drastic performance implications.
Fabian Huch (Mar 24 2025 at 08:36):Qiyuan Xu said:
The thing is, for almost 100% engineers, if you mention environment variables to them, they will want to change them by
VAR=xxx commandorexport VAR = xxx; command. Certainly, it's okay to have some special design to use some setting files, but the env var settings from the shell environment should also take effect because this is what is conventional and engineers would expect. If you want to introduce some unconventional things, it would be definitely appreciated if you warn users when they make mistakes.
Engineers maybe, but this is theorem proving: We don't want our environment to be polluted by implicit variables (and the manual does warn you).
Mathias Fleury (Mar 24 2025 at 08:37):Xmx states a maximum memory usage, not a minimum. So you are likely to not see a change by setting the option.
Qiyuan Xu (Mar 24 2025 at 10:38):Fabian Huch said:
Qiyuan Xu said:
The thing is, for almost 100% engineers, if you mention environment variables to them, they will want to change them by
VAR=xxx commandorexport VAR = xxx; command. Certainly, it's okay to have some special design to use some setting files, but the env var settings from the shell environment should also take effect because this is what is conventional and engineers would expect. If you want to introduce some unconventional things, it would be definitely appreciated if you warn users when they make mistakes.Engineers maybe, but this is theorem proving: We don't want our environment to be polluted by implicit variables (and the manual does warn you).
Hi, Fabian, I agree with the need to keep a specialized environment. I don't want to change the current design but only hope to add warning messages in the command line interface if the actual values taken by the system are different from the real environment variables.
Moreover, environment variable is a defined term that has a specific meaning in today's computer systems. You cannot call a variable as an environment variable just because it is determined by the environment. If the variables in Isabelle cannot be changed by the OS interfaces for environment variables, they are not environment variables but merely configuration variables. The system document shouldn't call them environment variables, which is a big misleading.
Fabian Huch (Mar 24 2025 at 12:16):I agree that a warning could be useful. In what sense do Isabelle environment variables not adhere to the POSIX standard?
Fabian Huch (Mar 24 2025 at 12:19):It specifically allows user-defined special implementations as well as readonly variables.
Last updated: Apr 18 2025 at 20:21 UTC