Andrew Helwer (Nov 27 2024 at 19:51): Andrew Helwer (Nov 27 2024 at 19:51):Hello! I am doing some development with the TLA+ proof manager (TLAPM https://github.com/tlaplus/tlapm) which embeds Isabelle as a backend theorem-prover to discharge obligations produced by the TLA+ proof language. Lately I was poking around to see why our releases take up so much space, and Isabelle comprised almost all of it. In particular, it seems to bundle an entire copy of the JDK, Haskell stack, Scala, some IDEs, etc. Does anybody have experience or pointers for slimming down Isabelle's storage footprint when it is embedded in this way? Thank you! Here is the related github issue: https://github.com/tlaplus/tlapm/issues/181
Mathias Fleury (Nov 27 2024 at 19:59):This is a non-trivial idea, mostly for the reason that Isabelle relies on specific version of tools like z3. Newer version do not work with Isabelle
Mathias Fleury (Nov 27 2024 at 20:01):I know that the nix people are bundling things differently ( https://github.com/jvanbruegge/nixpkgs/blob/d653b33f2083022e5e0bfad73002314570379ef1/pkgs/applications/science/logic/isabelle/default.nix)
Andrew Helwer (Nov 27 2024 at 20:10):It's understandable that it would bundle a specific version of Z3, and it would be interesting to see whether that version could be unified with the one used by TLAPM directly. However, things like the JDK or rsync could certainly be omitted in favor of the system version, right?
Fabian Huch (Nov 28 2024 at 16:14):Why would that be possible? Different versions of a software do different things.
Fabian Huch (Nov 28 2024 at 16:18):You can certainly try to mess with the system and change dependencies to arbitrary other versions, strip out system components, but you'll just end up with software that doesn't work (reliably).
Fabian Huch (Nov 28 2024 at 16:22):One GB of SSD space costs around 0.04€ -- I think this is a reasonable price to pay for Isabelle ;)
Mathias Fleury (Nov 28 2024 at 16:23):Andrew Helwer said:
It's understandable that it would bundle a specific version of Z3, and it would be interesting to see whether that version could be unified with the one used by TLAPM directly. However, things like the JDK or rsync could certainly be omitted in favor of the system version, right?
In our lecture, one person is writing code for Java 17 and it does not compile in Java 21. And we are talking about the code for an exercise that lasts one week, it is not a big project. So, why would a big Java project with many libraries work ?
Andrew Helwer (Nov 28 2024 at 16:32):Maybe I'm ignorant of how Isabelle works but why would it need to embed an entire version of the JDK unless it's compiling Java code? If the user has Java runtime version 21.0.3+ installed on their system then it will run anything compiled for JDK 21.0.3, until we get to 2040 and some lesser-used APIs for Java 21 are possibly removed from Java 35 or whatever the user might have on their system.
One GB of SSD space costs around 0.04€ -- I think this is a reasonable price to pay for Isabelle ;)
This is more about sensibilities but given that a stripped Debian install only clocks in at 150 MB if something takes up ten times that amount of space it should have a better reason than just storage being cheap.
Fabian Huch (Nov 28 2024 at 16:37):It does seem like you are a bit ignorant on how Isabelle and Java works:
Fabian Huch (Nov 28 2024 at 16:39):I am sure Isabelle could be made smaller. But is it the goal of the project? Not at all. The goal is to provide a theorem prover that works as well as possible, while running on hardware that people use.
Fabian Huch (Nov 28 2024 at 16:40):Even the official java website says:
Most Java applications will work with updated versions of Java. However some applications may break because of security related changes in Java
Fabian Huch (Nov 28 2024 at 16:46):If there is an actual problem (e.g., you are trying to run Isabelle on an embedded system) then I'm happy to discuss how to make it smaller.
Andrew Helwer (Nov 28 2024 at 17:14):We can skip the Java discussion because it's a bit different than what you present and Java is a VM-based language so one has to be careful to distinguish between compiling for a given JDK version and running on a given JVM version. But anyway. This conversation's tone is becoming a bit combative and defensive; this is easy to have happen in text-based communications so I would just like to restate my good will and I am not trying to criticize your project.
Let us also avoid discussion of whether 1.1 GB is a lot of space; there is no objective criterion to appeal to here so I will just say that the premise of this thread is that it is a lot of space, and I am interested in decreasing the space for an application where Isabelle is embedded within another application. If you think it is not a lot of space that is fine, but it is not a productive debate to have here. We can probably at least agree that if 90%+ of the compiled code shipped with a specific application (not Isabelle generally, just its embedding in TLAPM) is never run, then it would be nice if that code could be removed for that application.
I would like to refocus on what our project's use case is, which is translating proof obligations generated by TLA+ into forms that can be discharged by Isabelle. We probably do not need the entire capabilities of Isabelle for this. Certainly we do not need things like the various IDEs and rsync. I would be surprised if passing these obligations to Isabelle caused it to compile Java code but if that's how it works then that's how it works. Let's focus on a concrete example: how can something like JEdit be stripped from an Isabelle release?
Mathias Fleury (Nov 28 2024 at 17:15):IIRC (from downloading of components that I accidentally Control-C-ed during decompression), you can delete the content of the JEdit folder (the folder needs to exist however)
Mathias Fleury (Nov 28 2024 at 17:19):I think that you can safely delete:
- stack (haskell package manager):
- opam (ocaml package manager)
- mlton (ML compiler)
- napproche
- if you do not use sledgehammer: e, vampire, and zipperposition
(the rest I am not sure)
Mathias Fleury (Nov 28 2024 at 17:20):But, be warned, to know if you needed a component, you need to run into the situation where Isabelle is trying to execute it
Mathias Fleury (Nov 28 2024 at 17:21):so deleting the wrong thing will cause problems in strange ways
Fabian Huch (Nov 28 2024 at 17:36):No combative tone intended. I only have time to engage in some discussions, so it does matter to me whether something like this is 'just for fun' or actually relevant.
I am curious to learn how the java situation is different? The JDK contains the JVM.
You can strip components from Isabelle by modifying the Admin/components/main file. But the question which you need is a longer one as it depends on what you invoke in Isabelle.
irvin (Nov 29 2024 at 02:50):Mathias Fleury said:
IIRC (from downloading of components that I accidentally Control-C-ed during decompression), you can delete the content of the JEdit folder (the folder needs to exist however)
I think some more space could come from vscode deleted unless you use vscode or the lsp stuff that vscode provides from vim/emacs
Fabian Huch (Dec 11 2024 at 09:58):I just happened to look into how to build Isabelle2024/Pure on a minimal x86_64 linux. If that is all you need, then you should only require:
cat >contrib/jdk-21.0.3/etc/settings <<'EOF'
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
ISABELLE_JDK_HOME="<your-jdk-home>"
EOF
and delete the non-etc directories of the JDK component.
Fabian Huch (Dec 11 2024 at 10:00):Of course, if you want to run anything else, you'll need more components.
Last updated: Dec 21 2024 at 12:33 UTC