Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

putStr in javascript backend has extra newline

Open iacore opened this issue 3 years ago • 3 comments

Steps to Reproduce

Compile this with idris2 --cg javascript test.idr

main : IO ()
main = do
    putStrLn "1"
    putStrLn "2"

Expected Behavior

1
2

Observed Behavior

1

2

iacore avatar Jun 28 '22 13:06 iacore

At first I thought this might be because we are using console.log for node. But it turns out this works just fine in node. This is an issue with the browser backend only...

...and it looks like we may have to live with it for a while.

https://stackoverflow.com/a/41817778

ProofOfKeags avatar Jun 28 '22 20:06 ProofOfKeags

Yeah, this is not an issue if you compile with the node codegen, which I'd recommend if you intend to run the code outside the browser. It has a more complete and precise coverage of the primitives.

In chrome, it looks like the newline is not displayed, so console.log('foo') and console.log('foo\n') are identical and the issue described above doesn't occur. The output on the console resembles the "expected behavior" above.

However, we do still have the issue that the following code will emit two log messages with the javascript codegen (the node codegen is fine, but the output only runs in node):

main : IO ()
main = do
    putStr "hello, "
    putStrLn "world"

That could be addressed but holding onto any tail after the last \n and prepending to the next prim__putStr, but I'm not sure if that's desirable.

As an aside - I wonder if the codegen could be adjusted to make IO/PrimIO work in a continuation passing style. Might be a heavy lift, but it would enable implementing more of the primitives on the javascript side (and implementing them on the node side without relying on the sync versions of the functions).

dunhamsteve avatar Jun 29 '22 04:06 dunhamsteve

That could be addressed but holding onto any tail after the last \n and prepending to the next prim__putStr, but I'm not sure if that's desirable.

This wouldn't be different than a lot of stdout flushing systems that buffer before sending it to the console. Not only that but line buffering isn't uncommon. Happy to knock this out if we decide we want it.

ProofOfKeags avatar Jun 29 '22 15:06 ProofOfKeags