Re: [isabelle] Isabelle2016-RC0 - does not exit on Linux



Hi,

I'm testing Isabelle2016-RC0_app.tar.gz on Ubuntu 14.04.3 LTS, Unity,
Linux 4.2.0-22-generic x86_64.

I started it in the shell with
  ./Isabelle2016-RC0/bin/isabelle jedit

After I exited jEdit (clicking the x in the window), the process was
not gone and it was still active in my shell. The prompt did not
return.

`ps aux` shows the following processes

diekmann  2412  0.0  0.0  18316  3572 pts/16   S+   18:05   0:00 bash
/home/diekmann/Downloads/Isabelle2016-RC0/lib/Tools/java
-Duser.language=en -Dawt.useSystemAAFontSettings=on
-Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true
-Dapple.awt.application.name=Isabelle -Xms512m -Xmx2560m -Xss8m
-XX:MetaspaceSize=256m isabelle.Main
diekmann  2442  4.0 21.0 6546964 1701868 pts/16 Sl+ 18:05   9:40
/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jdk/x86_64-linux/jre/bin/java
-server -XX:MinHeapFreeRatio=30 -XX:MaxHeapFreeRatio=60
-XX:+UseConcMarkSweepGC -XX:+CMSParallelRemarkEnabled
-Dfile.encoding=UTF-8 -Disabelle.threads=0 -classpath
/home/diekmann/Downloads/Isabelle2016-RC0/lib/classes/Pure.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jortho-1.0-2/jortho.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/akka-actor_2.11-2.3.10.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/config-1.2.1.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/jline-2.12.1.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-actors-2.11.0.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-actors-migration_2.11-1.1.0.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-compiler.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-continuations-library_2.11-1.0.2.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-continuations-plugin_2.11.7-1.0.2.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-library.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scalap-2.11.7.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-parser-combinators_2.11-1.0.4.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-reflect.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-swing_2.11-1.0.2.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-xml_2.11-1.0.4.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/xz-java-1.2-1/lib/xz.jar:/home/diekmann/Downloads/Isabelle2016-RC0/src/Tools/jEdit/dist/jedit.jar
-Duser.language=en -Dawt.useSystemAAFontSettings=on
-Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true
-Dapple.awt.application.name=Isabelle -Xms512m -Xmx2560m -Xss8m
-XX:MetaspaceSize=256m isabelle.Main

Checking with `-H`, it seems that 2412 has started 2442.

ctrl+c in the shell kills the isabelle processes.


Steps to reproduce:
1) Load a large theory with many dependencies, let jEdit open the
theories the theory depends on.
2) On my system, the theories had errors (not yet ported for 2016).
3) Change a file on disc, e.g., `mv Scratch.thy Scratch.thy2`
4) click away the "deleted on disc" info.
5) While Isabelle is still checking proofs (and finding more errors), close it.

Best Regards,
  Cornelius

2016-01-01 20:17 GMT+01:00 Makarius <makarius at sketis.net>:
> Dear Isabelle users,
>
> the coming Isabelle2016 release is scheduled for February 2016, after the
> next big Java 8 update by Oracle in January and some weeks before the
> deadline of ITP 2016.
>
> To get started with systematic testing there is now the relatively early
> http://isabelle.in.tum.de/website-Isabelle2016-RC0 (corresponding to
> Isabelle/e18444532fce and AFP/c62777f3e932).
>
> The website, NEWS, ANNOUNCE etc. are already mostly up-to-date.  Some
> documentation is still lagging behind, notably the Isabelle/jEdit manual.
> There are further fine points still to be sorted out.
>
>
> When discussing problems, observations, suggustions, etc. the mail subject
> line should be changed to something meaningful (but the release candidate
> number still given in the message body).
>
> As usual it is important to keep general laws of causality in mind: release
> candidates may still change, but the final release is final. Although this
> is tautological, in the past few releases we've often had complaints right
> after final lift-off, when it was too late.
>
> So the best time to start testing is now.
>
>
>         Makarius
>




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