[polyml] standard input contains a leading blank line? (5.5.2 with --enable-shared)

Michael, I've had a look at that and I think I've fixed it in SVN trunk. The problem was that the buffer associated with stdIn was not being cleared so the remaining input after the PolyML.export line, in this case just the end of that line, was being read when your program started. There was actually a fix for this problem but it only applied if stdIn was its original imperative stream. Poly/ML 5.5.1 and 5.5.2 test whether stdIn is an interactive stream and in order to do that they have to rebuild stdIn based on a functional stream so the original fix no longer worked. It should work properly now. If there are no other problems associated with the fix I'll apply it to the 5.5.2-fixes branch.

David

On 28/05/2014 05:56, Michael Norrish wrote:

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
       recurse 1
     end;

 PolyML.export("mytest", doit);

and I then do

 $ poly < foo.ML
 $ cc -o mytest mytest.o -lpolymain -lpolyml
 $ echo "hello, world" | ./mytest

I get

 1:
 2: hello, world

as output.

This is with a polyml 5.5.2 just downloaded from Sourceforge and configured with --enable-shared. I'm pretty sure this used to work (a minor feature of the HOL4 build process depended on it).

Michael