Poly/ML

polyml@lists.polyml.org

1 participants
698 discussions

determining if an outstream is a tty
by Michael.Norrish＠nicta.com.au 07 May '16

07 May '16

The Basis library documentation for OS.IO suggests that it should be possible to get one's hand on a primitive reader or writer iodesc by pulling things apart to get PrimIO values. Doing type-directed programming, I thought I might do this for a TextIO.outstream with > val getIOD = (fn TextPrimIO.WR r => #ioDesc r) o #1 o TextIO.StreamIO.getWriter o TextIO.getOutstream; val getIOD = fn: TextIO.outstream -> OS.IO.iodesc option This has the right type (and I couldn't see any other way of getting the right type). Unfortunately, I can't run it: > getIOD TextIO.stdOut; Exception Io raised while writing to stdOut. terminating the session. If this had worked, I then hoped to be able to call Posix.FileSys.iodToFD on the value, if there was one, and to then eventually call Posix.ProcEnv.isatty on the result of that, if present. Is there a right way to do this? Many thanks, Michael ________________________________ 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.

2 3

Posix implementation raising Fail exception
by Michael.Norrish＠nicta.com.au 25 Apr '16

25 Apr '16

As can be seen in https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/124717527 our use of Posix waiting is occasionally causing a Fail exception to be raised from inside the Posix implementation (there's no Fail exception with that message in our source code, and our code *is* doing a wait at that point). I'm afraid this doesn't seem easy to reproduce. Michael ________________________________ 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.

3 6

reliably crashing 5.6 on OSX 10.11.4
by Michael.Norrish＠nicta.com.au 25 Apr '16

25 Apr '16

The attached tarball (derived from a prefix of the HOL4 sources) reliably (every one of the tens of attempts I've made so far) crashes PolyML 5.6 on my Macbook Pro with Assertion failed: (save_vec_addr < save_vec+1000), function push, file save_vec.cpp, line 70. Abort trap: 6 Just change into the crashpoly directory and do poly --use usethis.ML If the call to Posix.Process.sleep in multiLib.sml is made for a much shorter length of time (pass 15 instead of 15000 to the genthms call, say), it works as expected. I also got 3/3 crashes with the time delay at 5000. I have tried to remove extraneous material from the tarball, but I'd be very surprised if it was minimal. Michael ________________________________ 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.

3 3

Assertion failure in scanaddrs.cpp
by lars＠hupel.info 15 Apr '16

15 Apr '16

Hi, I'm afraid I don't have a reproducible test case, but Gerwin Klein encouraged me to post and document this problem anyway. Using "polyml-5.6-1" bundled with Isabelle, we got the following assertion failure*: poly: scanaddrs.cpp:338: void ScanAddress::ScanRuntimeWord(PolyWord*): Assertion `w->IsDataPtr()' failed. $ uname -a Linux vm-10-155-208-88 3.16.0-4-amd64 #1 SMP Debian 3.16.7-ckt20-1+deb8u3 (2016-01-17) x86_64 GNU/Linux ML_OPTIONS="-H 8000" Cheers Lars * <https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/131/console>

1 0

Unhandled errors in StateLoader::LoadFile
by matthew.fernandez＠gmail.com 04 Apr '16

04 Apr '16

Hi there, In StateLoader::LoadFile one of the final blocks has the comment "If we get errors just skip the error and continue rather than leave everything in an unstable state." When the reloc is corrupted sure, but the logic in this block seems to ignore errors in some places it shouldn't. In particular, shouldn't we return false when the initial fseek fails [0] or when an fread fails [1]? It seems to me that continuing in these cases causes us to either read garbage or an uninitialised stack variable. Am I missing something here? Thanks, Matt [0]: https://github.com/polyml/polyml/blob/master/libpolyml/savestate.cpp#L1051 [1]: https://github.com/polyml/polyml/blob/master/libpolyml/savestate.cpp#L1058

2 2

random 5.6 runtime errors
by Michael.Norrish＠nicta.com.au 01 Apr '16

01 Apr '16

As per, for example, https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/118129741 we are seeing "Out of store" aborts with builds that work fine under 5.5.2. The example above is on a Linux virtual machine. We've also seen them on real (i.e., not virtualised) OSX machines. Is there something obvious we might be doing that could be causing this? We're running all our sessions with --gcthreads=1 as per discussion in http://permalink.gmane.org/gmane.comp.lang.ml.polyml.general/976 Michael ________________________________ 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.

2 1

Basis Library: select for file descriptors
by Michael.Norrish＠nicta.com.au 01 Apr '16

01 Apr '16

I can see there is select for socket descriptors in the Socket structure, but it doesn't appear as if there is one for file_descs in the Posix structure. Am I right? Will my multiplexing file-manipulator just have to busy loop over the descriptors I have? Michael ________________________________ 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.

2 2

Reducing the size of on-disk saved state
by matthew.fernandez＠gmail.com 31 Mar '16

31 Mar '16

Hi Poly folk, I am an Isabelle/HOL user interested in reducing the on-disk size of my Isabelle/HOL heaps. These are read and written via the save state functionality in Poly/ML. Saved states compress very well via conventional algorithms. On a representative Isabelle/HOL heap I see the following: $ ls -lh -r--r--r-- 1 matthew matthew 1.7G Feb 10 11:22 MyHeap -r--r--r-- 1 matthew matthew 279M Feb 10 11:22 MyHeap.bz2 -r--r--r-- 1 matthew matthew 331M Feb 10 11:22 MyHeap.gz -r--r--r-- 1 matthew matthew 173M Feb 10 11:22 MyHeap.xz I would like to propose integrating compression into the save state functionality itself. The runtime of Bzip and XZ are probably slow enough to irritate some users, but Gzip is reasonably fast for the benefit it shows. Gzipping saved states would require linking against zlib or something similar. David Matthews has suggested the save state code detect whether a state is compressed or not on loading and act accordingly, which would provide a nice transition path for users with existing saved states. I'm interested in hearing others' opinions about this proposal. If we feel this is something reasonable to do, I'll work on implementing this. When replying to this email, please CC me directly as I'm not subscribed to the list. Thanks, Matthew

5 15

playing with Posix fork/exec/dup2 etc
by Michael.Norrish＠nicta.com.au 18 Mar '16

18 Mar '16

Under 5.5.1, and after compiling with polyc, the code below gives an assertion violation and core dump: > $ ./a.out > In parent - reading > Assertion failed: (save_vec_addr < save_vec+1000), function push, file save_vec.cpp, line 70. > Abort trap: 6 (That's the OSX wording. I get something very similar under Linux.) I may well be making a hash of my POSIX programming, but I'd still hope for an exception rather than a core dump. Michael - - - - fun mkTIO_instream fd = let open Posix.IO val (flags,_) = getfl fd val rdr = mkTextReader { fd = fd, name = "", initBlkMode = O.anySet (flags, O.nonblock) } in TextIO.mkInstream (TextIO.StreamIO.mkInstream (rdr, "")) end fun main() = let open Posix.Process Posix.IO val {infd,outfd} = pipe() in case fork () of NONE => let val () = dup2{old = outfd, new = Posix.FileSys.stdout} val () = List.app close [infd, outfd] in exec("/bin/ls", ["ls", "."]) end | SOME pid => let val _ = print "In parent - reading\n" val strm = mkTIO_instream infd fun recurse () = case TextIO.inputLine strm of NONE => () | SOME s => (print ("Child: " ^ s); recurse()) in recurse(); wait(); print "Seen child's exit\n" end end - - - - ________________________________ 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.

3 3

Poly/ML Changes History
by rda＠lemma-one.com 18 Mar '16

18 Mar '16

I thought there was a changes history for Poly/ML somewhere on the Poly/ML website, but I can?t find it any more. It would be useful to have a list of changes between Poly/ML 5.5.2 and Poly/ML 5.6. Apologies if I am just being unobservant. Regards, Rob.

3 3

← Newer
1
...
15
16
17
18
19
20
21
...
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