On Fr, 2014-06-27 at 14:22 +0200, Makarius wrote: > On Fri, 27 Jun 2014, Peter Lammich wrote: > > >> If problems happen again with 4-8 GB JVM heap, you should describe what > >> really happens, with clear experimental setup. > > > > Giving a clear experimental setup is a real problem for errors that > > appear nondeterministically. > > The first thing is to describe the starting conditions: > > * Precise CPU model + memory size vendor_id : GenuineIntel cpu family : 6 model : 42 model name : Intel(R) Core(TM) i7-2720QM CPU @ 2.20GHz stepping : 7 microcode : 0x1a cpu MHz : 2194.940 cache size : 6144 KB physical id : 0 siblings : 8 core id : 0 cpu cores : 4 apicid : 0 initial apicid : 0 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx rdtscp lm constant_tsc arch_perfmon pebs bts rep_good nopl xtopology nonstop_tsc aperfmperf pni pclmulqdq dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm pcid sse4_1 sse4_2 x2apic popcnt tsc_deadline_timer aes xsave avx lahf_lm ida arat epb xsaveopt pln pts dtherm tpr_shadow vnmi flexpriority ept vpid bogomips : 4389.88 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management:
+++++++++ 8Gb of memory, 8Gb of swap space > > * Operating system Distributor ID: Ubuntu Description: Ubuntu 12.04.4 LTS Release: 12.04 Codename: precise > > * ML options (heap size, threads) > ML_IDENTIFIER=polyml-5.5.2_x86-linux POLYML_HOME=/home/lammich/.isabelle/contrib/polyml-5.5.2 ML_SYSTEM=polyml-5.5.2 ML_PLATFORM=x86-linux ML_OPTIONS=-H 500 ISABELLE_POLYML=true > * JVM options (heap size) JEDIT_JAVA_OPTIONS=-Xms2048m -Xmx4096m -Xss4m I also attached the output of "isabelle getenv -a" > > The second thing to point the the examples that were used, and give some > hints about the concrete situation. I will try to remember those if it occurs next. By the way, another Isabelle/jEdit user at our chair pointed out a workaround if things seem to be frozen: Just go the beginning of the current file and make a change there ... this usually wakes up the IDE again. -- Peter
LC_PAPER=de_DE.UTF-8 ISABELLE_TMP_PREFIX=/tmp/isabelle-lammich CVC3_REMOTE_SOLVER=cvc3 SSH_AGENT_PID=1991 LC_ADDRESS=de_DE.UTF-8 LC_MONETARY=de_DE.UTF-8 ISABELLE_ATP=/home/lammich/devel/Isabelle-devel/src/HOL/Tools/ATP ML_IDENTIFIER=polyml-5.5.2_x86-linux ISABELLE_FONTS=/home/lammich/devel/Isabelle-devel/lib/fonts/IsabelleText.ttf:/home/lammich/devel/Isabelle-devel/lib/fonts/IsabelleTextBold.ttf JEDIT_HOME=/home/lammich/devel/Isabelle-devel/src/Tools/jEdit Z3_NEW_SOLVER=/home/lammich/.isabelle/contrib/z3-4.3.2pre-1/x86_64-linux/z3 GPG_AGENT_INFO=/tmp/keyring-my6CuJ/gpg:0:1 JEDIT_SYSTEM_OPTIONS=-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle MIRABELLE_THEORY=Main EXEC_PROCESS=/home/lammich/.isabelle/contrib/exec_process-1.0.3/x86_64-linux/exec_process KODKODI_PLATFORM=x86-linux SHELL=/bin/bash TERM=xterm ISABELLE_BUILD_JAVA_OPTIONS=-Xmx1024m -Xss1m XDG_SESSION_COOKIE=e98a42690e78d743ed79353600000007-1403084616.517570-346887857 ISABELLE_IDENTIFIER= ISABELLE_COMPONENTS_MISSING= ISABELLE_JDK_HOME=/home/lammich/.isabelle/contrib/jdk-8u5/x86_64-linux ISABELLE_MAKEINDEX=makeindex Z3_NEW_HOME=/home/lammich/.isabelle/contrib/z3-4.3.2pre-1/x86_64-linux ISABELLE_PROCESS=/home/lammich/devel/Isabelle-devel/bin/isabelle_process Z3_NEW_INSTALLED=yes ISABELLE_JAVA_EXT=/home/lammich/.isabelle/contrib/jdk-8u5/x86_64-linux/jre/lib/ext LC_NUMERIC=de_DE.UTF-8 WINDOWID=67827196 ISABELLE_DOCS_RELEASE_NOTES=ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:README_REPOSITORY MIRABELLE_TIMEOUT=30 GNOME_KEYRING_CONTROL=/tmp/keyring-my6CuJ ISABELLE_BIBTEX=bibtex DVI_VIEWER=xdg-open Z3_REMOTE_SOLVER=z3 REPLY= ISABELLE_SETTINGS_PRESENT=true ISABELLE_BUILD_OPTIONS= MUTABELLE_IMPORT_THEORY=Complex_Main POLYML_HOME=/home/lammich/.isabelle/contrib/polyml-5.5.2 Z3_COMPONENT=/home/lammich/.isabelle/contrib/z3-3.2-1 GTK_MODULES=canberra-gtk-module:canberra-gtk-module ISABELLE_PLATFORM_FAMILY=linux ISABELLE_SLEDGEHAMMER_MASH=/home/lammich/devel/Isabelle-devel/src/HOL/Tools/Sledgehammer/MaSh ISABELLE_PATH=/home/lammich/.isabelle/heaps:/home/lammich/devel/Isabelle-devel/heaps USER=lammich ML_SYSTEM=polyml-5.5.2 LC_TELEPHONE=de_DE.UTF-8 LS_COLORS=rs=0:di=01;34:ln=01;36:mh=00:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:su=37;41:sg=30;43:ca=30;41:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.lzma=01;31:*.tlz=01;31:*.txz=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.dz=01;31:*.gz=01;31:*.lz=01;31:*.xz=01;31:*.bz2=01;31:*.bz=01;31:*.tbz=01;31:*.tbz2=01;31:*.tz=01;31:*.deb=01;31:*.rpm=01;31:*.jar=01;31:*.war=01;31:*.ear=01;31:*.sar=01;31:*.rar=01;31:*.ace=01;31:*.zoo=01;31:*.cpio=01;31:*.7z=01;31:*.rz=01;31:*.jpg=01;35:*.jpeg=01;35:*.gif=01;35:*.bmp=01;35:*.pbm=01;35:*.pgm=01;35:*.ppm=01;35:*.tga=01;35:*.xbm=01;35:*.xpm=01;35:*.tif=01;35:*.tiff=01;35:*.png=01;35:*.svg=01;35:*.svgz=01;35:*.mng=01;35:*.pcx=01;35:*.mov=01;35:*.mpg=01;35:*.mpeg=01;35:*.m2v=01;35:*.mkv=01;35:*.webm=01;35:*.ogm=01;35:*.mp4=01;35:*.m4v=01;35:*.mp4v=01;35:*.vob=01;35:*.qt=01;35:*.nuv=01;35:*.wmv=01;35:*.asf=01;35:*.rm=01;35:*.rmvb=01;35:*.flc=01;35:*.avi=01;35:*.fli=01;35:*.flv=01;35:*.gl=01;35:*.dl=01;35:*.xcf=01;35:*.xwd=01;35:*.yuv=01;35:*.cgm=01;35:*.emf=01;35:*.axv=01;35:*.anx=01;35:*.ogv=01;35:*.ogx=01;35:*.aac=00;36:*.au=00;36:*.flac=00;36:*.mid=00;36:*.midi=00;36:*.mka=00;36:*.mp3=00;36:*.mpc=00;36:*.ogg=00;36:*.ra=00;36:*.wav=00;36:*.axa=00;36:*.oga=00;36:*.spx=00;36:*.xspf=00;36: ISABELLE_OPEN=xdg-open Z3_NEW_COMPONENT=/home/lammich/.isabelle/contrib/z3-4.3.2pre-1 ISABELLE_EPSTOPDF=epstopdf XDG_SESSION_PATH=/org/freedesktop/DisplayManager/Session0 HASKABELLE_HOME_USER=/home/lammich/.isabelle/Haskabelle-2013 XDG_SEAT_PATH=/org/freedesktop/DisplayManager/Seat0 ISABELLE_SITE_SETTINGS_PRESENT=true Z3_HOME=/home/lammich/.isabelle/contrib/z3-3.2-1/x86-linux SSH_AUTH_SOCK=/tmp/keyring-my6CuJ/ssh ISABELLE_COMPONENTS=/home/lammich/devel/Isabelle-devel:/home/lammich/devel/Isabelle-devel/src/Tools/Code:/home/lammich/devel/Isabelle-devel/src/Tools/jEdit:/home/lammich/devel/Isabelle-devel/src/Tools/Graphview:/home/lammich/devel/Isabelle-devel/src/HOL/Mirabelle:/home/lammich/devel/Isabelle-devel/src/HOL/Mutabelle:/home/lammich/devel/Isabelle-devel/src/HOL/Library/Sum_of_Squares:/home/lammich/devel/Isabelle-devel/src/HOL/Tools:/home/lammich/devel/Isabelle-devel/src/HOL/Tools/ATP:/home/lammich/devel/Isabelle-devel/src/HOL/Tools/Sledgehammer/MaSh:/home/lammich/devel/Isabelle-devel/src/HOL/TPTP:/home/lammich/devel/Isabelle-devel/Admin:/home/lammich/.isabelle:/home/lammich/.isabelle/contrib/cvc3-2.4.1:/home/lammich/.isabelle/contrib/e-1.8:/home/lammich/.isabelle/contrib/exec_process-1.0.3:/home/lammich/.isabelle/contrib/Haskabelle-2013:/home/lammich/.isabelle/contrib/jdk-8u5:/home/lammich/.isabelle/contrib/jedit_build-20140511:/home/lammich/.isabelle/contrib/jfreechart-1.0.14-1:/home/lammich/.isabelle/contrib/jortho-1.0-2:/home/lammich/.isabelle/contrib/kodkodi-1.5.2:/home/lammich/.isabelle/contrib/polyml-5.5.2:/home/lammich/.isabelle/contrib/scala-2.11.1:/home/lammich/.isabelle/contrib/spass-3.8ds:/home/lammich/.isabelle/contrib/z3-3.2-1:/home/lammich/.isabelle/contrib/z3-4.3.2pre-1:/home/lammich/.isabelle/contrib/xz-java-1.2-1:/home/lammich/.isabelle/contrib/ProofGeneral-4.2-1:/home/lammich/.isabelle/contrib/hol-light-bundle-0.5-126:/home/lammich/.isabelle/contrib/ProofGeneral-4.1:/home/lammich/devel/isabelle/afp-devel JFREECHART_HOME=/home/lammich/.isabelle/contrib/jfreechart-1.0.14-1 KODKODI_JAVA_LIBRARY_PATH=/home/lammich/.isabelle/contrib/kodkodi-1.5.2/jni/x86-linux ISABELLE_HOME_USER=/home/lammich/.isabelle Z3_NEW_VERSION=4.3.2pre-1 HOL_LIGHT_BUNDLE_COMPONENT=/home/lammich/.isabelle/contrib/hol-light-bundle-0.5-126 DEFAULTS_PATH=/usr/share/gconf/ubuntu.default.path SESSION_MANAGER=local/lapbroy33:@/tmp/.ICE-unix/1945,unix/lapbroy33:/tmp/.ICE-unix/1945 X=/home/lammich/devel/isabelle/afp-devel/tools MUTABELLE_NUMBER_OF_MUTANTS=4 MUTABELLE_NUMBER_OF_MUTATIONS=1 ISABELLE_BROWSER_INFO=/home/lammich/.isabelle/browser_info JORTHO_HOME=/home/lammich/.isabelle/contrib/jortho-1.0-2 XDG_CONFIG_DIRS=/etc/xdg/xdg-ubuntu:/etc/xdg ML_PLATFORM=x86-linux MIRABELLE_LOGIC=HOL ML_OPTIONS=-H 500 DESKTOP_SESSION=ubuntu PATH=/usr/local/heroku/bin:/home/lammich/bin:/home/lammich/opt/bin:/home/lammich/bin:/usr/lib/lightdm/lightdm:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/home/lammich/.rvm/bin:/home/lammich/.rvm/bin AFP=/home/lammich/devel/isabelle/afp-devel/thys LC_IDENTIFICATION=de_DE.UTF-8 ISABELLE_TOOL=/home/lammich/devel/Isabelle-devel/bin/isabelle ISABELLE_PLATFORM32=x86-linux ISABELLE_SUM_OF_SQUARES=/home/lammich/devel/Isabelle-devel/src/HOL/Library/Sum_of_Squares PWD=/home/lammich USER_HOME=/home/lammich JEDIT_OPTIONS=-reuseview -noserver -nobackground -log=9 KODKODI_CLASSPATH=/home/lammich/.isabelle/contrib/kodkodi-1.5.2/jar/antlr-runtime-3.1.1.jar:/home/lammich/.isabelle/contrib/kodkodi-1.5.2/jar/kodkod-1.5.jar:/home/lammich/.isabelle/contrib/kodkodi-1.5.2/jar/kodkodi-1.5.2.jar:/home/lammich/.isabelle/contrib/kodkodi-1.5.2/jar/sat4j-2.3.jar TPTP_HOME=/home/lammich/devel/Isabelle-devel/src/HOL/TPTP CVC3_INSTALLED=yes JAVA_HOME=/home/lammich/.isabelle/contrib/jdk-8u5/x86_64-linux ISABELLE_HOME=/home/lammich/devel/Isabelle-devel ISABELLE_POLYML=true LANG=en_US.UTF-8 GNOME_KEYRING_PID=1934 ISABELLE_LINE_EDITOR=/usr/bin/rlwrap E_VERSION=1.8 MANDATORY_PATH=/usr/share/gconf/ubuntu.mandatory.path ISABELLE_OUTPUT=/home/lammich/.isabelle/heaps/polyml-5.5.2_x86-linux MUTABELLE_HOME=/home/lammich/devel/Isabelle-devel/src/HOL/Mutabelle CVC3_SOLVER=/home/lammich/.isabelle/contrib/cvc3-2.4.1/x86_64-linux/cvc3 LC_MEASUREMENT=de_DE.UTF-8 COMPIZ_CONFIG_PROFILE=ubuntu UBUNTU_MENUPROXY=libappmenu.so ISABELLE_DOCS_EXAMPLES=src/HOL/ex/Seq.thy:src/HOL/ex/ML.thy:src/HOL/Unix/Unix.thy:src/HOL/Isar_Examples/Drinker.thy:src/Tools/SML/Examples.thy MASH_PORT=9255 ML_HOME=/home/lammich/.isabelle/contrib/polyml-5.5.2/x86-linux ISABELLE_ID= ISABELLE_JAVA_SYSTEM_OPTIONS=-Dfile.encoding=UTF-8 -server CVC3_HOME=/home/lammich/.isabelle/contrib/cvc3-2.4.1/x86_64-linux ISABELLE_JEDIT_BUILD_HOME=/home/lammich/.isabelle/contrib/jedit_build-20140511 KODKODI=/home/lammich/.isabelle/contrib/kodkodi-1.5.2 GDMSESSION=ubuntu ISABELLE_COMPONENT_REPOSITORY=http://isabelle.in.tum.de/components KODKODI_JAVA_OPT=-Dkodkod.minisat=_32 -Dkodkod.cryptominisat=_32 -Dkodkod.lingeling=_32 PDF_VIEWER=xdg-open KODKODI_JAR=/home/lammich/.isabelle/contrib/kodkodi-1.5.2/jar ISABELLE_LOGIC=HOL HOME=/home/lammich SHLVL=2 ISABELLE_PLATFORM64=x86_64-linux E_HOME=/home/lammich/.isabelle/contrib/e-1.8/x86_64-linux KODKODI_JNI=/home/lammich/.isabelle/contrib/kodkodi-1.5.2/jni AFP_BUILD_OPTIONS=-v -o browser_info -o "document=pdf" -o "document_variants=document:outline=/proof,/ML" LANGUAGE=en HASKABELLE_HOME=/home/lammich/.isabelle/contrib/Haskabelle-2013 SPASS_HOME=/home/lammich/.isabelle/contrib/spass-3.8ds/x86_64-linux ISABELLE_CLASSPATH=/home/lammich/devel/Isabelle-devel/lib/classes/Pure.jar:/home/lammich/.isabelle/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar:/home/lammich/.isabelle/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar:/home/lammich/.isabelle/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar:/home/lammich/.isabelle/contrib/jortho-1.0-2/jortho.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/akka-actor_2.11-2.3.3.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/config-1.2.1.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/jline-2.11.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-actors-2.11.0.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-actors-migration_2.11-1.1.0.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-compiler.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-continuations-library_2.11-1.0.2.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-continuations-plugin_2.11.1-1.0.2.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-library.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-parser-combinators_2.11-1.0.1.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-reflect.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-swing_2.11-1.0.1.jar:/home/lammich/.isabelle/contrib/scala-2.11.1/lib/scala-xml_2.11-1.0.2.jar:/home/lammich/.isabelle/contrib/xz-java-1.2-1/lib/xz.jar HOL_LIGHT_BUNDLE=/home/lammich/.isabelle/contrib/hol-light-bundle-0.5-126/proofs GNOME_DESKTOP_SESSION_ID=this-is-deprecated CVC3_VERSION=2.4.1 ISABELLE_JEDIT_BUILD_VERSION=jedit-5.1.0-patched KODKODI_VERSION=1.5.2 SPASS_VERSION=3.8ds XZ_JAVA_HOME=/home/lammich/.isabelle/contrib/xz-java-1.2-1 ISABELLE_LATEX=latex JEDIT_JAVA_OPTIONS=-Xms2048m -Xmx4096m -Xss4m LOGNAME=lammich ISABELLE_TOOLS=/home/lammich/devel/Isabelle-devel/lib/Tools:/home/lammich/devel/Isabelle-devel/src/Tools/Code/lib/Tools:/home/lammich/devel/Isabelle-devel/src/Tools/jEdit/lib/Tools:/home/lammich/devel/Isabelle-devel/src/HOL/Mirabelle/lib/Tools:/home/lammich/devel/Isabelle-devel/src/HOL/Mutabelle/lib/Tools:/home/lammich/devel/Isabelle-devel/src/HOL/TPTP/lib/Tools:/home/lammich/devel/Isabelle-devel/Admin/lib/Tools:/home/lammich/.isabelle/contrib/Haskabelle-2013/lib/Tools:/home/lammich/devel/isabelle/afp-devel/tools MIRABELLE_HOME=/home/lammich/devel/Isabelle-devel/src/HOL/Mirabelle JFREECHART_JAR_NAMES=iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar JORTHO_DICTIONARIES=/home/lammich/.isabelle/contrib/jortho-1.0-2/dictionaries/en.gz:/home/lammich/.isabelle/contrib/jortho-1.0-2/dictionaries/en_US.gz:/home/lammich/.isabelle/contrib/jortho-1.0-2/dictionaries/en_GB-ise.gz:/home/lammich/.isabelle/contrib/jortho-1.0-2/dictionaries/en_GB-ize.gz:/home/lammich/.isabelle/contrib/jortho-1.0-2/dictionaries/en_CA.gz ML_SOURCES=/home/lammich/.isabelle/contrib/polyml-5.5.2/src DBUS_SESSION_BUS_ADDRESS=unix:abstract=/tmp/dbus-Sb8q94GqsB,guid=305479556cf016a0fbf7acda00000019 XDG_DATA_DIRS=/usr/share/ubuntu:/usr/share/gnome:/usr/local/share/:/usr/share/ PROOFGENERAL_OPTIONS= LESSOPEN=| /usr/bin/lesspipe %s ISABELLE_PLATFORM=x86-linux ISABELLE_PDFLATEX=pdflatex SCALA_HOME=/home/lammich/.isabelle/contrib/scala-2.11.1 PROOFGENERAL_HOME=/home/lammich/.isabelle/contrib/ProofGeneral-4.1 CVC3_COMPONENT=/home/lammich/.isabelle/contrib/cvc3-2.4.1 Z3_SOLVER=/home/lammich/.isabelle/contrib/z3-3.2-1/x86-linux/z3 AFP_BASE=/home/lammich/devel/isabelle/afp-devel DISPLAY=:0.0 MUTABELLE_LOGIC=HOL ISABELLE_DOCS=/home/lammich/devel/Isabelle-devel/doc:/home/lammich/devel/Isabelle-devel/src/Tools/jEdit/dist/doc:/home/lammich/.isabelle/contrib/Haskabelle-2013/doc XDG_CURRENT_DESKTOP=Unity LC_TIME=de_DE.UTF-8 LESSCLOSE=/usr/bin/lesspipe %s %s ISABELLE_SYMBOLS=/home/lammich/devel/Isabelle-devel/etc/symbols:/home/lammich/.isabelle/etc/symbols ISABELLE_SCALA_SCRIPT=/home/lammich/devel/Isabelle-devel/bin/isabelle_scala_script ISABELLE_SCALA_BUILD_OPTIONS=-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130 JEDIT_SETTINGS=/home/lammich/.isabelle/jedit Z3_INSTALLED=yes LC_NAME=de_DE.UTF-8 XAUTHORITY=/home/lammich/.Xauthority COLORTERM=gnome-terminal ISABELLE_JEDIT_OPTIONS=-m brackets ISABELLE_NEOS_SERVER=http://neos-server.org:3332 librarypath=() { for X in "$@"; do case "$ISABELLE_PLATFORM" in *-darwin) if [ -z "$DYLD_LIBRARY_PATH" ]; then DYLD_LIBRARY_PATH="$X"; else DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"; fi; export DYLD_LIBRARY_PATH ;; *) if [ -z "$LD_LIBRARY_PATH" ]; then LD_LIBRARY_PATH="$X"; else LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"; fi; export LD_LIBRARY_PATH ;; esac; done } splitarray=() { SPLITARRAY=(); local IFS="$1"; shift; for X in $*; do SPLITARRAY["${#SPLITARRAY[@]}"]="$X"; done } classpath=() { for X in "$@"; do if [ -z "$ISABELLE_CLASSPATH" ]; then ISABELLE_CLASSPATH="$X"; else ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"; fi; done; export ISABELLE_CLASSPATH } jvmpath=() { echo "$@" } isabelle_scala_script=() { "$ISABELLE_SCALA_SCRIPT" "$@" } isabelle_admin_build=() { "$ISABELLE_HOME/Admin/build" "$@" } isabelle_process=() { "$ISABELLE_PROCESS" "$@" } init_components=() { local BASE="$1"; local CATALOG="$2"; 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 \#* | "") ;; /*) init_component "$REPLY" ;; *) init_component "$BASE/$REPLY" ;; esac; done } < "$CATALOG" } 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 } isabelle_scala=() { if [ -z "$ISABELLE_JDK_HOME" ]; then echo "Unknown ISABELLE_JDK_HOME -- Java tools 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 } isabelle_jdk=() { if [ -z "$ISABELLE_JDK_HOME" ]; then echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" 1>&2; return 127; else local PRG="$1"; shift; "$ISABELLE_JDK_HOME/bin/$PRG" "$@"; fi } isabelle=() { "$ISABELLE_TOOL" "$@" } _=/usr/bin/env
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev