Hanna Lachnitt (Nov 10 2024 at 20:56): Hanna Lachnitt (Nov 10 2024 at 20:56):Hi everyone,
I am sure this has been asked before but I don't really know how to find it, so please feel free to send a link. I am using a slightly modified version of Isabelle so if something seems off it might also be that. Pinging @Mathias Fleury since he knows more about what is different in that version.
This question is about how to build a session without Isabelle writing to the home directory.
Basically, I have an Isabelle theory that I want to run on a set of benchmarks. The way this works on the cluster I am using is that for each benchmark, the benchmark and the theory file are copied into their own directory. I am writing the file dynamically so I have to copy it into the directory.
For now I wrote my script in a way that it copies not only the theory file but the whole directory it is in including the ROOT file. Then, I try to build the session with Isabelle and that is where my trouble start. If I leave the HOME directory as it is Isabelle will try to write to $HOME/.isabelle/heaps/polyml.../ (as far as I understand) which is forbidden in this situation.
On the other hand if I set the Home directory (globally I am not sure how I would change it just for Isabelle) to the new folder, Isabelle will complain about the missing JAVA_HOME. While I see that I could re-download all dependencies I really don't want to do that for every benchmark. I also don't want to rebuild all session images that came before my new session but I guess there might be an option to avoid that anyways. I've tried to add the original directory as a component but that did not work.
I saw that there is a command line option -o system_heaps but that just writes the files to ISABELLE_HEAPS_SYSTEM which is still not helpful for me. I read the system manual (without understanding much unfortunately) and tried -e with an example from the ROOT file of HOL but that did also not do this.
irvin (Nov 11 2024 at 00:47):for the $HOME/.isabelle/contrib im pretty sure you can set that manually using the ISABELLE_COMPONENTS_BASE variable. by default its set to "$USER_HOME/.isabelle/contrib" thou im not sure about the heap part. you could also just copy $HOME/.isabelle whenever you set the home directory globally. AFAIK most modern filesystems are smart enough to optimize this copy away
irvin (Nov 11 2024 at 00:52):You can also modify the ISABELLE_HEAPS_SYSTEM variable if your using a repo version as i dont think there are any system heaps on the repo version
Hanna Lachnitt (Nov 15 2024 at 01:30):Thanks, I will try that
Last updated: Dec 21 2024 at 12:33 UTC