Poly/ML July 2010

polyml@lists.polyml.org

5 participants
4 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

Fwd: [isabelle] insufficient memory exception in polyml
by kleing＠cse.unsw.edu.au 27 Jul '10

27 Jul '10

This looks more like a polyml issue than an Isabelle issue, so I'm reposting here. Since the below I've run a few more experiments, and the theory does run fine with image built after less than 25min with the current svn trunk version of polyml on x86_64-darwin (5.4 Experimental). However, with the polyml-3.1-fixes version, it is still running after 45min with memory usage approaching 7.5GB and still raising. I'm not quite sure how to proceed. I don't think I'll want to run our production proofs on an experimental polyml version. How experimental/far away from release is the current trunk? Cheers, Gerwin Begin forwarded message: > From: Gerwin Klein <gerwin.klein(a)nicta.com.au> > Date: 23 July 2010 4:06:19 PM GMT+02:00 > To: Isabelle Users ML <cl-isabelle-users(a)lists.cam.ac.uk> > Subject: [isabelle] insufficient memory exception in polyml > > I am currently updating a very large theory from Isabelle2009-1 to Isabelle2009-2. So far this update was less painful than previous one, but I seem to be stuck now: > > I am getting various versions of insufficient memory exceptions from polyml-5.3 after the theory has been fully processed at the point (I presume) where polyml is writing the image to disk, possibly while it is doing garbage collection. > > A sample output of the log file is (the log file is btw gzipped and the error code is success, but the image is never written): > > lemma ... [last lemma of thy] > val it = () : unit > val it = () : unit > ML> Exception- Fail "Insufficient memory" raised > ML> > > The platform is polyml-5.3.0_x86-linux > with > ISABELLE_USEDIR_OPTIONS="-M 1 -p 0 -q 0 -v true" > and unchanged standard ML settings. > > The machine has 8G of RAM and otherwise works fine for other big developments. > > On polyml-5.3.0_x86-darwin, I am getting the same with the same settings. With -M 2, I am getting a C level exception in polyml at the same point with the message to set a breakpoint in a malloc function on stdour/err (but the same exception in the log). > > On polyml-5.3.0_x86_64-darwin, I am getting with -M 1 the same log, and this message on std out: > > Building CKERNEL ... > poly(5949,0xa0a3e500) malloc: *** mmap(size=134217728) failed (error code=12) > *** error: can't allocate region > *** set a breakpoint in malloc_error_break to debug > Finished CKERNEL (0:32:51 elapsed time, 0:32:47 cpu time, factor 0.99) > > (possibly the same as the 32bit version, but I've lost the previous output. Can reproduce if needed) > > With -M 3 and -M 2, on 64bit Darwin, I am instead getting exceptions about not being able to start another thread (at the same point). Again, the machine has 8GB of RAM and is otherwise rock solid. > > The same image builds easily under 32bit and 64bit polyml 5.3.0 (same version) on machines with less than 4GB of memory in Isabelle2009-1. > > Any ideas? > > I've tried playing around with -H and --mutable/--immutable settings, without success, but I don't have a good guideline what to try. > > Cheers, > Gerwin > > >

4 8

PASCO 2010: Programming Challenge
by Daniel.Cordeiro＠imag.fr 13 Jul '10

13 Jul '10

Matrix product over multi-precision integer and gcd computation http://pasco2010.imag.fr/contest.html 21st-23rd July 2010 PASCO 2010 Programming Challenge http://pasco2010.imag.fr/ Call for Participation ---------------------- Since the 80s and during the 90s a lot of parallel algorithms was proposed for computer algebra. Thus, 30 years after few computer algebra system are able to exploit modern parallel architectures multi-core, cluster and GPUs. The International Workshop on Parallel and Symbolic Computation (PASCO) is a series of workshops dedicated to the promotion and advancement of parallel algorithms and software in all areas of symbolic mathematical computation. The pervasive ubiquity of parallel architectures and memory hierarchy has led to the emergence of a new quest for parallel mathematical algorithms and software capable of exploiting the various levels of parallelism: from hardware acceleration technologies (multi-core and multi-processor system on chip, GPGPU, FPGA) to cluster and global computing platforms. To push up the limits of symbolic and algebraic computations, beyond the optimization of the application itself, the effective use of a large number of resources -- memory and general or specialized computing units -- is expected to enhance the performance multi-criteria objectives: time, energy consumption, resource usage, reliability. This year the PASCO 2010 workshop organize two programming challenges on ones of the most fundamental algorithms arising in computer algebra and providing rich opportunities for high performance computing. The two problems are matrix multiplication and gcd computations. Instances of the problems are given on the web site. The competition will take place live during the PASCO 2010 workshop. The results of the competition will be presented as part of the PASCO 2010 program. All participating teams will run their program on a selected set of the problems. The rule of the game is available on the PASCO 2010 workshop site [http://pasco2010.imag.fr/contest.html]. We strongly encourage all developers of parallel program or developers of parallel computer algebra system tools to participate in the competition. Teams are invited to send a declaration of participation as soon as possible by sending a mail to the PASCO 2010 conference organizers at pasco2010(a)imag.fr with the following information: * The name of the team and the contact information (name, email address, institution or company) of each team member willing to participate to the PASCO 2010 programming contest; * The name of the contact person (interlocutor and team representative). Accounts will be created on machine to allow teams to prepare their competition. Important dates --------------- Team declaration of participation: 19 July 2010 Preparation of the team: From 18 June until 20 July (remotely) Final preparation day: Wednesday 21 July 2010 at the Conference location Face to face challenge: Thursday 22 July 2010 Publication of the results during the Conference banquet.

1 0

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 2010