Reduce size of TLAPM release bundle

[ahelwer]

Currently, TLAPM releases are enormous; on Linux they take up 473 MB zipped and 1.1 GB unzipped, while on macOS they take up 668 MB zipped and 1.5 GB unzipped. This seems far, far larger than should be necessary. Unzipping a Linux TLAPM release, we have the following notably-large components:

/
├── (57  MB) bin/
│   ├── (17  MB) tlapm
│   ├── (37  MB) tlapm_lsp
│   └── (3.6 MB) translate
└── (1.1 GB) lib/tlapm/backends/
    ├── (36  MB) bin/
    │   ├── (1.5 MB) ls4
    │   ├── (3.6 MB) ptl_to_trp
    │   ├── (26  MB) z3
    │   └── (5.1 MB) zenon
    └── (1.1 GB) Isabelle/
        ├── (33  MB) heaps/polyml-5.9.1_x86_64_32-linux/
        │   ├── (23  MB) Pure
        │   └── (9.1 MB) TLA+
        ├── (71  MB) src/
        ├── (9.6 MB) lib/classes/
        │   └── (9.6 MB) isabelle.jar
        └── (903 MB) contrib/
            ├── (355 MB) jdk-21.0.3
            ├── (84  MB) stack-2.15.5
            ├── (61  MB) mlton-20210117-3
            ├── (56  MB) jedit-20240425
            ├── (48  MB) polyml-5.9.1
            ├── (36  MB) naproche-20240519
            ├── (27  MB) e-3.0.03-1
            ├── (23  MB) vampire-4.8
            ├── (21  MB) cvc4-1.8
            ├── (19  MB) pdfjs-2.14.305
            ├── (17  MB) jfreechart-1.5.3
            ├── (15  MB) zipperposition-2.1-1
            ├── (14  MB) z3-4.4.0pre-4
            ├── (14  MB) sqlite-3.45.2.0
            ├── (11  MB) rsync-3.2.7-1
            ├── (6.7 MB) zstd-jni-1.5.5-4
            ├── (6.0 MB) verit-2021-06.2-rmx-1
            └── (5.9 MB) opam-2.0.7

There are a few smaller candidates for removal:

• tlapm_lsp; does it need to be there it should it be a separate OPAM package?
• The entirety of the Isabelle/src directory

Of course by far the largest size contributor is the Isabelle/contrib/ directory, which includes full versions of the JDK, Haskell, StandardML, Scala, a second version of Z3, and a bunch of command-line tools & editors that TLAPM would seemingly have no use for. So cutting those out where possible seems like the most effective way to greatly reduce the size of the release binary.

[ahelwer]

I have asked about this on the Isabelle zulip here: https://isabelle.zulipchat.com/#narrow/channel/202961-General/topic/Embedding.20Isabelle.20in.20another.20prover.20-.20how.20to.20reduce.20size.3F/near/484789342

[kape1395]

• tlapm_lsp should be distributed along with the tlapm if vscode is considered the target IDE.
• I spent some time trying to reduce the Isabelle part by avoiding Java, but it seems it is now on the critical path and it would be hacking to overrule it. Maybe other parts could be stripped down.
• Ofc jedit could be dropped, probably (I thought I has done it).

[muenchnerkindl]

AFAIK we need polyml and probably bash_process and gnu_utils from Isabelle/contrib. As @kape1395 says, Isabelle may now complain if it doesn't see Java, although we don't need it (its absence previously resulted in a warning that could be ignored). From Isabelle/src, we need Provers, Pure, and (some parts of) Tools. It should not be necessary to include the heaps in the distribution as they are (or can be) rebuilt. Isabelle/doc can also be removed if it is included in the distribution.

[ahelwer]

@muenchnerkindl in the zulip thread they said Isabelle actually compiles Java code during the normal course of operation which is why the JDK is bundled with it; do you think the way TLAPM uses Isabelle would require it to compile Java code? I'm unfamiliar with the Isabelle toolchain although do hope to learn the basics within the next year or so!

[muenchnerkindl]

No, Isabelle/TLA+ doesn't rely on Java, but it may well be that the Isabelle binary checks if Java is present and doesn't start otherwise.