Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Manuel Eberl 
The following seems to be the most reliable way to trigger the problem:

while true
isabelle build -b -c Pure
end

I did that and about 6% of builds with Scala 2.12.3 failed with
something like the attached log. I then tried the same thing with Scala
2.12.2 (double-checked "isabelle scala -version" to be sure) and the
same thing happened. I got 9 failures in 152 iterations; however, I
never got a JVM segfault with either Scala version; only these "silent
failures". That was on my Ryzen 1800X.

I then did the exact same thing on my laptop (with Scala 2.12.3 though)
and haven't gotten a single failure in over 100 iterations. So maybe
this is the Ryzen bug after all?

Lars, maybe you can run the same test on your machine and see what
happens there.

Manuel


On 19/08/17 21:29, Makarius wrote:
> On 19/08/17 21:27, Makarius wrote:
>> I propose to try the previous Scala release locally, e.g. as follows in
>> $ISABELLE_HOME_USER/etc/settings:
>>
>>   init_component "$HOME/.isabelle/contrib/scala-2.12.2"
> 
> Do not forget "isabelle jedit -b -f" after flipping Scala versions (that
> is not required for changes of the Java version).
> 
> 
>   Makarius
> 
Cleaning Pure ...
Building Pure ...
Pure FAILED
(see also /home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/Pure)
val warning_message: string -> unit
val writeln_message: string -> unit
  end
structure Debugger: DEBUGGER
val it = (): unit
signature NAMED_THEOREMS =
  sig
val add: string -> attribute
val add_thm: string -> thm -> Context.generic -> Context.generic
val check: Proof.context -> string * Position.T -> string
val clear: string -> Context.generic -> Context.generic
val declare: binding -> string -> local_theory -> string * local_theory
val del: string -> attribute
val del_thm: string -> thm -> Context.generic -> Context.generic
val get: Proof.context -> string -> thm list
val member: Proof.context -> string -> thm -> bool
  end
structure Named_Theorems: NAMED_THEOREMS
val it = (): unit
signature JEDIT = sig val check_action: string * Position.T -> string end
structure JEdit: JEDIT
val it = (): unit
Loading theory "Pure"
### theory "Pure"
### 0.436s elapsed time, 0.436s cpu time, 0.016s GC time
Loading theory "ML_Bootstrap"
structure Output_Primitives: OUTPUT_PRIMITIVES
structure Thread_Data: THREAD_DATA
val ML_system_pp = fn: (int -> 'a -> 'b -> PolyML.pretty) -> unit
val it = (): unit
val it = (): unit
structure PolyML:
  sig
structure IntInf:
  sig val gcd: int * int -> int val lcm: int * int -> int end
  end
val it = (): unit
val it = (): unit
### theory "ML_Bootstrap"
### 0.006s elapsed time, 0.006s cpu time, 0.000s GC time
Unfinished session(s): Pure
0:00:32 elapsed time, 0:00:10 cpu time, factor 0.31
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Makarius 
On 19/08/17 21:27, Makarius wrote:
> I propose to try the previous Scala release locally, e.g. as follows in
> $ISABELLE_HOME_USER/etc/settings:
> 
>   init_component "$HOME/.isabelle/contrib/scala-2.12.2"

Do not forget "isabelle jedit -b -f" after flipping Scala versions (that
is not required for changes of the Java version).


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Makarius 
On 19/08/17 21:14, Manuel Eberl wrote:
> 
> As for Scala, could a problem in the Scala compiler really lead to the
> JVM segfaulting? I would have thought if the JVM segfaults, that's a bug
> in the JVM. (unless it's a hardware-related issue, of course)
> 
> So, all in all, my money would be on the JVM.

The JVM is indeed the weakest link in the chain, but I've seen
situations in the past where the Scala compiler has triggered a JVM
problem by producing certain byte code: the problem disappeared again
after another update of Scala.

I propose to try the previous Scala release locally, e.g. as follows in
$ISABELLE_HOME_USER/etc/settings:

  init_component "$HOME/.isabelle/contrib/scala-2.12.2"

If that crashes again, we can be quite sure that it is jdk-8u144.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Manuel Eberl 
The Ryzen thing was also on my mind, but I have not experienced any of
those instability issues. From what I read, they are extremely rare
under normal use and the error occured a few seconds after initiating
isabelle build.

Besides, I know that Lars does not have a Ryzen CPU, and it would be a
very strange coincidence that he ran into a different issue that also
leads to a JVM crash.

As for Scala, could a problem in the Scala compiler really lead to the
JVM segfaulting? I would have thought if the JVM segfaults, that's a bug
in the JVM. (unless it's a hardware-related issue, of course)

So, all in all, my money would be on the JVM.

Manuel


On 19/08/17 21:04, Makarius wrote:
> On 19/08/17 20:31, Manuel Eberl wrote:
>>> If you still have that, can you send it to me?
>>
>> Sure.
>>
>>> Since the JVM crash happened during scalac compilation, I recommend to
>>> enforce a fresh build, e.g. like this:
> 
> The log says "java_command: isabelle.Isabelle_Tool build -b
> HOL-Analysis" so this was really the "isabelle build", after scalac
> compilation was finished.
> 
> Reading the tea leaves further, I see the following potential reasons of
> the crash:
> 
>   * jdk-8u144 (see Isabelle/98afae4308f5)
> 
>   * scala-2.12.3 (see Isabelle/96ad7d5ff613)
> 
>   * hardware: AMD Ryzen 7 1800X Eight-Core Processor
> 
> I've seen occasional press articles discussing problems of AMD Ryzen,
> e.g.
> https://www.phoronix.com/scan.php?page=news_item&px=Ryzen-Compiler-Issues
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Makarius 
On 19/08/17 17:19, Lars Hupel wrote:
>> on 158c513a39f5, I just had a JVM crash during "isabelle build" when it
>> was building Isabelle/Scala. (Log attached).
> 
> I had a similar problem today. Unfortunately I didn't save the logfile.

Can you say anything about the system? Hardware, OS etc.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Makarius 
On 19/08/17 20:31, Manuel Eberl wrote:
>> If you still have that, can you send it to me?
> 
> Sure.
> 
>> Since the JVM crash happened during scalac compilation, I recommend to
>> enforce a fresh build, e.g. like this:

The log says "java_command: isabelle.Isabelle_Tool build -b
HOL-Analysis" so this was really the "isabelle build", after scalac
compilation was finished.

Reading the tea leaves further, I see the following potential reasons of
the crash:

  * jdk-8u144 (see Isabelle/98afae4308f5)

  * scala-2.12.3 (see Isabelle/96ad7d5ff613)

  * hardware: AMD Ryzen 7 1800X Eight-Core Processor

I've seen occasional press articles discussing problems of AMD Ryzen,
e.g.
https://www.phoronix.com/scan.php?page=news_item&px=Ryzen-Compiler-Issues


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Manuel Eberl 
> If you still have that, can you send it to me?

Sure.

> Since the JVM crash happened during scalac compilation, I recommend to
> enforce a fresh build, e.g. like this:

That seems to have worked. The only output I got was this:

### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...


Manuel
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x7f25a57c5b6c, pid=13339, tid=0x7f256066c700
#
# JRE version: Java(TM) SE Runtime Environment (8.0_144-b01) (build 1.8.0_144-b01)
# Java VM: Java HotSpot(TM) 64-Bit Server VM (25.144-b01 mixed mode linux-amd64 compressed oops)
# Problematic frame:
# J 2075 C2 scala.util.parsing.combinator.Parsers$Parser$$Lambda$107.apply(Ljava/lang/Object;)Ljava/lang/Object; (16 bytes) @ 0x7f25a57c5b6c [0x7f25a57c5b00+0x6c]
#
# Core dump written. Default location: /home/manuel/hg/afp-devel/core or core.13339
#
# If you would like to submit a bug report, please visit:
#   http://bugreport.java.com/bugreport/crash.jsp
#

---  T H R E A D  ---

Current thread (0x7f25b5e99800):  JavaThread "pool-1-thread-5" daemon [_thread_in_Java, id=13390, stack(0x7f256026c000,0x7f256066d000)]

siginfo: si_signo: 11 (SIGSEGV), si_code: 1 (SEGV_MAPERR), si_addr: 0xf21517da

Registers:
RAX=0x0007c0061210, RBX=0x7f25622e2870, RCX=0xe404fdd3, RDX=0x0007947664a0
RSP=0x7f256066a898, RBP=0xe4000482, RSI=0xf21517ca, RDI=0xf28ece10
R8 =0x0007c01b3230, R9 =0xf1dfb1a3, R10=0xf21517ca, R11=0x0007c01b3230
R12=0x, R13=0x00072027ee98, R14=0xf803c74e, R15=0x7f25b5e99800
RIP=0x7f25a57c5b6c, EFLAGS=0x00010202, CSGSFS=0x002b0033, ERR=0x0004
  TRAPNO=0x000e

Top of Stack: (sp=0x7f256066a898)
0x7f256066a898:   7f25a573cae8 f2152037
0x7f256066a8a8:   7f25a573cae8 e4000482
0x7f256066a8b8:   e4000482 0007f21517d3
0x7f256066a8c8:   000790a8eb00 000794766dd8
0x7f256066a8d8:   7f25a5af59b8 e4000482
0x7f256066a8e8:   7f25a573cae8 000794766e78
0x7f256066a8f8:   000794766e78 e4000482
0x7f256066a908:   7f25a57bd270 0007f2151765
0x7f256066a918:   7f25a5af5b0c 0007c01b1650
0x7f256066a928:   7f25a5b01884 e4000482
0x7f256066a938:   7f25a573cae8 e40de09c
0x7f256066a948:   7f25a573cae8 e4000482
0x7f256066a958:   7f25a57bd270 e40de09c
0x7f256066a968:   7f25a57bd270 000794765550
0x7f256066a978:   7f25a5af5b0c e40d8883
0x7f256066a988:   7f25a57bd270 e40de0a2
0x7f256066a998:   7f25a573cae8 f21519e3
0x7f256066a9a8:   7f25a573cae8 e40de0a2
0x7f256066a9b8:   7f25a57bd270 f21519e3
0x7f256066a9c8:   7f25a5af59b8 f21519e6e40db48e
0x7f256066a9d8:   0007947664a0 f2152177
0x7f256066a9e8:   7f25a5af5a58 f215199f
0x7f256066a9f8:   7f25a573cae8 000794765f60
0x7f256066aa08:   0007c00d41e0 f21519ec
0x7f256066aa18:   7f25a5af5a58 f21519a3947655f0
0x7f256066aa28:   0007947664a0 000794766fa8
0x7f256066aa38:   7f25a5af5a58 f2151e2b6066aa80
0x7f256066aa48:   000794764c40 0007947656f8
0x7f256066aa58:   7f25bc2f28b0 f21519ac
0x7f256066aa68:   7f25a573cae8 7f256066aac0
0x7f256066aa78:   7f25bbcd0e20 f21519ac
0x7f256066aa88:   7f25a5af59b8 f21519afb5e99800 

Instructions: (pc=0x7f25a57c5b6c)
0x7f25a57c5b4c:   5b 30 49 b8 30 32 1b c0 07 00 00 00 4d 3b d8 75
0x7f25a57c5b5c:   30 49 8b f2 48 c1 e6 03 90 48 b8 ff ff ff ff ff
0x7f25a57c5b6c:   ff ff ff e8 14 d9 d7 ff 44 8b 58 08 41 81 fb 27
0x7f25a57c5b7c:   64 03 f8 75 24 48 83 c4 20 5d 85 05 74 14 74 17 

Register to memory mapping:

RAX=0x0007c0061210 is pointing into metadata
RBX={method} {0x7f25622e2870} 'apply' '(Ljava/lang/Object;)Ljava/lang/Object;' in 'scala/util/parsing/combinator/Parsers$Parser$$Lambda$107'
RCX=0xe404fdd3 is an unknown value
RDX=0x0007947664a0 is an oop
scala.util.parsing.input.CharSequenceReader 
 - klass: 'scala/util/parsing/input/CharSequenceReader'
RSP=0x7f256066a898 is pointing into the stack for thread: 0x7f25b5e99800
RBP=0xe4000482 is an unknown value
RSI=0xf21517ca is an unknown value
RDI=0xf28ece10 is an unknown value
R8 =0x0007c01b3230 is pointing into metadata
R9 =0xf1dfb1a3 is an unknown value
R10=0xf21517ca is an unknown value
R11=0x0007c01b3230 is pointing into metadata
R12=0x is an unknown value
R13=0x00072027ee98 is an oop
scala.util.DynamicVariable$$anon$1 
 - klass: 'scala/util/DynamicVariable$$anon$1'
R14=0xf803c74e is an unknown value
R15=0x7f25b5e998

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Makarius 
On 19/08/17 17:16, Manuel Eberl wrote:
> 
> on 158c513a39f5, I just had a JVM crash during "isabelle build" when it
> was building Isabelle/Scala.

Since the JVM crash happened during scalac compilation, I recommend to
enforce a fresh build, e.g. like this:

  isabelle jedit -b -f


> Log attached

This refers to a separate log file
/home/manuel/hg/afp-devel/hs_err_pid13339.log

If you still have that, can you send it to me?


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Lars Hupel 
> on 158c513a39f5, I just had a JVM crash during "isabelle build" when it
> was building Isabelle/Scala. (Log attached).

I had a similar problem today. Unfortunately I didn't save the logfile.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] [158c513a39f5] JVM crash

2017-08-19 Thread Manuel Eberl 
Hallo,

on 158c513a39f5, I just had a JVM crash during "isabelle build" when it
was building Isabelle/Scala. (Log attached).

When I did "isabelle build" again, it proceeded to build the Pure
session without problems. However, when I then tried to build
HOL-Computational_Algebra, it stopped and said
"HOL-Computational_Algebra FAILED", but the log did not contain any
error messages. The last message was

### theory "HOL-Computational_Algebra.Polynomial_Factorial"
### 10.690s elapsed time, 39.546s cpu time, 6.455s GC time

I wonder if this could also be due to a JVM crash.

Cheers,

Manuel
### Building Isabelle/Scala ...
Changed files:
  Admin/build_status.scala
  GUI/wrap_panel.scala
  General/file.scala
  General/http.scala
  General/path.scala
  General/url.scala
  PIDE/command.scala
  PIDE/document.scala
  PIDE/document_id.scala
  PIDE/markup.scala
  PIDE/protocol.scala
  PIDE/session.scala
  PIDE/xml.scala
  System/isabelle_tool.scala
  System/system_channel.scala
  Thy/html.scala
  Thy/sessions.scala
  Thy/thy_header.scala
  Tools/imports.scala
  Tools/server.scala
  library.scala
  ../Tools/Graphview/graph_panel.scala
  ../Tools/Graphview/tree_panel.scala
  ../Tools/VSCode/src/build_vscode.scala
  ../Tools/VSCode/src/grammar.scala
  ../Tools/VSCode/src/preview_panel.scala
  ../Tools/VSCode/src/protocol.scala
  ../Tools/VSCode/src/server.scala
  ../Tools/VSCode/src/state_panel.scala
  ../Tools/VSCode/src/vscode_javascript.scala
  ../Tools/VSCode/src/vscode_rendering.scala
  ../Tools/VSCode/src/vscode_resources.scala
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x7f25a57c5b6c, pid=13339, tid=0x7f256066c700
#
# JRE version: Java(TM) SE Runtime Environment (8.0_144-b01) (build 
1.8.0_144-b01)
# Java VM: Java HotSpot(TM) 64-Bit Server VM (25.144-b01 mixed mode linux-amd64 
compressed oops)
# Problematic frame:
# J 2075 C2 
scala.util.parsing.combinator.Parsers$Parser$$Lambda$107.apply(Ljava/lang/Object;)Ljava/lang/Object;
 (16 bytes) @ 0x7f25a57c5b6c [0x7f25a57c5b00+0x6c]
#
# Core dump written. Default location: /home/manuel/hg/afp-devel/core or 
core.13339
#
# An error report file with more information is saved as:
# /home/manuel/hg/afp-devel/hs_err_pid13339.log
#
# If you would like to submit a bug report, please visit:
#   http://bugreport.java.com/bugreport/crash.jsp
#
/home/manuel/hg/isabelle/lib/scripts/getfunctions: line 1: 13339 Aborted
 (core dumped) "$JAVA_HOME/bin/$PRG" "$@"
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev