[isabelle-dev] [158c513a39f5] JVM crash

[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
> 
-------------- next part --------------
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