Skip to content

Console Output

+ bin/isabelle getenv -a
ISABELLE_JDK_HOME=/media/data/jenkins/.isabelle/contrib/jdk-15.0.2+7/x86_64-linux
MIRABELLE_TIMEOUT=30
LD_LIBRARY_PATH=/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jni/x86_64-linux
RUN_DISPLAY_URL=https://ci.isabelle.systems/jenkins/job/isabelle-dump/49/display/redirect
ISABELLE_PLATFORM32=x86-linux
JENKINS_URL=https://ci.isabelle.systems/jenkins/
ISABELLE_JAVA_SYSTEM_OPTIONS=-server -Dfile.encoding=UTF-8 -Disabelle.threads=0
SMBC_HOME=/media/data/jenkins/.isabelle/contrib/smbc-0.4.1/x86_64-linux
EXECUTOR_NUMBER=0
SSH_CONNECTION=131.159.47.3 46818 192.168.1.163 22
ISABELLE_VERSION=5c4a09c4bc9c48f7fd7d6ff825ffa9e906b2a5d0
ISABELLE_SCALA_SCRIPT=/media/data/jenkins/workspace/isabelle-dump/bin/isabelle_scala_script
ISABELLE_JEDIT_OPTIONS=
ISABELLE_COMPONENTS_MISSING=
ISABELLE_TOOL=/media/data/jenkins/workspace/isabelle-dump/bin/isabelle
LANG=C.UTF-8
BUILD_ID=49
ISABELLE_DIRECTORIES=~:$ISABELLE_HOME_USER:~~
E_HOME=/media/data/jenkins/.isabelle/contrib/e-2.5-1/x86_64-linux
ISABELLE_ROOT=/media/data/jenkins/workspace/isabelle-dump
JEDIT_JAVA_SYSTEM_OPTIONS=-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle
ISABELLE_GNUPLOT=gnuplot
OLDPWD=/media/data/jenkins
RUN_CHANGES_DISPLAY_URL=https://ci.isabelle.systems/jenkins/job/isabelle-dump/49/display/redirect?page=changes
ISABELLE_HOME_USER=/media/data/jenkins/.isabelle
TPTP_HOME=/media/data/jenkins/workspace/isabelle-dump/src/HOL/TPTP
ISABELLE_LINE_EDITOR=rlwrap
ISABELLE_SCALAC_OPTIONS=-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -J-Xms512m -J-Xmx4g -J-Xss16m
ISABELLE_TOOL_JAVA_OPTIONS=-Xmx40g -Xss16m
Z3_INSTALLED=yes
JENKINS_NODE_COOKIE=2338ccf4-11b3-4de9-94bb-f24a0a3c4bb1
ISABELLE_DOCS_RELEASE_NOTES=~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY
ISABELLE_OCAMLFIND=/media/data/jenkins/workspace/isabelle-dump/lib/scripts/ocamlfind
ISABELLE_SITE_SETTINGS_PRESENT=true
KODKODI_JAVA_LIBRARY_PATH=/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jni/x86_64-linux
ISABELLE_OCAML_VERSION=ocaml-base-compiler.4.07.0
MIRABELLE_LOGIC=HOL
JAVA_HOME=/media/data/jenkins/.isabelle/contrib/jdk-15.0.2+7/x86_64-linux
ISABELLE_COMPONENT_REPOSITORY=https://isabelle.sketis.net/components
JOB_BASE_NAME=isabelle-dump
ISABELLE_CLASSPATH=/media/data/jenkins/workspace/isabelle-dump/lib/classes/Pure.jar:/media/data/jenkins/.isabelle/contrib/flatlaf-1.0/lib/flatlaf-1.0.jar:/media/data/jenkins/.isabelle/contrib/jfreechart-1.5.1/lib/iText-2.1.5.jar:/media/data/jenkins/.isabelle/contrib/jfreechart-1.5.1/lib/jfreechart-1.5.1.jar:/media/data/jenkins/.isabelle/contrib/jortho-1.0-2/jortho.jar:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/antlr-runtime-3.1.1.jar:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/kodkod-1.5.jar:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/kodkodi-1.5.6.jar:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/sat4j-2.3.jar:/media/data/jenkins/.isabelle/contrib/postgresql-42.2.18/postgresql-42.2.18.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/jline-3.19.0.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/jna-5.3.1.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scala-compiler.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scala-library.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scalap-2.13.5.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scala-parallel-collections_2.13-1.0.0.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scala-parser-combinators_2.13-1.1.2.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scala-reflect.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scala-swing_2.13-3.0.0.jar:/media/data/jenkins/.isabelle/contrib/scala-2.13.5/lib/scala-xml_2.13-1.3.0.jar:/media/data/jenkins/.isabelle/contrib/sqlite-jdbc-3.34.0/sqlite-jdbc-3.34.0.jar:/media/data/jenkins/.isabelle/contrib/ssh-java-20190323/lib/jsch-0.1.55.jar:/media/data/jenkins/.isabelle/contrib/ssh-java-20190323/lib/jzlib-1.1.3.jar:/media/data/jenkins/.isabelle/contrib/ssh-java-20190323/lib/jce.jar:/media/data/jenkins/.isabelle/contrib/xz-java-1.8/lib/xz.jar
WORKSPACE_TMP=/media/data/jenkins/workspace/isabelle-dump@tmp
BIB2XHTML_HOME=/media/data/jenkins/.isabelle/contrib/bib2xhtml-20190409
ISABELLE_ATP=/media/data/jenkins/workspace/isabelle-dump/src/HOL/Tools/ATP
ISABELLE_FONTS=/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSansMono.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSansMono-Bold.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSansMono-Oblique.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSansMono-BoldOblique.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSans.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSans-Bold.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSans-Oblique.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSans-BoldOblique.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSerif.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSerif-Bold.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSerif-Italic.ttf:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf-hinted/IsabelleDejaVuSerif-BoldItalic.ttf
POLYML_HOME=/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686
ML_SYSTEM=polyml-5.8.2
ISABELLE_STACK_RESOLVER=lts-16.31
PDF_VIEWER=xdg-open
KODKODI_JAR=/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar
JORTHO_DICTIONARIES=/media/data/jenkins/.isabelle/contrib/jortho-1.0-2/dictionaries/en.gz:/media/data/jenkins/.isabelle/contrib/jortho-1.0-2/dictionaries/en_US.gz:/media/data/jenkins/.isabelle/contrib/jortho-1.0-2/dictionaries/en_GB-ise.gz:/media/data/jenkins/.isabelle/contrib/jortho-1.0-2/dictionaries/en_GB-ize.gz:/media/data/jenkins/.isabelle/contrib/jortho-1.0-2/dictionaries/en_CA.gz
ISABELLE_PDFLATEX=lualatex --file-line-error
SCALA_HOME=/media/data/jenkins/.isabelle/contrib/scala-2.13.5
HUDSON_COOKIE=3e084bca-644f-48b5-bb6a-9aec7a43212c
XDG_SESSION_ID=1258
MIRABELLE_THEORY=Main
ISABELLE_BROWSER_INFO_SYSTEM=/media/data/jenkins/workspace/isabelle-dump/browser_info
ISABELLE_PLATFORM_FAMILY=linux
USER=jenkins
ISABELLE_BROWSER_INFO=/media/data/jenkins/.isabelle/browser_info
AFP_VERSION=28fe4ca859cdb506e2203e570460daa181b3958c
SPASS_VERSION=3.8ds
BUILD_NUMBER=49
JEDIT_HOME=/media/data/jenkins/workspace/isabelle-dump/src/Tools/jEdit
WORKSPACE=/media/data/jenkins/workspace/isabelle-dump
ISABELLE_OPEN=xdg-open
POLYML_EXE=/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/x86_64-linux/poly
PWD=/media/data/jenkins/workspace/isabelle-dump
HUDSON_URL=https://ci.isabelle.systems/jenkins/
ISABELLE_SCALA_SERVICES=isabelle.Tools:isabelle.Admin_Tools:isabelle.Scala_Functions:isabelle.Sessions$File_Format:isabelle.Bibtex$File_Format:isabelle.ML_Statistics$Handler:isabelle.Scala$Handler:isabelle.Print_Operation$Handler:isabelle.Simplifier_Trace$Handler:isabelle.Server_Commands:isabelle.spark.SPARK$Load_Command1:isabelle.spark.SPARK$Load_Command2:isabelle.nitpick.Kodkod$Handler:isabelle.nitpick.Scala_Functions:isabelle.FlatLightLaf:isabelle.FlatDarkLaf
HOME=/media/data/jenkins
ISABELLE_VERIT=/media/data/jenkins/.isabelle/contrib/verit-2020.10-rmx-1/x86_64-linux/veriT
MIRABELLE_HOME=/media/data/jenkins/workspace/isabelle-dump/src/HOL/Mirabelle
NODE_NAME=workerlrz6
Z3_VERSION=4.4.0pre
HUDSON_SERVER_COOKIE=89935be03e7b1021
SSH_CLIENT=131.159.47.3 46818 22
Z3_HOME=/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-3/x86_64-linux
JENKINS_HOME=/var/lib/jenkins
JOB_NAME=isabelle-dump
ISABELLE_DOCS_EXAMPLES=~~/src/HOL/Examples/Seq.thy:~~/src/HOL/Examples/Drinker.thy:~~/src/HOL/Examples/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML:$ML_SOURCES/ROOT.ML
RUN_TESTS_DISPLAY_URL=https://ci.isabelle.systems/jenkins/job/isabelle-dump/49/display/redirect?page=tests
BASH_ENV=/media/data/jenkins/workspace/isabelle-dump/lib/scripts/getfunctions
MUTABELLE_LOGIC=HOL
VAMPIRE_HOME=/media/data/jenkins/.isabelle/contrib/vampire-4.2.2/x86_64-linux
JORTHO_HOME=/media/data/jenkins/.isabelle/contrib/jortho-1.0-2
ML_PLATFORM=x86_64-linux
ISABELLE_SQLITE_HOME=/media/data/jenkins/.isabelle/contrib/sqlite-jdbc-3.34.0
JEDIT_OPTIONS=-reuseview -nobackground -nosplash -log=9
ISABELLE_GHC_VERSION=ghc-8.8.4
XZ_JAVA_HOME=/media/data/jenkins/.isabelle/contrib/xz-java-1.8
HUDSON_HOME=/var/lib/jenkins
JOB_DISPLAY_URL=https://ci.isabelle.systems/jenkins/job/isabelle-dump/display/redirect
JEDIT_SETTINGS=/media/data/jenkins/.isabelle/jedit
MUTABELLE_NUMBER_OF_MUTANTS=4
ML_HOME=/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/x86_64-linux
ISABELLE_LOGIC=HOL
VAMPIRE_EXTRA_OPTIONS=--mode casc
MUTABELLE_IMPORT_THEORY=Complex_Main
ISABELLE_COMPONENTS_BASE=/media/data/jenkins/.isabelle/contrib
RUN_ARTIFACTS_DISPLAY_URL=https://ci.isabelle.systems/jenkins/job/isabelle-dump/49/display/redirect?page=artifacts
ISABELLE_JENKINS_ROOT=https://ci.isabelle.systems/jenkins
ML_OPTIONS=--maxheap 40G
MAIL=/var/mail/jenkins
ZIPPERPOSITION_HOME=/media/data/jenkins/.isabelle/contrib/zipperposition-2.0-1/x86_64-linux
KODKODI_CLASSPATH=/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/antlr-runtime-3.1.1.jar:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/kodkod-1.5.jar:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/kodkodi-1.5.6.jar:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jar/sat4j-2.3.jar
ISABELLE_EXTERNAL_FILES=bmp:eps:gif:jpeg:jpg:pdf:png:xmp
CVC4_INSTALLED=yes
ISABELLE_GHC_STACK=true
KODKODI_VERSION=1.5.6
ISABELLE_GHC=/media/data/jenkins/workspace/isabelle-dump/lib/scripts/ghc
ISABELLE_NAME=Isabelle
ISABELLE_OPAM_ROOT=/media/data/jenkins/.opam
BUILD_URL=https://ci.isabelle.systems/jenkins/job/isabelle-dump/49/
SHELL=/bin/sh
STAGE_NAME=Install
ISABELLE_BIBTEX=bibtex
ISABELLE_STACK_ROOT=/media/data/jenkins/.stack
JOB_URL=https://ci.isabelle.systems/jenkins/job/isabelle-dump/
ISABELLE_HEAPS=/media/data/jenkins/.isabelle/heaps
NUNCHAKU_HOME=/media/data/jenkins/.isabelle/contrib/nunchaku-0.5/x86_64-linux
ISABELLE_FONTFORGE=fontforge
ISABELLE_STACK=/media/data/jenkins/.isabelle/contrib/stack-2.5.1/x86_64-linux/stack
BUILD_DISPLAY_NAME=#49
ISABELLE_APPLE_PLATFORM64=
ISABELLE_WINDOWS_PLATFORM64=
SMBC_VERSION=0.4.1
JEDIT_JAVA_OPTIONS=-Xms512m -Xmx4g -Xss16m
ISABELLE_PRINTENV=/usr/bin/printenv
CVC4_VERSION=1.8
ISABELLE_JAVA_PLATFORM=x86_64-linux
ISABELLE_COMPONENTS=/media/data/jenkins/workspace/isabelle-dump:/media/data/jenkins/workspace/isabelle-dump/src/Tools/jEdit:/media/data/jenkins/workspace/isabelle-dump/src/Tools/Graphview:/media/data/jenkins/workspace/isabelle-dump/src/Tools/VSCode:/media/data/jenkins/workspace/isabelle-dump/src/HOL/Mirabelle:/media/data/jenkins/workspace/isabelle-dump/src/HOL/Mutabelle:/media/data/jenkins/workspace/isabelle-dump/src/HOL/Library/Sum_of_Squares:/media/data/jenkins/workspace/isabelle-dump/src/HOL/SPARK:/media/data/jenkins/workspace/isabelle-dump/src/HOL/Tools:/media/data/jenkins/workspace/isabelle-dump/src/HOL/TPTP:/media/data/jenkins/workspace/isabelle-dump/Admin:/media/data/jenkins/.isabelle:/media/data/jenkins/.isabelle/contrib/gnu-utils-20210414:/media/data/jenkins/.isabelle/contrib/bash_process-1.2.3-1:/media/data/jenkins/.isabelle/contrib/bib2xhtml-20190409:/media/data/jenkins/.isabelle/contrib/csdp-6.1.1:/media/data/jenkins/.isabelle/contrib/cvc4-1.8:/media/data/jenkins/.isabelle/contrib/e-2.5-1:/media/data/jenkins/.isabelle/contrib/flatlaf-1.0:/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322:/media/data/jenkins/.isabelle/contrib/jdk-15.0.2+7:/media/data/jenkins/.isabelle/contrib/jedit_build-20210201:/media/data/jenkins/.isabelle/contrib/jfreechart-1.5.1:/media/data/jenkins/.isabelle/contrib/jortho-1.0-2:/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1:/media/data/jenkins/.isabelle/contrib/nunchaku-0.5:/media/data/jenkins/.isabelle/contrib/opam-2.0.7:/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686:/media/data/jenkins/.isabelle/contrib/postgresql-42.2.18:/media/data/jenkins/.isabelle/contrib/scala-2.13.5:/media/data/jenkins/.isabelle/contrib/smbc-0.4.1:/media/data/jenkins/.isabelle/contrib/spass-3.8ds-2:/media/data/jenkins/.isabelle/contrib/sqlite-jdbc-3.34.0:/media/data/jenkins/.isabelle/contrib/ssh-java-20190323:/media/data/jenkins/.isabelle/contrib/stack-2.5.1:/media/data/jenkins/.isabelle/contrib/vampire-4.2.2:/media/data/jenkins/.isabelle/contrib/verit-2020.10-rmx-1:/media/data/jenkins/.isabelle/contrib/xz-java-1.8:/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-3:/media/data/jenkins/.isabelle/contrib/zipperposition-2.0-1
MUTABELLE_NUMBER_OF_MUTATIONS=1
E_VERSION=2.5
SHLVL=1
SPASS_HOME=/media/data/jenkins/.isabelle/contrib/spass-3.8ds-2/x86_64-linux
ISABELLE_JEDIT_BUILD_VERSION=jedit-5.6.0-patched
ISABELLE_SYMBOLS=/media/data/jenkins/workspace/isabelle-dump/etc/symbols:/media/data/jenkins/.isabelle/etc/symbols
ISABELLE_CSDP=/media/data/jenkins/.isabelle/contrib/csdp-6.1.1/x86_64-linux/csdp
ISABELLE_BASH_PROCESS=/media/data/jenkins/.isabelle/contrib/bash_process-1.2.3-1/x86_64-linux/bash_process
ISABELLE_MAKEINDEX=makeindex
BUILD_TAG=jenkins-isabelle-dump-49
ISABELLE_SETTINGS_PRESENT=true
ISABELLE_BUILD_OPTIONS=
MUTABELLE_HOME=/media/data/jenkins/workspace/isabelle-dump/src/HOL/Mutabelle
ISABELLE_JEDIT_BUILD_HOME=/media/data/jenkins/.isabelle/contrib/jedit_build-20210201
KODKODI=/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1
ISABELLE_PLATFORM64=x86_64-linux
NODE_LABELS=lrz-large workerlrz6
LOGNAME=jenkins
ISABELLE_TOOLS=/media/data/jenkins/workspace/isabelle-dump/lib/Tools:/media/data/jenkins/workspace/isabelle-dump/src/Tools/jEdit/lib/Tools:/media/data/jenkins/workspace/isabelle-dump/src/HOL/Mirabelle/lib/Tools:/media/data/jenkins/workspace/isabelle-dump/src/HOL/Mutabelle/lib/Tools:/media/data/jenkins/workspace/isabelle-dump/src/HOL/TPTP/lib/Tools:/media/data/jenkins/workspace/isabelle-dump/Admin/lib/Tools
XDG_RUNTIME_DIR=/run/user/902
NUNCHAKU_VERSION=0.5
ISABELLE_DOCS=/media/data/jenkins/workspace/isabelle-dump/doc:/media/data/jenkins/workspace/isabelle-dump/src/Tools/jEdit/dist/doc
ISABELLE_TMP_PREFIX=/tmp/isabelle-jenkins
ML_IDENTIFIER=polyml-5.8.2_x86_64-linux
ISABELLE_TAR=/bin/tar
PATH=/media/data/jenkins/workspace/isabelle-dump/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin
ISABELLE_HEAPS_SYSTEM=/media/data/jenkins/workspace/isabelle-dump/heaps
USER_HOME=/media/data/jenkins
ISABELLE_WINDOWS_PLATFORM32=
CVC4_SOLVER=/media/data/jenkins/.isabelle/contrib/cvc4-1.8/x86_64-linux/cvc4
ML_SOURCES=/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/src
ISABELLE_EPSTOPDF=epstopdf
ISABELLE_OPAM=/media/data/jenkins/.isabelle/contrib/opam-2.0.7/x86_64-linux/opam
ISABELLE_FONTS_HIDDEN=/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322/ttf/Vacuous.ttf
ISABELLE_HOME=/media/data/jenkins/workspace/isabelle-dump
CVC4_HOME=/media/data/jenkins/.isabelle/contrib/cvc4-1.8/x86_64-linux
KODKODI_JNI=/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1/jni
VAMPIRE_VERSION=4.2.2pre
JENKINS_SERVER_COOKIE=durable-fa0e22c704037a59f60591045674f4a1
Z3_SOLVER=/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-3/x86_64-linux/z3
BASH_FUNC_tar%%=() {  if [ -f "$ISABELLE_TAR" ]; then
 "$ISABELLE_TAR" "$@";
 else
 "$(type -P tar)" "$@";
 fi
}
BASH_FUNC_isabelle_stack%%=() {  if [ -z "$ISABELLE_STACK" ]; then
 echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" 1>&2;
 return 127;
 else
 env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@";
 fi
}
BASH_FUNC_splitarray%%=() {  SPLITARRAY=();
 local IFS="$1";
 shift;
 local X="";
 for X in $*;
 do
 SPLITARRAY["${#SPLITARRAY[@]}"]="$X";
 done
}
BASH_FUNC_isabelle_opam%%=() {  if [ -z "$ISABELLE_OPAM" ]; then
 echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" 1>&2;
 return 127;
 else
 env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@";
 fi
}
BASH_FUNC_init_component%%=() {  local COMPONENT="$1";
 case "$COMPONENT" in 
 /*)

 ;;
 *)
 echo "Absolute component path required: \"$COMPONENT\"" 1>&2;
 exit 2
 ;;
 esac;
 if [ -d "$COMPONENT" ]; then
 if [ -z "$ISABELLE_COMPONENTS" ]; then
 ISABELLE_COMPONENTS="$COMPONENT";
 else
 ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT";
 fi;
 else
 echo "### Missing Isabelle component: \"$COMPONENT\"" 1>&2;
 if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
 ISABELLE_COMPONENTS_MISSING="$COMPONENT";
 else
 ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT";
 fi;
 fi;
 if [ -f "$COMPONENT/etc/settings" ]; then
 source "$COMPONENT/etc/settings";
 local RC="$?";
 if [ "$RC" -ne 0 ]; then
 echo "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" 1>&2;
 exit 2;
 fi;
 fi;
 if [ -f "$COMPONENT/etc/components" ]; then
 init_components "$COMPONENT" "$COMPONENT/etc/components";
 fi
}
BASH_FUNC_isabelle_jdk%%=() {  if [ -z "$ISABELLE_JDK_HOME" ]; then
 echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" 1>&2;
 return 127;
 else
 local PRG="$1";
 shift;
 "$ISABELLE_JDK_HOME/bin/$PRG" "$@";
 fi
}
BASH_FUNC_java_library%%=() {  local X="";
 for X in "$@";
 do
 case "$ISABELLE_PLATFORM_FAMILY" in 
 linux)
 if [ -z "$LD_LIBRARY_PATH" ]; then
 export LD_LIBRARY_PATH="$X";
 else
 export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$X";
 fi
 ;;
 macos)
 if [ -z "$JAVA_LIBRARY_PATH" ]; then
 export JAVA_LIBRARY_PATH="$X";
 else
 export JAVA_LIBRARY_PATH="$JAVA_LIBRARY_PATH:$X";
 fi
 ;;
 windows)
 if [ -z "$PATH" ]; then
 export PATH="$X";
 else
 export PATH="$PATH:$X";
 fi
 ;;
 esac;
 done;
 export ISABELLE_CLASSPATH
}
BASH_FUNC_isabelle_admin_build%%=() {  "$ISABELLE_HOME/Admin/build" "$@"
}
BASH_FUNC_isabelle_fonts%%=() {  local X="";
 for X in "$@";
 do
 if [ -z "$ISABELLE_FONTS" ]; then
 ISABELLE_FONTS="$X";
 else
 ISABELLE_FONTS="$ISABELLE_FONTS:$X";
 fi;
 done;
 export ISABELLE_FONTS
}
BASH_FUNC_isabelle_directory%%=() {  local X="";
 for X in "$@";
 do
 if [ -z "$ISABELLE_DIRECTORIES" ]; then
 ISABELLE_DIRECTORIES="$X";
 else
 ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X";
 fi;
 done;
 export ISABELLE_DIRECTORIES
}
BASH_FUNC_classpath%%=() {  local X="";
 for X in "$@";
 do
 if [ -z "$ISABELLE_CLASSPATH" ]; then
 ISABELLE_CLASSPATH="$X";
 else
 ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X";
 fi;
 done;
 export ISABELLE_CLASSPATH
}
BASH_FUNC_isabelle_scala%%=() {  if [ -z "$JAVA_HOME" ]; then
 echo "Unknown JAVA_HOME -- Java unavailable" 1>&2;
 return 127;
 else
 if [ -z "$SCALA_HOME" ]; then
 echo "Unknown SCALA_HOME -- Scala unavailable" 1>&2;
 return 127;
 else
 local PRG="$1";
 shift;
 "$SCALA_HOME/bin/$PRG" "$@";
 fi;
 fi
}
BASH_FUNC_init_components%%=() {  local REPLY="";
 local BASE="$1";
 local CATALOG="$2";
 local COMPONENT="";
 local -a COMPONENTS=();
 if [ ! -f "$CATALOG" ]; then
 echo "Bad component catalog file: \"$CATALOG\"" 1>&2;
 exit 2;
 fi;
 { 
 while { 
 unset REPLY;
 read -r;
 test "$?" = 0 -o -n "$REPLY"
 }; do
 case "$REPLY" in 
 \#* | "")

 ;;
 /*)
 COMPONENTS["${#COMPONENTS[@]}"]="$REPLY"
 ;;
 *)
 COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY"
 ;;
 esac;
 done
 } < "$CATALOG";
 for COMPONENT in "${COMPONENTS[@]}";
 do
 init_component "$COMPONENT";
 done
}
BASH_FUNC_isabelle_java%%=() {  if [ -z "$JAVA_HOME" ]; then
 echo "Unknown JAVA_HOME -- Java unavailable" 1>&2;
 return 127;
 else
 local PRG="$1";
 shift;
 "$JAVA_HOME/bin/$PRG" "$@";
 fi
}
BASH_FUNC_isabelle_scala_service%%=() {  local X="";
 for X in "$@";
 do
 if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
 ISABELLE_SCALA_SERVICES="$X";
 else
 ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X";
 fi;
 done;
 export ISABELLE_SCALA_SERVICES
}
BASH_FUNC_standard_path%%=() {  echo "$@"
}
BASH_FUNC_platform_path%%=() {  echo "$@"
}
BASH_FUNC_isabelle_fonts_hidden%%=() {  local X="";
 for X in "$@";
 do
 if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
 ISABELLE_FONTS_HIDDEN="$X";
 else
 ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X";
 fi;
 done;
 export ISABELLE_FONTS_HIDDEN
}
_=/usr/bin/env