Poly/ML

polyml@lists.polyml.org

2 participants
698 discussions

Isabelle/PIDE front-end for Poly/ML debugger
by makarius＠sketis.net 20 Aug '15

20 Aug '15

Dear friends of the most advanced Standard ML system on the planet. Some month ago, David Matthews has reworked the internal interface for source-level debugging, see also http://www.polyml.org/documentation/Reference/PolyMLDebuggerInterface.html (This requires an intermediate repository version of Poly/ML, until a proper release emerges.) I've already wrapped up the debugger in the Prover IDE framework of Isabelle. A fully integrated version can be downloaded for testing here: http://www4.in.tum.de/~wenzelm/test/Isabelle_20-Aug-2015 and a minal example here: http://www4.in.tum.de/~wenzelm/test/Isabelle_20-Aug-2015/Debugger_Example.t… The Debugger panel can be opened via the Isabelle/jEdit menu "Plugins / Isabelle / Debugger panel" or the jEdit action "isabelle-debugger". Without such a panel, there is no effect on the running ML program. What is also interesting in this preview of the next Poly/ML release is native support for x86-windows, based on MingW32 instead of Cygwin. Cygwin remains the portable system glue for the Isabelle environment, but both the IDE front-end (Scala/JVM) and the ML backend are now fully at home on Windows. Makarius

1 0

error building from SVN
by Michael.Norrish＠nicta.com.au 11 Aug '15

11 Aug '15

My Travis CI builds of HOL using a Subversion checkout of Poly (as opposed to the released version, which I also check), are failing to build Poly with the error below. (See also https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/56529081). Is this expected, or some quirk of the Travis setup? Michael -- Error- in './basis/FinalPolyML.sml', line 1607. Value or constructor (decodeBinary) has not been declared Error- in './basis/FinalPolyML.sml', line 1608. Value or constructor (encodeBinary) has not been declared Exception trace for exception - Fail raised in mlsource/MLCompiler/MAKE_.ML line 423 MAKE_().useIntoEnv(2) <top level> CODETREE().genCode(3)(1) COMPILER_BODY().baseCompiler(3)executeCode(1) End of trace Exception trace for exception - Fail raised in mlsource/MLCompiler/MAKE_.ML line 423 MAKE_().useIntoEnv(2) <top level> CODETREE().genCode(3)(1) COMPILER_BODY().baseCompiler(3)executeCode(1) End of trace ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

9 18

Truth Tables
by dtopham＠gmail.com 30 Jul '15

30 Jul '15

As part of my ongoing efforts to introduce the use of SML to complement the teaching of discrete math, I have prepared some slides showing one way to print truth tables. Since my knowledge and experience in SML is so limited, I would appreciate any constructive comments on how to improve this approach. (I am afraid my many years of using C++ has made it difficult to transition to the functional way of thinking!) Attached is pdf of slides with SML embedded. (similar to literate programming). I am grateful for the use of ProofPower as a development environment since it allows me to combine Latex and SML in one document and extract the pieces when needed. -Dave

1 0

Interpreter commands?
by dtopham＠ohlone.edu 17 Jul '15

17 Jul '15

Are there commands for the PolyML interpreter to do things list the values in the current environment? e.g. If I have loaded or defined several functions and then want to review them as reference to calling them correctly, is there a way to display their prototypes? (I did look through the documentation and tried to search the "archives" but I don't seem to have a search feature for that purpose) -Dave p.s. I did discover the use of rlwarp (on Linux) to solve the problem of not being able to use arrow keys within the interpreter--that is a nice addition for repeating previous commands. i.e. rlwrap poly

2 1

PolyML on AArch64
by chneukirchen＠gmail.com 13 Jul '15

13 Jul '15

Hi, I have added 64-bit ARM support for PolyML, using the interpreted mode. It seems to be enough to natively compile and run the test suite completely. Tested on Linux voidarm64 3.16.0-37-generic #51-Ubuntu SMP Tue May 5 13:51:19 UTC 2015 aarch64 aarch64 aarch64 GNU/Linux

2 2

polyml 64bit Darwin heap size
by Gerwin.Klein＠nicta.com.au 17 May '15

17 May '15

Hi, I?m running into problems with large heap sizes on 64bit Darwin. The machine I?m running on has 32GB physical memory, and runs out of polyml memory on sessions that take about 12GB on 64bit Linux. The error message is val it = (): unit ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised (This is from an Isabelle build of the image CBaseRefine in https://github.com/seL4/l4v/tree/master/proof) The initial heap size was specified as ?-H 2000?. Playing around with that option, I got for instance for ?-H 8000? the message: "Value of -H option is too large" I?m getting the same for trying to increase ?maxheap. The same -H 8000 option on a 64-bit Linux machine works fine. The check that throws this error seems to be: libpolyml/mpoly.cpp:177 // Check that the number of kbytes is less than the address space. // The value could overflow when converted to bytes. if (result >= ((POLYUNSIGNED)1 << (SIZEOF_VOIDP*8 - 10))) Usage("Value of %s option is too large\n", arg); As far as I can see, config sets the value of SIZEOF_VOIDP to 8 on both platforms, so I?m a bit mystified why one works and the other doesn?t. The polyml version is 5.5.2 (-3 in the Isabelle distribution, but same problem for vanilla 5.5.2). Any ideas? Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 1

polyc and poly --script
by rene.neumann＠in.tum.de 24 Mar '15

24 Mar '15

Hi, two completely orthogonal questions/remarks for PolyML 5.5.1: 1.) When building PolyML with '--with-system-libffi' the '-lffi' part is missing in the linker line in polyc. 2.) Is it somehow possible to see if an ML file is run via 'poly --script' or as a standalone executable? Because for the one the logic has to be wrapped in 'fun main ()', and for the other it should not :). (Ie, what I want: if is_script then main() else () ) Thanks, Ren? -- Ren? Neumann Institut f?r Informatik (I7) Technische Universit?t M?nchen Boltzmannstr. 3 85748 Garching b. M?nchen Tel: +49-89-289-17232 Office: MI 03.11.055

4 9

emacs SML mode
by dm＠prolingua.co.uk 20 Mar '15

20 Mar '15

Peter, I'm copying this to the Poly/ML list as you suggested. It would be nice to have SML emacs mode working with Poly/ML for those who would like to use it but my feeling is that it is rather old-fashioned. Poly/ML now supports a much more extensive interface designed for an IDE. The best example of this is Isabelle's ML mode. See http://sketis.net/2014/isabellepide-as-ide-for-standard-ml which has a nice screen-shot. Lucas Dixon and I both had a go at producing IDEs which were completely independent of Isabelle but we didn't get as far as Makarius has. It all works by having the Poly/ML compiler as a function which takes a large set of parameters most of which have simple defaults. All the interaction with the compiler is through ML functions. The default REPL just calls the compiler with streams connected to the console but it's very easy for a user to replace the REPL with something else. The Isabelle IDE is just using the Poly/ML compiler function but passing in parameters which capture error messages and also allow browsing of the parse-tree to get information about the types. So far the debugger hasn't been fully integrated with this but it's something I have in mind. The format that the default REPL uses for error messages was one that was used by various compilers at one time and it used to be possible to parse it automatically. If there's a more up-to-date format I'm happy to change to it. I don't know if anyone is parsing the current format automatically and would be inconvenienced by a change. David On 03/12/2014 03:26, Peter Gammie wrote: > Dave, > > I?ve been talking to Stefan about the SML mode for emacs that he > maintains. I?m hoping to use it with Poly/ML and it is starting to > come together. > > Stefan observed that it would be super-helpful if Poly/ML generated > errors in a standard format, such as e.g. the one that GCC or clang > use, as far as that makes sense. > > Would you be open to that? I could try to crank out some patches to > Poly/ML if so. > > BTW I am wondering how people interact with Poly/ML?s repl. With more > hacking it is likely to be somewhat emacs-friendly, but I?m still > struggling to understand how people have done it in the past. > > For instance, I presently more-or-less just load all modules into > poly with a series of ?use?s in dependency order. Now I?d like to use > the debugger and it seems I have to hack all this scaffolding to do > so. From the looks of it Isabelle does the same. > > Feel free to reply via the Poly/ML list if you prefer. > > Thanks for the awesome system. I hope I can make some use of the > concurrency! > > thanks, peter >

9 17

forgetVal(ue)
by peteg42＠gmail.com 15 Mar '15

15 Mar '15

David, I?ve been trying to repurpose your Poly/ML test harness, that encapsulates the tests in private namespaces. With some head scratching I got it to somewhat work, so thanks for that. One remaining nit is that the treatment of forgetVal(ue) does not take into account the current namespace. Did you have a reason for leaving it out of the PolyML.NameSpace.nameSpace record? cheers, peter

2 1

Typo in Socket.select
by hiroya.ebine1＠gmail.com 11 Mar '15

11 Mar '15

In Poly/ML source code, polyml/basis/Socket.sml, Socket.select function declared like this: val select: { rds: sock_desc list, wrs : sock_desc list, exs : sock_desc list, timeOut: Time.time option } -> { rds: sock_desc list, wrs : sock_desc list, exs : sock_desc list } But, basis library says: select {rds, wrs, exs, timeout} (http://sml-family.org/Basis/socket.html#SIG:SOCKET.select:VAL) It seems a typo. Argument "timeOut" shoud be "timeout". Please fix it or tell me where post a patch. Sorry for poor english. Thank you.

2 1

← Newer
1
...
21
22
23
24
25
26
27
...
70
Older →

Jump to page:

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