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