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

2017-11-08 Thread Manuel Eberl
> You could try with a fresh build of Poly/ML: Okay, I rebuilt Poly/ML (not libsha1 and libgmp though; apparently your build script does not build those). The crashes still occured though. I think I did everything correctly, because when I delete the files that the compilation created, isabelle

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

2017-11-08 Thread Makarius
On 08/11/17 15:45, Manuel Eberl wrote: > Is there an easy way to disable that for testing purposes? Some line I > have to remove from a .scala file or something? It should be sufficient to remove the is_pure() here:

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

2017-11-08 Thread Manuel Eberl
Is there an easy way to disable that for testing purposes? Some line I have to remove from a .scala file or something? Manuel On 2017-11-08 15:44, Makarius wrote: > On 08/11/17 15:39, Manuel Eberl wrote: >>> If these crashes are happening at the end of the build process I would >>> suspect that

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

2017-11-08 Thread Makarius
On 08/11/17 15:39, Manuel Eberl wrote: >> If these crashes are happening at the end of the build process I would >> suspect that it is something to do with either the data sharing or >> writing out the heap image. > > Does writing out of the heap happen also when I just do "isabelle build > Pure"

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

2017-11-08 Thread Manuel Eberl
> If these crashes are happening at the end of the build process I would > suspect that it is something to do with either the data sharing or > writing out the heap image. Does writing out of the heap happen also when I just do "isabelle build Pure" as opposed to "isabelle build -b Pure"? Because

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

2017-11-08 Thread Makarius
On 08/11/17 09:21, Manuel Eberl wrote: > > After a lengthy bisection, I found that the first revision where no > crashes occur is this one: > > changeset:   66920:aefaaef29c58 > user:    wenzelm > date:    Thu Oct 26 13:44:41 2017 +0200 > summary: use Poly/ML 5.7.1 test version as

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

2017-11-08 Thread David Matthews
If these crashes are happening at the end of the build process I would suspect that it is something to do with either the data sharing or writing out the heap image. Writing the heap image does not involve any concurrency but the data sharing does, so I would suspect the latter. That has

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

2017-11-08 Thread Manuel Eberl
I was not able to find out what exactly crashes and why, but while trying to do that, I found out that the problem is actually not present in the development version of Isabelle anymore. After a lengthy bisection, I found that the first revision where no crashes occur is this one: changeset:  

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

2017-09-04 Thread Manuel Eberl
Alas, it would appear I have spoken too soon! I experienced a strange build failure with RC1 yesterday and, fearing the worst, did my experiment from a few weeks ago again, with the following result: – building "Pure" fails in around 6 % of the cases – this does not change even after a cold

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

2017-08-20 Thread Manuel Eberl
Addendum: I did a system upgrade (including a major kernel upgrade) around the same time when I first noticed the problem and I don't think I rebooted afterwards, so one very plausible explanation is that Linux introduced some workarounds/bug fixes in the kernel within the last few weeks that

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

2017-08-20 Thread Manuel Eberl
Okay I have no idea what is going on anymore. I know have the following new data points: – 2500 iterations on my Intel Core i7 laptop. No failures. So it must be the Ryzen issue after all, I thought. I recalled that some people said the problem was less pronounced with SMT disabled, so I

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

2017-08-20 Thread Lars Hupel
> Lars, maybe you can run the same test on your machine and see what > happens there. I did, and nothing happened for about 100 iterations. I have a Core i7-2600. OS is otherwise identical to Manuel (Arch Linux). > As for Scala, could a problem in the Scala compiler really lead to the > JVM

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

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

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

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

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.

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

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 ...

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

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