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:
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:
It shows "bf5ddf4ec64b".
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
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.
I put 'ML_OPTIONS="-H 1000" ' in my user etc file and it makes no
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and