Poly/ML

polyml@lists.polyml.org

2 participants
711 discussions

Handling Interrupts
by Frank Pfenning 31 Dec '02

31 Dec '02

Along similar lines: I have a Twelf top-level function in server that should interrupt the current computation and return to the Twelf top-level, not to an ML debugger or the ML top-level. I saw the documentation on signals, but I don't see how to achieve the desired effect because the handler will be run in a different thread. Any advice or help would be appreciated. - Frank

3 5

Poly/ML -- Exporting stand-alone applications
by Frank Pfenning 20 Dec '02

20 Dec '02

I have ported the Twelf logical framework implementation from SML/NJ to Poly/ML. The changes were significant, because Twelf was not SML'97 standards compliant as far as its uses of module features are concerned. The only other change had to do with the absence of a Word32 structure in Poly/ML. Now I would like to export a standalone Twelf server. Usually, this is run as an inferior process to Emacs and should not carry the ML compiler, for example. The FAQ gives a method to achieve this (sort of) using PolyML.onEntry. Has there been any progress on making it possible to export stand-along executables? Thanks, - Frank ---------------------------------------------------------------------- Frank Pfenning Phone: +1 412 268-6343 Department of Computer Science Fax: +1 412 268-3608 Carnegie Mellon University Email: fp(a)cs.cmu.edu Pittsburgh, PA 15213-3891, U.S.A. URL: http://www.cs.cmu.edu/~fp/ ----------------------------------------------------------------------

1 0

Re: basis/Net* and basis/*Sock* modules (polyml digest, Vol 1 #26)
by jeremy＠discus.anu.edu.au 26 Nov '02

26 Nov '02

Another question: are the basis/Net* and basis/*Sock* modules documented anywhere? I have a version of the Basis document dated August 5, 1997 by Jonh Reppy. Has it been amended since? If yes, where can I get the current version? http://sml.sourceforge.net/Basis/ Jeremy

1 0

proc-enums?
by itz＠speakeasy.org 25 Nov '02

25 Nov '02

The documentation for CInterface says among many other things: We would like to convert C-enumerations like colour into an equivalent ML datatype, together with functions to convert between values of the datatype and ML integers. This can be achieved automatically by using the script proc-enums, contained in the scripts subdirectory of the source tree. I don't see any such script anywhere in the tarballs from which I built PolyML: driver, mlsource, or basis. In fact, if I should believe "locate" it isn't anywhere on my machine :) Where oh where is it hiding? -- Ian Zimmerman, Oakland, California, U.S.A. I did not vote for Emperor Bush. GPG: 433BA087 9C0F 194F 203A 63F7 B1B8 6E5A 8CA3 27DB 433B A087

2 2

feature request: make
by itz＠speakeasy.org 19 Nov '02

19 Nov '02

Would it be possible for PolyML.make to return a boolean indicating success/failure? -- Ian Zimmerman, Oakland, California, U.S.A. I did not vote for Emperor Bush. GPG: 433BA087 9C0F 194F 203A 63F7 B1B8 6E5A 8CA3 27DB 433B A087

2 2

PolyML 4.1.3 now released
by David.Matthews＠prolingua.co.uk 04 Oct '02

04 Oct '02

PolyML version 4.1.3 is now available. Below are a list of the major changes and bug fixes since the 4.1.2 release taken from the release notes. Version 4.1.3 has been available unofficially for a while but the release on the web site is now complete and this incorporates a few bug fixes which were only found during testing. As usual I welcome comments and bug reports and I'll try to respond fairly quickly but the response will depend on pressure of other work. David New features and Changes Printing control switches New switches have been added to the Poly/ML.Compiler structure to control the printing of declarations. In both cases the default setting is true. Setting PolyML.Compiler.printInAlphabeticalOrder causes declarations to be printed in the order in which they were made rather than in alphabetical order. Setting PolyML.Compiler.printTypesWithStructureName to false causes types to be printed without the structure from which they came. Large database support The support for large databases has been improved and it is now possible to create a database which will occupy all of the virtual memory reserved for it. The actual limits vary between operating systems and platforms but are typically around 400Mbytes. To aid this the -S option when running the disc garbage-collector (-d option), introduced in 4.1.1, has been extended with -Smin and -Smax. The options can be written using either -s or -S and with or without a space. Setting a size is now "sticky" so if no -s/-S option is given the previous limits are retained rather than being reset to the default. The -Smax option sets the limits to the maximum space available. This space now depends only on the size reserved for any parent databases and not, as before, on the history of the database. The -Smin option compacts the database into a size whose upper limit is set to the size actually in use before compaction. To make best use of it it is probably best to run it twice, once to compact the database and again to set the upper limits to the now reduced size. It is useful when a database has been created which will not be modified further but where child databases may be created. Compacting a database to the minimum size allows any child databases to occupy as much space as possible. The disc garbage collection has been changed so that it is now possible to use all the address space. Previously it was always necessary to reserve a certain portion of the space to allow the database to be collected. Bugs fixed Mac OS X 10.2 Mac OS X 10.2 introduced a undocumented change to the kernel interface when delivering signals. This meant that the original binaries will not run on 10.2. This has now been fixed. Crash on delivering console interrupt on PowerPC There was a bug in the Poly/ML process (lightweight thread) code on the PowerPC which caused a crash when a process terminated. This could happen when a user-installed signal handler was called, for example the console interrupt handler in Isabelle. Crash in equality code An error in the compilation of the equality function meant that certain expressions involving equality could cause a crash. This has been fixed.

2 3

Poly/ML on Mac OS X
by David.Matthews＠prolingua.co.uk 20 Sep '02

20 Sep '02

Several people contacted me about Mac OS X 10.2 so I decided to take the plunge and buy it. I managed to track down the problem and you can find an updated version of Poly/ML in http://www.polyml.org/distrib/polyml-macosx.4.1.3.tar.gz . This contains executable and database and will only run on version 10.2 . I'll update the source in due course. For those who are interested, the problem was that the kernel included with 10.2 calls a signal handler with different parameters from previous versions. Previously it was called with a sigcontext structure containing register information, now the kernel seems to follow Solaris in providing a ucontext structure. Poly/ML needs this information because it uses a variety of signals to deal with things such as writes to database mutables, long-precision arithmetic and garbage-collection traps. Needless to say the change was not documented and the signal man page still refers to sigcontext, indeed it appears not to have changed since 1994. The only way I managed to find out what was going on was to download the Darwin kernel source and look at that. At least the source is available. The way the change was made means that it would be difficult to provide a binary that would work under 10.2 and also earlier versions of Mac OS X. It's also difficult to provide source that will automatically select the correct version when it's compiled. I'm going to assume that most people will have upgraded to 10.2 and concentrate on that. Let me know if there are any further problems. David.

1 0

PolyML om Mac OS X 10.2 (Jaguar)
by kramer＠acm.org 12 Sep '02

12 Sep '02

--Apple-Mail-7--233804249 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; format=flowed I've tried the binary download for Max OS X on 10.2 (Jaguar) and found PolyML to "hang". It starts, but there's no input prompt. It chews cpu cycles though. Then I tried to compile the sources and ran into the problem below. ? Does anyone have a patch to make PolyML work on OS X 10.2? Thanks, - Reto $ cd driver; ./configure; make [...] cc -DGCC -DPOWER2 -DMACOSX -g -O2 -Wall -DDEFAULT_POLYPATH='".:/usr/lib/poly:/usr/local/lib/poly"' -c -o run_time.o run_time.c run_time.c: In function `init_run_time_system': run_time.c:1249: warning: implicit declaration of function `sigaltstack' cc -E -DPOWER2 -DMACOSX -DGCC power_assembly.S | tr ';' '\012' > powtemp.s cc -x assembler-with-cpp -o power_assembly.o -c powtemp.s power_assembly.S:673:Parameter syntax error (parameter 3) power_assembly.S:723:Parameter syntax error (parameter 3) make[1]: *** [power_assembly.o] Error 1 make: *** [none] Error 2 --Apple-Mail-7--233804249 Content-Transfer-Encoding: 7bit Content-Type: text/enriched; charset=US-ASCII I've tried the binary download for Max OS X on 10.2 (Jaguar) and found PolyML to "hang". It starts, but there's no input prompt. It chews cpu cycles though. Then I tried to compile the sources and ran into the problem below. ? Does anyone have a patch to make PolyML work on OS X 10.2? Thanks, - Reto $ cd driver; ./configure; make [...] cc -DGCC -DPOWER2 -DMACOSX -g -O2 -Wall -DDEFAULT_POLYPATH='".:/usr/lib/poly:/usr/local/lib/poly"' -c -o run_time.o run_time.c run_time.c: In function `init_run_time_system': run_time.c:1249: warning: implicit declaration of function `sigaltstack' cc -E -DPOWER2 -DMACOSX -DGCC power_assembly.S | tr ';' '\012' > powtemp.s cc -x assembler-with-cpp -o power_assembly.o -c powtemp.s <bold>power_assembly.S:673:Parameter syntax error (parameter 3) power_assembly.S:723:Parameter syntax error (parameter 3) </bold>make[1]: *** [power_assembly.o] Error 1 make: *** [none] Error 2 --Apple-Mail-7--233804249--

2 2

Problems interacting using stdin/stdout
by bart.jacobs＠cs.kuleuven.ac.be 26 Aug '02

26 Aug '02

Hi, I'm writing a program that runs Poly/ML as a child process, redirecting standard input and output. I'm working on the Windows XP platform. Poly/ML behaves suboptimally in this setting. I'm experiencing two problems. One problem is fatal, the other is very annoying. The fatal problem is that Poly/ML simply hangs at some point during the interaction. I suppose it's some kind of deadlock. The problem is reproducible in that it happens at the exact same point, every time I run the program with the same input. But the entire environment in which the program runs is so big (it's Isabelle) that I'm not going to try to describe it. I'm just hoping that someone out there already knows about this. I don't have a debugger now, but when I get hold of one, I will try to hunt down the bug myself. The annoying problem is that Poly/ML goes to sleep for 0.5 seconds after every command. My program feeds hundreds of commands at a time to Poly/ML, so this means a *huge* slowdown. Putting all commands on a single line is not an option, since I need to stop feeding commands as soon as a command prints an error message. I think I found the cause of this sleeping problem: it's the MsgWaitForMultipleObjects call in processes.c. In the comments in the source code, David Matthews explains that it's just too hard to avoid this. I'm sure that's true in the general case, when you're running many lightweight processes, all of which are reading, writing, doing GUI stuff, etc., but in my case, Poly/ML is really just a simple sequential single-threaded read-eval-print loop. So, what I'm saying is, would it be possible to do some special-casing for the one-lightweight-process case on the Windows platform, so that you could just do blocking I/O calls? (This would probably also solve the fatal problem described above.) And I also don't really need the DDE functionality, so that we could do away with the message pump. These problems would have caused me to defect to another ML implementation, if it wasn't that Poly/ML is simply by far the best implementation out there. Many thanks to David Matthews for this great piece of software! But again, I hope there is some way to fix these problems. Bart

1 0

problem installing polyml on linux
by baxter＠math.umn.edu 17 Jul '02

17 Jul '02

Hello all, after using polyml on my windows machine I decided to install it on our dept linux system, and seem to be doing something wrong (as usual!). I downloaded the gzipped tarred archive. When I try to start it I type poly ML_dbase Then I get the following message: Poly/ML RTS version I386-4.1.2 (14:43:27 Jan 15 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Segmentation fault I also downloaded the driver source and built poly with gcc 2.95.4 and glibc 2.2.5. I downloaded the i386 database by itself. Using these files gives the same result. Can anyone suggest what I should be doing here? Thanks, John

1 0

Jump to page:

2026

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