Stream: Beginner Questions

Topic: Debugging heap rebuilds


view this post on Zulip 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?

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Jakub Kądziołka (Jan 27 2021 at 18:53):

I'm using the package from nixpkgs, not sure whether they pin the polyml

view this post on Zulip Mathias Fleury (Jan 27 2021 at 18:53):

I don't think so, but I have never used remote_build

view this post on Zulip Mathias Fleury (Jan 27 2021 at 18:54):

but usually you know what sessions you use (because you start the session every day)

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Jan 27 2021 at 19:14):

Got an isabelle env diff, only some paths changed their hash

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:19):

Those expressions are still up to date (Isabelle2020)

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:21):

One could improve the expressions by also managing the isabelle settings and preferences

view this post on Zulip 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...

view this post on Zulip Jakub Kądziołka (Jan 27 2021 at 19:23):

it also seems that the polyml in nixpkgs is newer

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:24):

Yeah, back when I created those it was outdated in nixpkgs.

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:24):

And some minor changes where necessary from Isabelle2019 -> Isabelle2020

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:25):

The polyml version is the version that Isabelle2020 is shipped with.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jakub Kądziołka (Jan 27 2021 at 19:28):

what's the default maxheap?

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:30):

Not really sure. I think as much as possible.

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:31):

But since Linux deals with OOM situations badly that backfires often.

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:39):

Conceptually, it is better to do that, though.

view this post on Zulip Jakub Kądziołka (Jan 27 2021 at 19:39):

AFAICS nixpkgs matches the versions used by the actual release

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:39):

I don't think it does for z3

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Jan 27 2021 at 19:42):

and it does fix some smt proofs

view this post on Zulip 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).

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:43):

It would be quite easy to pin the versions with nix on the other hand.

view this post on Zulip Lukas Stevens (Jan 27 2021 at 19:46):

Thanks for making me aware. I am now using Isabelle from nixpkgs again.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Jakub Kądziołka (Jan 27 2021 at 19:58):

I mean, the hash changes quite often because the dependency graph is quite deep

view this post on Zulip Lukas Stevens (Jan 27 2021 at 20:00):

Ok, maybe it was just because I didn't pay much attention to it.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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: Sep 25 2021 at 09:17 UTC