Re: [isabelle] Isabelle2014-RC0: Cygwin can't delete temp files, the prover terminates



On 14-07-11 11:57, Makarius wrote:
On Fri, 11 Jul 2014, Gottfried Barrow wrote:
It shows "bf5ddf4ec64b".
Do you have any special options? Notably the number of ML threads? The default is 0 and should give you the real number of CPU cores. You can check that within a theory document like this:

  ML "Multithreading.max_threads_value ()"

What precisely is your version of Windows?

Windows version: Windows 7 Home Premium.

ML "Multithreading.max_threads_value ()" output:
  val it = 4: int

It does the same thing when I run Isabelle2014-RC0 with no option changes, that is, using the first-time startup options in C:\Users\<myaccount>\.isabelle\Isabelle2014-RC0.

On 14-07-11 13:07, Makarius wrote:
On Fri, 11 Jul 2014, Makarius wrote:
Concerning the "Isabelle/HOL too big to fail" hypothesis: you can try to give a bit more ML heap, to make it feel more comfortably.
ML_OPTIONS="-H 1000"

I put 'ML_OPTIONS="-H 1000" ' in my user etc file and it makes no difference.

I'll run Isabelle_11-Jul-2014.exe with the default options, but it's possible I'll ride my bicycle first, thinking about Andre Greipel and Marcel Kittel, and how they've dished up a lot of humble pie the last few years to that guy who crashed out. Where's the dissing of Greipel now, that he's free to compete? Nice guys, who win.

Regards,
GB










This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.