[isabelle-dev] HOL-ODE-Numerics FAILED

2018-05-21 Thread Florian Haftmann
isabelle: 4acc029f69e9 tip afp: c0882468fab2 tip > HOL-ODE-Numerics FAILED > (see also > /home/haftmann/.isabelle/heaps/polyml-5.7.1_x86_64-linux/log/HOL-ODE-Numerics) >thm -> > int -> >int -> > int -> >int -> > (int * int * string) list -> >

Re: [isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Florian Haftmann
Do the problems persist if you remove ~/.isabelle e.g. to ~/.isabelle_tmp? Florian Am 21.05.2018 um 16:23 schrieb Lawrence Paulson: > Well, it worked on the third attempt. Same as two weeks ago. My guess is that > it pauses to wait for some resource: when it stalls, the process is still

Re: [isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Lawrence Paulson
Well, it worked on the third attempt. Same as two weeks ago. My guess is that it pauses to wait for some resource: when it stalls, the process is still visible but only uses 0.1% of the processor. Larry > On 21 May 2018, at 15:13, Manuel Eberl wrote: > > It works fine for

Re: [isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Manuel Eberl
It works fine for me. Did you perhaps switch on ML debugging/exception tracing? HOL becomes virtually impossible to build with that switched on. What is the content of your ".isabelle/etc/preferences"? Manuel On 2018-05-21 15:43, Lawrence Paulson wrote: > I am continuing to be plagued by HOL

[isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Lawrence Paulson
I am continuing to be plagued by HOL failing to build, stalling quite reproducibly after about two minutes of processor time. It's a big obstacle to getting any work done, so tips would be welcome. Larry ___ isabelle-dev mailing list