[isabelle-dev] Remaining uses of Proof General?
Peter Lammich
lammich at in.tum.de
Fri Jun 27 14:37:33 CEST 2014
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
-------------- next part --------------
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
More information about the isabelle-dev
mailing list