l4v: reduce l4v image size

- use default polyml32_64 builds, which go up to 16GB of heap size,
  which was the max before anyway. This should reduce heap size.

- remove vscodium component from cache (saves > 1GB)

- remove separate MLTon download, which is now an Isabelle component
  anyway

Signed-off-by: Gerwin Klein <[email protected]>

res/isabelle_settings

@@ -8,10 +8,12 @@
 init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
 init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/bundled"
 
-# 64 bit setup for large C proofs:
-ML_OPTIONS="-H 4096 --maxheap 16384"
-ML_PLATFORM=${OVERRIDE_ML_PLATFORM:-"$ISABELLE_PLATFORM64"}
-ML_HOME="$(dirname ${ML_HOME})/$ML_PLATFORM"
+# Start with a larger heap size
+ML_OPTIONS="-H 2048"
+
+# We no longer need 64 bit platform settings for running the L4v proofs, so we
+# leave ML_HOME etc untouched.
+
 ISABELLE_BUILD_OPTIONS=${OVERRIDE_ISABELLE_BUILD_OPTIONS:-"threads=4"}
 
 # Default to ARM l4v builds

scripts/l4v.sh

@@ -53,13 +53,6 @@ as_root apt-get install -y --no-install-recommends \
         python3-lxml \
         # end of list
 
-# looks like there is no Debian package for mlton any more
-MLTON=mlton-20210117-1.amd64-linux-glibc2.31
-wget https://github.com/MLton/mlton/releases/download/on-20210117-release/$MLTON.tgz
-tar  -xzC /opt -f $MLTON.tgz
-ln -s /opt/$MLTON opt/mlton
-rm $MLTON.tgz
-
 # Get l4v and setup isabelle
 try_nonroot_first mkdir "$ISABELLE_DIR" || chown_dir_to_user "$ISABELLE_DIR"
 ln -s "$ISABELLE_DIR" "$HOME/.isabelle"
@@ -68,6 +61,14 @@ mkdir -p "$HOME/.isabelle/etc"
 ISABELLE_SETTINGS_LOCATION="$HOME/.isabelle/etc/settings"
 cp "$NEW_ISABELLE_SETTINGS" "$ISABELLE_SETTINGS_LOCATION"
 
+# MLton is needed for the L4v C parser. It is a default component for Isabelle,
+# so we point PATH directly there. The component will only be available by
+# default if the cache below is installed or if the components are later
+# installed by the user. To run anything in L4v one has to install components,
+# so the path assignment here will be useful even without the cache.
+# The component name/version is stable enough to update manually when it changes.
+export PATH="/isabelle/contrib/mlton-20210117-1/x86_64-linux/bin/":"$PATH"
+
 if [ "$MAKE_CACHES" = "yes" ] ; then
     # Get a copy of the L4v repo, and build all the isabelle and haskell
     # components, so we have them cached.
@@ -77,6 +78,20 @@ if [ "$MAKE_CACHES" = "yes" ] ; then
         repo sync -c
         pushd l4v
             ./isabelle/bin/isabelle components -a
+
+            # Isabelle downloads tar.gz files, and then uncompresses them for
+            # its contrib. We don't need both the uncompressed AND decompressed
+            # versions, but Isabelle checks for the tarballs. To fool it, we now
+            # truncate the tars and save disk space. We also remove the large
+            # vscodium component, which is not needed for command line builds.
+            # This will lead to a warning when Isabelle starts, which is safe to
+            # ignore.
+            pushd "$HOME/.isabelle/contrib"
+                truncate -s0 ./*.tar.gz
+                rm -r vscodium-*
+                ls -lah  # show the evidence
+            popd
+
             pushd spec/haskell
                 make sandbox
             popd
@@ -86,14 +101,6 @@ if [ "$MAKE_CACHES" = "yes" ] ; then
     # Now cleanup the stuff we don't want cached
     rm -rf "$TEMP_L4V_LOCATION"
     as_root rm -rf /tmp/isabelle-  # This is a random tmp folder isabelle makes
-
-    # Isabelle downloads tar.gz files, and then uncompresses them for its contrib.
-    # We don't need both the uncompressed AND decompressed versions, but Isabelle
-    # checks for the tarballs. To fool it, we now truncate the tars and save disk space.
-    pushd "$HOME/.isabelle/contrib"
-        truncate -s0 ./*.tar.gz
-        ls -lah  # show the evidence
-    popd
 fi
 
 possibly_toggle_apt_snapshot