From ee5881f4217ca330210e17e67a4c4a4768444e8b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 12 Feb 2024 15:43:02 +1100 Subject: [PATCH 1/2] isabelle: remove obsolete settings Signed-off-by: Gerwin Klein --- res/isabelle_settings | 20 +------------------- 1 file changed, 1 insertion(+), 19 deletions(-) diff --git a/res/isabelle_settings b/res/isabelle_settings index d32e85d..f15d2b2 100644 --- a/res/isabelle_settings +++ b/res/isabelle_settings @@ -17,28 +17,10 @@ ISABELLE_BUILD_OPTIONS=${OVERRIDE_ISABELLE_BUILD_OPTIONS:-"threads=4"} # Default to ARM l4v builds L4V_ARCH=${L4V_ARCH:-"ARM"} -# Heap input locations. We have a unique set of heap files for each copy of -# Isabelle the user has checked out, so that users can have multiple sessions -# running at the same time without too many problems. -# Also check if we're running under Bamboo. If so, add the plan key, so the heaps -# don't conflict. (the ${...+x} is just a way to check if it's set) -if [ ! -z ${bamboo_planKey+x} ]; then - PATH_PREFIX="${bamboo_planKey}-" -fi -USER_HEAPS=${OVERRIDE_USER_HEAPS:-"/isabelle/${PATH_PREFIX:-}${L4V_ARCH}"} +USER_HEAPS=${OVERRIDE_USER_HEAPS:-"/isabelle/${L4V_ARCH}"} ISABELLE_OUTPUT=${OVERRIDE_ISABELLE_OUTPUT:-"$USER_HEAPS"} ISABELLE_PATH=${OVERRIDE_ISABELLE_PATH:-"$USER_HEAPS"} ISABELLE_HEAPS=${ISABELLE_OUTPUT} ISABELLE_BROWSER_INFO=${OVERRIDE_ISABELLE_BROWSER_INFO:-"$ISABELLE_HOME_USER/browser_info"} -JEDIT_JAVA_SYSTEM_OPTIONS="$JEDIT_SYSTEM_OPTIONS" # 2016 - -ISABELLE_BUILD_JAVA_OPTIONS="-Xms2048m -Xmx6096m -Xss4m" -JEDIT_JAVA_OPTIONS="-Xms128m -Xmx4096m -Xss4m" - -ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components" - -# SORRY_BITFIELD_PROOFS="1" -#SKIP_REFINE_PROOFS="1" SKIP_DUPLICATED_PROOFS="1" - From ee33c88658a9519209416c68565c3c15b26f659f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 10 Feb 2024 11:35:33 +1100 Subject: [PATCH 2/2] 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 --- res/isabelle_settings | 10 ++++++---- scripts/l4v.sh | 37 ++++++++++++++++++++++--------------- 2 files changed, 28 insertions(+), 19 deletions(-) diff --git a/res/isabelle_settings b/res/isabelle_settings index f15d2b2..0667999 100644 --- a/res/isabelle_settings +++ b/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 diff --git a/scripts/l4v.sh b/scripts/l4v.sh index 14564cd..a5e680d 100644 --- a/scripts/l4v.sh +++ b/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