[isabelle-dev] Multicore performance preview

Makarius wrote: On Tue, 21 Oct 2008, Stefan Berghofer wrote: Makarius wrote: You will need the latest Poly/ML 5.2.1 version to prevent a strange GC deadlock problem in 5.1/5.2. Where can I get the latest version? The latest version offered for download on the Sourceforge page

Re: [isabelle-dev] Fwd: status (AFP)

On 14/10/2011 10:02, Makarius wrote: On Fri, 14 Oct 2011, Gerwin Klein wrote: Is anyone else observing intermittent problems like this? Building Jinja ... poly: scanaddrs.cpp:107: PolyWord ScanAddress::ScanStackAddress(PolyWord, StackObject*, bool): Assertion `val.IsDataPtr()' failed.

Re: [isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

On 14/10/2011 09:13, Andreas Schropp wrote: On 10/13/2011 01:24 PM, Thomas Sewell wrote: Good day all. Just wanted to let the Isabelle developers know about the latest feature David Matthews has added to PolyML, and to let you all know how useful it is. The feature allows profiling of objects

Re: [isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

On 14/10/2011 10:56, Makarius wrote: On Fri, 14 Oct 2011, Andreas Schropp wrote: val dummy_task = Task(NONE, ~1) Values are not shared?! What the hell? Datatypes and tuples that contain only constant data are created once during compilation. This looks like an older version. Thomas was

Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click

Just to add that I'm very grateful for this support which enables Poly/ML to continue and get better with each release since I don't have a university or a big company behind me. If anyone has a feature that requires work on Poly/ML and a bit of money I'm happy to discuss it. David On

Re: [isabelle-dev] Max threads Sledgehammer

On 07/01/2013 10:11, Stefan Berghofer wrote: On 01/07/2013 10:45 AM, Makarius wrote: On Fri, 4 Jan 2013, Stefan Berghofer wrote: I am currently getting an exception Thread Thread creation failed after some time when compiling HOL with PolyML 5.5.0 on a machine with quite a few CPUs (I am

Re: [isabelle-dev] Max threads Sledgehammer

the problem. So how many cores do you have? I reckon it should work until 32 at the least. Well, obviously not :-( Intel has hyperthreading, so it will report 48 CPUs here, or do you have 12 cores that are reported as 24? Anyway, we should tell David Matthews about it as well -- he could restrict his

Re: [isabelle-dev] Max threads Sledgehammer

On 07/01/2013 17:49, Stefan Berghofer wrote: You could certainly hit limits on memory for stacks with a large number of threads particularly if the default stack size is large. What does ulimit -s say? You could try setting that smaller. ulimit -s says 102400 This is surprisingly large.

Re: [isabelle-dev] Segmentation faults

then I'm not getting anywhere. Has anybody else had this problem with Poly/ML? Since nobody else replied: I do get occasional segfaults from Poly/ML (not only running Isabelle, but also other ML code). David Matthews is usually quite responsive to bug reports. That's interesting. Is there any way

Re: [isabelle-dev] Segmentation faults

From that crash log it looks as though the crash happened in ML code rather than the run-time system itself. The source of the crash, though, could be a bug in the run-time system resulting in some addresses being mangled. It's difficult to say more without being able to reproduce it.

Re: [isabelle-dev] Isabelle_10-Sep-2013

bloat factor with every new release, although David Matthews was usually ahead of most big applications in recent years. In fact he is about to release Poly/ML 5.5.1 pretty soon, so a quick test with some repository version of Poly/ML might help (e.g. SVN 1843). I would suggest trying

Re: [isabelle-dev] Isabelle_10-Sep-2013

On 13/09/2013 11:08, René Thiemann wrote: I would suggest trying with the --stackspace option e.g. ML_OPTIONS='--stackspace 500' The Fail exception with Insufficient space arises in a number of places such as when trying to fork a thread. This requires memory outside the ML heap. The

Re: [isabelle-dev] Isabelle_10-Sep-2013

On 16/09/2013 11:28, Makarius wrote: On Fri, 13 Sep 2013, Makarius wrote: I've made my own tests with the following setup: Poly/ML SVN 1848 IsaFoR a44e26d6605e Isabelle a49ce8d72a44 AFP 4e87a0fc2528 ML_PLATFORM=x86-darwin

Re: [isabelle-dev] Pushing to AFP fails

On 18/02/2014 14:45, Andreas Lochbihler wrote: I am trying to push a changeset to Coinductive to the AFP, but I always get the following error message: remote: abort: could not lock repository /hg/p/afp/code: Permission denied abort: unexpected response: empty string Until last week, hg

Re: [isabelle-dev] PolyML crashes

Hi, I'm aware of a number of assertion failures that seem to occur intermittently. This is one of the ones on my list. I suspect they are all symptoms of the same bug but I have never been able to narrow it down or reproduce it. It does seem to occur when the memory management is under

Re: [isabelle-dev] Remaining uses of Proof General?

On 08/05/2014 11:25, Makarius wrote: On Thu, 8 May 2014, Thomas Sewell wrote: If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Preempting long-running

Re: [isabelle-dev] HOL-Proofs

code=3) *** error: can't allocate region *** set a breakpoint in malloc_error_break to debug *** Interrupt HOL-Proofs FAILED When I load the session interactively, I don't have a problem. Any hints what I should be doing? That is a Poly/ML heap allocation problem specifically on Mac OS X. David

Re: [isabelle-dev] Proper sign of gcd / lcm on type int

On 02/06/2016 08:19, Manuel Eberl wrote: I do think that we should enforce the same thing in the ML implementation of gcd/lcm. Any definition of gcd/lcm for integers where either of them may be negative does not make much sense to me. My guess would be that lcm can be negative in the

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

On 17/02/2016 21:47, Dmitriy Traytel wrote: ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised This looks like an attempt to allocate memory for something other than the heap. There are quite a few situations where this can happen. Try adding a --stackspace argument to

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

On 20/02/2016 00:08, Lars Hupel wrote: Thanks for the suggestion. I've deployed that change on all our build boxes. We'll see how it works out. The problem still persists, as can be witnessed from this log: This time,

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

On 22/02/2016 07:58, Lars Hupel wrote: Another possibility is to set the maximum heap size with --maxheap e.g. ML_OPTIONS="--maxheap 28G" If the application needs it Poly/ML will try to grow the heap to avoid doing a lot of garbage collection. That can result in it crowding out other parts of

Re: [isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

On 08/12/2016 15:01, Florian Haftmann wrote: Hi all, when testing polyml-test-7a7b742897e9 I found out that this breaks session Algebraic_Numbers in the AFP: *** At command "value" (line 42 of "/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy") ***

Re: [isabelle-dev] Slow builds due to excessive heap images

On 03/11/2017 19:07, Makarius wrote: On 03/11/17 19:26, Fabian Immler wrote: I looked at it once more: profiling told me that IntInf.pow (in combination with Par_List.map) seems to be the culprit. The following snippet shows similar behavior: ML ‹ fun powers [] = [] | powers (x::xs) =

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

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] NEWS: support for GHC

On 22/10/2018 14:05, Lars Hupel wrote: The binary provided by Homebrew does not exhibit that problem. I have no other information beyond that. I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there. Interestingly enough, I get Poly/ML warnings of the form: 14:11:19

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

On 23/01/2019 21:08, Makarius wrote: On 23/01/2019 12:05, David Matthews wrote: I've had a look at this under Windows and the problem seems to be with calls to IntInf.divMod from generated code, not from IntInf.pow.  The underlying RTS call used by IntInf.quotRem has changed in the 32-in-64

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

On 22/01/2019 23:01, Makarius wrote: On 22/01/2019 23:08, Fabian Immler wrote: On 1/22/2019 4:00 PM, Fabian Immler wrote: On 1/22/2019 2:28 PM, Makarius wrote: On 22/01/2019 20:05, Fabian Immler wrote: These numbers look quite extreme: The slowdown in polyml-5.7.1-8 is about a factor of 2-3

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

On 28/01/2019 09:20, Bertram Felgenhauer wrote: I've made sure that the machine is mostly idle; things will be much different if several processes start competing for the ressources. I intended to experiment with smaller numbers but have not yet done so. On another, similar machine,