[polyml] Building an executable that runs the read-eval-print loop

Rob,

Inside polyc, poly is invoked with -q to suppress output. This flag sets the print depth to zero and this is being inherited by your application. In your second example, you would also lose the output if you specified -q as follows:

poly -q < t.ML polyc -o t t.o

You could add val () = PolyML.print_depth ... to the end of t.ML. If you add it before the end, polyc output will no longer be suppressed. Alternatively you could add val () = PolyML.onEntry (fn () => PolyML.print_depth ...) anywhere. Unlike PolyML.export, using PolyML.print_depth avoids having to mention the object file name.

Regards, Phil

On 27/03/19 18:48, Rob Arthan wrote:

I wanted to create an executable that runs the Poly/ML read-eval-print loop with some code of mine precompiled. What I found was that the print part of the read-eval-print loop doesn't work if I compile from source with polyc, but does work if I use PolyML.export to create a .o file and then link it with polyc.

For example, if I have a file t.ML containing the following two lines:

fun p s = (TextIO.output(TextIO.stdOut, s); s); val main = PolyML.rootFunction

and compile it with:

polyc -o t t.ML

and then run:

echo 'val x = p "Boo!\n"' | t

the output I see is:

Poly/ML 5.7 Release Boo!

So it's executed my code, but it hasn't printed the usual report on the new value binding for x.

So I copied what I do in ProofPower, which does something similar but doesn't have this problem. I appended the following line to t.ML:

val _ = PolyML.export ("t", main);

and compiled it with:

poly < t.ML polyc -o t t.o

Then when I run t as above, I see the output, I'd expected to get:

Poly/ML 5.7 Release Boo! val x = "Boo!\n": string

The work-around is easy, but it would be nice to be able to compile from source to executable directly (and to minimise the Poly/ML-specific code in my source).

Regards,

Rob.

---

polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml