jjduan wrote:
I have a Virtualbox set up on Windows 7 64 bit. On top of it I run Ubuntu.
My intention is to build HOL on Ubuntu.
However I ran into some issue which is weird. It appears on Ubuntu
9.10/9.04, 32 or 64 bit, Polyml 5.3 or 5.2.1. Seems to be a universal
issue. I know someone who runs
I tried this out under the debugger and found it was actually ls
itself that was crashing. I suspect the reason for the difference in
behaviour has to do with differences in the implementation of /bin/ls
on different platforms. When calling Posix.Process.exec you have to pass
all the arguments
In the above code the invoker will return immediately with success. It
ought to be possible to modify the code to use Posix.Process.waitpid to
wait for the child process. Possibly something along the lines of
SOME pid =
(case Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) of
W_EXITED =
I have a Linux shell-script that calls
poly-image script
and which is being dying unexpectedly in a cronjob. The end of the log looks
like:
Poly/ML 5.3 Release
Killed
/home/michaeln/stdhol/bin/Holmake: Failed script build for
arm_improved_gcScript - exited with code 89
Build failed in
On 13/05/10 11:01, Michael Norrish wrote:
The presence of Killed makes me think that the script is being killed
by an external signal, perhaps a SIGSEGV caused by hitting a limit on
stack-size. But is this plausible? Would Poly/ML catch that signal and
then exit with 89?
Experiments reveal
On 17/09/12 00:02, Rob Arthan wrote:
Object files now use standard text and data areas when exporting. In
particular this means that it is no longer necessary to use --segprot on Mac
OS X to avoid a bus error.
I have make files that detect Mac OS X and insert the -segprot option
On 22/04/13 4:29 PM, Andreas Rossberg wrote:
On Apr 22, 2013, at 03:31 , Michael Norrish
michael.norr...@nicta.com.au wrote:
Is the following really supposed to be acceptable? Both Poly/ML and
mlton accept it without complaining:
datatype '+ = C | D;
(Moscow ML rejects it. mlton
On 22/04/13 18:54, Andreas Rossberg wrote:
Incidentally, I think that makes your grammar at
http://www.mpi-sws.org/~rossberg/sml.html incorrect: the grammar there
wants an id to follow the apostrophe for var, and ids have at
least one character in them.
Yes, you are right. I was
Using PolyML 5.5.0 as downloaded from Sourceforge, we can reliably produce:
Exception- InternalError: indirect - invalid constant address raised while
compiling
Exception- InternalError: indirect - invalid constant address raised while
compiling
We can also regularly, but somewhat less
A minimally modified version of the file at
https://raw.github.com/mn200/HOL/master/src/bool/boolScript.sml
takes 83 seconds to be “used” (using PolyML.use) into an interactive PolyML
session.
There are a great many files that need to be used before boolScript gets to
work, but none of
run? I
appreciate that it may not be easy but it's really the only way I can make
any sense of this.
Regards,
David
On 10/12/2013 06:05, Michael Norrish wrote:
A minimally modified version of the file at
https://raw.github.com/mn200/HOL/master/src/bool/boolScript.sml
takes 83 seconds
Is there any way to detect if the system has been built with --enable-shared?
Something in the PolyML structure (say)? I'd like to be able to have my build
script abort if the PolyML hasn't been built correctly. Or is there anything
obvious my script could check in the file system to make this
I seem to be able to pretty reliably produce the following:
Exception- InternalError: indirect - invalid constant address raised while
compiling
Exception- InternalError: indirect - invalid constant address raised while
compiling
Unfortunately, it takes hours to get there...
Switching to
If the following is foo.ML:
fun doit () =
let
fun recurse i =
case TextIO.inputLine TextIO.stdIn of
NONE = ()
| SOME l = (print (Int.toString i ^ : ^ l);
recurse (i + 1))
in
If you search github with its builtin search functionality, you can do so by
what github thinks is the primary language of project with the language:
modifier. I just tried
language:sml
and got back 950 results.
These are not necessarily all genuine. For example, the first hit I got, the
of commits are complete.
Does anyone have any thoughts on this?
David
On 31/03/2015 09:56, Michael Norrish wrote:
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
, Michael Norrish wrote:
(I'll attempt to attach the tgz file to this message, but if 817KB is too big
and this bounces or the attachment is dropped, I'll make it available
separately.)
If compiled with Poly/ML, the attached program performs abysmally on the
provided testcase.sml input file
It would be useful for HOL4 if polyc could be used with a different base
executable. At the moment, the shell-script is hardcoded to use e.g.,
/usr/local/bin/poly. If HOL has created a different heap H with a lot of
preloaded context, but for which the main function is still
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
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
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
vid
>
> On 24/03/2016 00:48, Michael Norrish wrote:
>> 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-manip
leep that was exactly this
> problem but it seems that the bug was left in Posix.Process.sleep. I've
> committed a fix to git master that seems to fix it. It could be worth adding
> this and a few other fixes to the fixes branch and perhaps making a new
> release.
>
> David
&
at
> raises the question of where this value is coming from and how it should be
> treated. Does this seem to fit with your code? Are you using
> Posix.Process.fromStatus and where is the value coming from?
>
> David
>
> On 21/04/2016 12:34, Michael Norrish wrote:
>>
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
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
gt; is_term_in)
> to fix that before anything (e.g., the read-eval-print loop) attempts to do
> I/O on the stream.
>
> Regards,
>
> Rob.
>
>
>> On 7 May 2016, at 06:01, Michael Norrish <michael.norr...@nicta.com.au>
>> wrote:
>>
>> The Basi
I’m getting random SIGSEGVs while building HOL with latest git on an Apple
Silicon MacBook Pro. These don’t always occur, but when they do, they have (so
far) always been in one of two places.
Michael
> On 16 Jan 2022, at 10:51 pm, David Matthews
> wrote:
>
> The long-promised update to
I see signal 11 (seg fault) periodically, but I just also saw
> Assertion failed: (space->partialGCScan+length+1 <= space->lowerAllocPtr),
> function ScanOwnedAreas, file quick_gc.cpp, line 499.
This is running SHA bafe319b.
--
Michael Norrish
School of Computing, Aust
29 matches
Mail list logo
