Jakub Kądziołka (Jan 27 2021 at 18:41): Jakub Kądziołka (Jan 27 2021 at 18:41):I'm managing my Isabelle installation with the Nix package manager. Each time I update, Isabelle decides to rebuild the heap images for Pure and HOL. I suspect that this might be because the path to the isabelle installation changes each time, but I don't understand why that would affect this - Isabelle ships with heap images in the tarball, and they get picked up regardless of the installation directory. How can I debug this?
Jakub Kądziołka (Jan 27 2021 at 18:43):(the reason this is quite annoying for me is that the build takes so much RAM that I cannot simply run it in the background. Is the required RAM an intrinsic property of the process, or could it be reduced by, for example, reducing the parallelism or something?)
Mathias Fleury (Jan 27 2021 at 18:49):https://arxiv.org/pdf/1805.07195.pdf the remote_build tools makes it possible to compile remotely. So I don't believe that the path is important
Mathias Fleury (Jan 27 2021 at 18:50):How drastic is your nix setup? Do you use the default components or do you also use the nix-provided version of the components?
Mathias Fleury (Jan 27 2021 at 18:51):(I believe that at least the polyml version is included in the heap, so a change in that wll cause a new compilation)
Jakub Kądziołka (Jan 27 2021 at 18:52):re: remote_build - interesting, is it possible to set up jedit so that the heap builds it starts use remote_build too?
Jakub Kądziołka (Jan 27 2021 at 18:53):I'm using the package from nixpkgs, not sure whether they pin the polyml
Mathias Fleury (Jan 27 2021 at 18:53):I don't think so, but I have never used remote_build
Mathias Fleury (Jan 27 2021 at 18:54):but usually you know what sessions you use (because you start the session every day)
Jakub Kądziołka (Jan 27 2021 at 18:54):however, both the old and new heaps are in ~/.isabelle/Isabelle2020/heaps/polyml-5.8.1_x86_64-linux, so the polyml version seems to match
Mathias Fleury (Jan 27 2021 at 18:58):Sadly, I don't use nix. Could you try isabelle env before and after your next update and see if there is any difference (for example by git diff --no-index old new)?
Mathias Fleury (Jan 27 2021 at 19:03):If you use https://github.com/NixOS/nixpkgs/blob/master/pkgs/applications/science/logic/isabelle/default.nix, then Nix is really using its own components. So the only person who understands the low-level isabelle part will tell you to use the nicely packaged isabelle version
Jakub Kądziołka (Jan 27 2021 at 19:07):The problem with that is that the packaged Isabelle doesn't work as-is because the dynamic libraries don't exist at the expected locations :D
Jakub Kądziołka (Jan 27 2021 at 19:14):Got an isabelle env diff, only some paths changed their hash
Lukas Stevens (Jan 27 2021 at 19:17):I am also using nix without problems. I maintain my own nix expression (forked from the one in nixpkgs), though. See here: https://github.com/lukasstevens/dotfiles/blob/master/nix/isabelle/default.nix
Lukas Stevens (Jan 27 2021 at 19:18):You will also need an updated version of polyml: https://github.com/lukasstevens/dotfiles/blob/master/nix/polyml/default.nix
Lukas Stevens (Jan 27 2021 at 19:19):Those expressions are still up to date (Isabelle2020)
Lukas Stevens (Jan 27 2021 at 19:21):One could improve the expressions by also managing the isabelle settings and preferences
Jakub Kądziołka (Jan 27 2021 at 19:23):I don't see any relevant differences between your expression and the one in nixpkgs...
Jakub Kądziołka (Jan 27 2021 at 19:23):it also seems that the polyml in nixpkgs is newer
Lukas Stevens (Jan 27 2021 at 19:24):Yeah, back when I created those it was outdated in nixpkgs.
Lukas Stevens (Jan 27 2021 at 19:24):And some minor changes where necessary from Isabelle2019 -> Isabelle2020
Lukas Stevens (Jan 27 2021 at 19:25):The polyml version is the version that Isabelle2020 is shipped with.
Jakub Kądziołka (Jan 27 2021 at 19:26):the one on my plain-old-Debian computer is also using 5.8.1, you seem to be using 5.8
Lukas Stevens (Jan 27 2021 at 19:27):You can reduce RAM usage by setting ML_OPTIONS="--maxheap 8G" in ~/.isabelle/Isabelle2020/etc/settings. Although for large sessions this won't help you much and the process will just be killed.
Jakub Kądziołka (Jan 27 2021 at 19:28):what's the default maxheap?
Lukas Stevens (Jan 27 2021 at 19:30):Not really sure. I think as much as possible.
Lukas Stevens (Jan 27 2021 at 19:31):But since Linux deals with OOM situations badly that backfires often.
Manuel Eberl (Jan 27 2021 at 19:39):I don't think I would recommend using your own version of components (JDK, PolyML, etc.) instead of the ones that Isabelle ships with.
Lukas Stevens (Jan 27 2021 at 19:39):Conceptually, it is better to do that, though.
Jakub Kądziołka (Jan 27 2021 at 19:39):AFAICS nixpkgs matches the versions used by the actual release
Lukas Stevens (Jan 27 2021 at 19:39):I don't think it does for z3
Lukas Stevens (Jan 27 2021 at 19:40):This often leads to broken smt proofs. Thats my hunch on why that happens for me anyways
Manuel Eberl (Jan 27 2021 at 19:41):I just remember all kinds of problems arising from this kind of repackaging. People ask on the mailing list because something crashes or doesn't work and after some interrogation it transpires it's because of some repackaging issue and Makarius gets really annoyed by this because he wasted time tracking down an issue that only arises because people did something he specifically advises against.
Jakub Kądziołka (Jan 27 2021 at 19:41):Lukas Stevens said:
This often leads to broken smt proofs. Thats my hunch on why that happens for me anyways
It didn't earlier, now does
Jakub Kądziołka (Jan 27 2021 at 19:42):and it does fix some smt proofs
Lukas Stevens (Jan 27 2021 at 19:42):Manuel Eberl said:
I just remember all kinds of problems arising from this kind of repackaging. People ask on the mailing list because something crashes or doesn't work and after some interrogation it transpires it's because of some repackaging issue and Makarius gets really annoyed by this because he wasted time tracking down an issue that only arises because people did something he specifically advises against.
On has to say that this approach to packaging is not really sustainable (at least if many applications would do it).
Lukas Stevens (Jan 27 2021 at 19:43):It would be quite easy to pin the versions with nix on the other hand.
Lukas Stevens (Jan 27 2021 at 19:46):Thanks for making me aware. I am now using Isabelle from nixpkgs again.
Jakub Kądziołka (Jan 27 2021 at 19:47):oh well, I guess one day this will annoy me enough for me to figure out how and where to put the printfs to debug this further
Lukas Stevens (Jan 27 2021 at 19:48):Manuel Eberl said:
I just remember all kinds of problems arising from this kind of repackaging. People ask on the mailing list because something crashes or doesn't work and after some interrogation it transpires it's because of some repackaging issue and Makarius gets really annoyed by this because he wasted time tracking down an issue that only arises because people did something he specifically advises against.
Even further it is just not possible to run Isabelle on NixOS without patching it up first (at least not without ugly workarounds like FHSuserenv). Of course, the nix package also replaces some dependencies by their system versions (which may cause problems).
Lukas Stevens (Jan 27 2021 at 19:55):Do you also need to rebuild the heap images if the Isabelle or PolyML version do not change? It seems weird to me because I never had the problem before and the paths should not change as well when the hash stays the same.
Jakub Kądziołka (Jan 27 2021 at 19:58):I mean, the hash changes quite often because the dependency graph is quite deep
Lukas Stevens (Jan 27 2021 at 20:00):Ok, maybe it was just because I didn't pay much attention to it.
Jakub Kądziołka (Feb 09 2021 at 08:55):I just stumbled upon the line external_file "$POLYML_EXE" in ML_Bootstrap.thy. Does this mean that the hash of the PolyML binary is a dependency?
Mathias Fleury (Feb 09 2021 at 09:55):Stupid question: isn't polyml saving structure (used to save heaps), version-dependent? (Independently of what external_file does)
Jakub Kądziołka (Feb 09 2021 at 11:07):yes, but the polyml version in question wasn't changing - just some paths embedded in the polyml binary
Last updated: Dec 07 2024 at 16:22 UTC