Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

reduce l4v/Isabelle image size #67

Merged
merged 2 commits into from
Feb 12, 2024
Merged

reduce l4v/Isabelle image size #67

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ee5881f
isabelle: remove obsolete settings
lsf37 Feb 12, 2024
ee33c88
l4v: reduce l4v image size
lsf37 Feb 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 7 additions & 23 deletions res/isabelle_settings
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,37 +8,21 @@
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
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"

37 changes: 22 additions & 15 deletions scripts/l4v.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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