Re: [isabelle] Plugin error with Isabelle-2016



On 29/07/16 13:49, Eugene W. Stark wrote:
> What I am easily and reliably able to reproduce is as follows:
> 
> % /opt/Isabelle2016/Isabelle2016 &
> (wait for Isabelle to start)
> % kill -KILL 29909   # or whatever the PID is of the Java process
> [1]  + Killed                        /opt/Isabelle2016/Isabelle2016
> % /opt/Isabelle2016/Isabelle2016&
> [1] 9015
> % 7:40:39 AM [main] [error] PluginJAR: Error while starting plugin isabelle.jedit.Plugin
> 7:40:39 AM [main] [error] PluginJAR: java.lang.NoClassDefFoundError: scala/Function0

Thanks. This is sufficient to reproduce the problem, which is actually
rather profane and without esoteric effects of JVM startup or warmup.

The problem is some invalid application state that remains after killing
the JVM. The next startup tries to connect to an already running
applications, but it does not work.

The situation can be improved by replacing Isabelle2016/Isabelle2016.run
with the included version. Note that the file needs to be executable.

This is only relevant to Linux: the Windows and Mac OS X applications
are different.


	Makarius

#!/usr/bin/env bash
#
# Author: Makarius
#
# Main Isabelle application script.

# dereference executable
if [ -L "$0" ]; then
  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi


# minimal Isabelle environment

ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"


# Java runtime options

ISABELLE_NAME="$(basename "$0" .run)"
if [ -z "$ISABELLE_PLATFORM64" ]; then
  declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options32"))
else
  declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options64"))
fi


# main

#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS

exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/jre/bin/java" \
  "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[ at ]}" \
  -classpath "$ISABELLE_HOME/lib/classes/Pure.jar:$ISABELLE_HOME/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar:$ISABELLE_HOME/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar:$ISABELLE_HOME/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar:$ISABELLE_HOME/contrib/jortho-1.0-2/jortho.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/akka-actor_2.11-2.3.10.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/config-1.2.1.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/jline-2.12.1.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-actors-2.11.0.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-actors-migration_2.11-1.1.0.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-compiler.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-continuations-library_2.11-1.0.2.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-continuations-plugin_2.11.7-1.0.2.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-library.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scalap-2.11.7.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-parser-combinators_2.11-1.0.4.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-reflect.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-swing_2.11-1.0.2.jar:$ISABELLE_HOME/contrib/scala-2.11.7/lib/scala-xml_2.11-1.0.4.jar:$ISABELLE_HOME/contrib/xz-java-1.2-1/lib/xz.jar:$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" \
  "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
  isabelle.Main "$@"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.