Poly/ML July 2011

polyml@lists.polyml.org

5 participants
6 discussions

Inspecting structures
by ramana.kumar＠gmail.com 27 Jan '16

27 Jan '16

Is there a way to look at the contents (i.e. signature) of a structure without opening it? (I suppose you could just open it then call a lot of PolyML.Compiler.forgetXXX, but that's quite tedious) Also, is it possible to retrieve the long path of an identifier in scope? Something that will, for example, take the rev in scope and say that it came from List. Finally, what about searching for an identifier that would come into scope if you opened some structures?

3 5

[Fwd: Re: [polyml] Building Poly/ML on MacOS X 10.6]
by rda＠lemma-one.com 29 Dec '14

29 Dec '14

I wrote: > I am completely baffled. I thought I hada solved all my problems on > MacOS X > 10.6 and was just tidying up, when I had to recompile a 32 bit > version of > Poly/ML to test a tidied up make file. This failed because > PolyML.Compiler.printTypesWithStructureName no longer exists. The same > problem happened when i rebuild a 64 bit version. What has happened? but it was a false alarm: my make file was wrong for other reasons and the absence of PolyML.Compiler.printTypesWithStructureName was not relevant. No doubt there are good reasons why this variable has been withdrawn. Regards, Rob.

3 6

Experiences with Lion
by aleks0＠gmail.com 24 Jul '11

24 Jul '11

Hi folks, I'm considering updating my system to OS X 10.7, though I'm wondering if it will torpedo poly (cf. Snow leopard). Has anyone had success/struggles running poly/ML under Lion? Aleks

1 0

Bug fixes and 5.4.1
by David.Matthews＠prolingua.co.uk 14 Jul '11

14 Jul '11

There have been a few bugs fixed since the release of 5.4. I've now back-ported the fixes to the 5.4-fixes branch and updated the pre-built compilers for all the architectures. The two issues that seem to have caused particular problems are the divide instruction bug that caused an assertion fault in the garbage collector and the failure to pass floating point rounding control that meant that IEEEReal.setRoundingMode didn't have any effect. I'm planning to release this as a bug-fix release in the next week or so unless anyone reports any problems. Because the pre-built compilers have been updated it should only be necessary to run ./configure make in the fixes branch. Run "make distclean" if necessary to get a clean directory. David

2 1

measuring/profiling memory consumption
by kleing＠cse.unsw.edu.au 07 Jul '11

07 Jul '11

What is the best way to measure memory consumption in polyml? Background: we're running out of memory after porting some of our tools and proofs to Isabelle-2011. It seems that the main problem is that we are now producing more objects that can later be shared, i.e. we think we were able to get memory consumption down by sharing more often (using PolyML.shareCommonData PolyML.rootFunction, not sure if this is the sane thing to do). It's still too much for saving the state at the end of the session on a 32bit system, though. On 64bit systems, we seem to need about 12GB for something that fit into about 2G on 32bit before. We tried various measurements and tried to bisect where in Isabelle or our code the problem was introduced, but we're only getting strange results - seemingly completely unrelated changes. My guess is that we didn't measure right. We used PolyML.objSize PolyML.rootFunction as an approximation of the overall memory consumption, but that doesn't always seem to correspond. What is the best way to figure out more precisely what is going? More specifically, I'd like to figure out: - maximum total memory consumption of the polyml process in a complete program run - current non-garbage heap consumption at a given point in the program - more detailed view of which type of object is how big and occurs how often at a given point Does anyone have more experience with this kind of thing? Cheers, Gerwin

2 1

Assertion `val.IsDataPtr()' failed
by alex.merry＠cs.ox.ac.uk 01 Jul '11

01 Jul '11

I think Lucas has probably mentioned this problem that we keep running into with quantomatic. I'm using Poly/ML 5.4 (ie: the lastest version of the 5.4 branch from subversion). Occasionally (or, in my case, frequently) we get the following error: poly: scanaddrs.cpp:107: PolyWord ScanAddress::ScanStackAddress(PolyWord, StackObject*, bool): Assertion `val.IsDataPtr()' failed. There appears to be no rhyme or reason to it. Re-running poly with the same code another time will not necessarily produce this assertion, or may produce it in a different place. It happens regardless of compiler optimisations (I've tried -O3, -O2 and -O0). I managed to get a backtrace: #0 0x0000003ff54330c5 in raise () from /lib64/libc.so.6 #1 0x0000003ff5434a76 in abort () from /lib64/libc.so.6 #2 0x0000003ff542b905 in __assert_fail () from /lib64/libc.so.6 #3 0x00007ffff7dc357e in ScanAddress::ScanStackAddress (this=0x7fffffffde10, val=..., base=0x7fffed6b56c0, isCode=false) at scanaddrs.cpp:107 #4 0x00007ffff7dc3811 in ScanAddress::ScanAddressesInObject (this=0x7fffffffde10, obj=0x7fffed6b56c0, lengthWord=4827858800541175088) at scanaddrs.cpp:146 #5 0x00007ffff7d9b4e2 in ProcessMarkPointers::ScanAddressesInObject (this=0x7fffffffde10, base=0x7fffed6b56c0, L=4827858800541175088) at gc.cpp:509 #6 0x00007ffff7dc42c8 in ScanAddress::ScanAddressesInObject (this=0x7fffffffde10, base=0x7fffed6b56c0) at scanaddrs.h:86 #7 0x00007ffff7dc3d48 in ScanAddress::ScanAddressesInRegion (this=0x7fffffffde10, region=0x7fffed6a3af0, end=0x7fffed6c3000) at scanaddrs.cpp:252 #8 0x00007ffff7d9ad12 in OpMutables (process=0x7fffffffde10) at gc.cpp:348 #9 0x00007ffff7d9d2cc in doGC (doFullGC=false, wordsRequiredToAllocate=3) at gc.cpp:1341 #10 0x00007ffff7d9f473 in QuickGCRequest::Perform (this=0x7fffeaa10cc0) at gc.cpp:1955 #11 0x00007ffff7da732c in Processes::BeginRootThread (this=0x7ffff7ffa8e0, rootFunction=0x605278) at processes.cpp:1253 #12 0x00007ffff7d9a472 in polymain (argc=3, argv=0x7fffffffe218, exports=0xf72a00) at mpoly.cpp:205 #13 0x0000000000400659 in main (argc=3, argv=0x7fffffffe218) at polystub.c:43 I don't know how useful that is, though. Alex

2 4

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML July 2011