Scryer-prolog: format/3 may sometimes fail to write all characters

[triska]

I think the following call may under some circumstances fail to write all bytes: https://github.com/mthom/scryer-prolog/blob/7e7aa7992ab633058d9002bc1149426681589400/src/machine/system_calls.rs#L2140

It would be nice to find a test case, using for example format/3 from library(format), that exhibits this problem, and then augment the code to reliably write all characters.

This could be an interesting issue for contributors who are interested in Rust.

[notoria]

The issue should be reproducible with:

:- use_module(library(format)).
:- use_module(library(lists)).

test(N) :-
    open('/tmp/a.txt', write, S),
    length(Data, N),
    maplist(=(a), Data),
    format(S, Data, []),
    close(S).

And:

#!/bin/sh

while true; do
    for i in $(seq 0 1024 65536); do
        scryer-prolog -g "test($i)" -g halt test.pl
        if [ "$(wc -c /tmp/a.txt | cut -d' ' -f1)" != "$i" ]; then
            echo Error: $i != $(wc -c /tmp/a.txt | cut -d' ' -f1)
            break
        fi
    done
done

The solution would be to use write_all.

[triska]

Brilliant, many thanks for looking into this, and for suggesting this correction!

I have filed #694 to address this.

Before your test case, I managed to reproduce the problem only with TLS connections:

1. On host H, open a TLS server on port 8785, using cert.pem, fullchain.pem and privkey.pem as produced by Let's Encrypt:

   $ openssl s_server -cert cert.pem -cert_chain fullchain.pem \
                       -key privkey.pem -port 8785
   

2. Consult the following definitions:

   :- use_module(library(format)).
   :- use_module(library(sockets)).
   :- use_module(library(dcgs)).
   :- use_module(library(clpz)).
   
   list(0) --> [].
   list(N) -->
           format_("~D ", [N]),
           { N1 #= N - 1 },
           list(N1).
   

   Then, open a TLS connection to H, and send list Ls:

   ?- socket_client_open(<H>:8785, Stream, [tls(true)]),
      phrase(list(4000), Ls),
      format(Stream, "~s\n", [Ls]).
   

   yielding:

   %@    Stream = '$stream'(0x5624d2d70590), Ls = "4,000 3,999 3,998 3 ..."
   %@ ;  false.
   

   However, the server's echo ends with:

   ... 1,273 1,272 1,271 1,27
   

Your test case is much more elegant, exhaustive and simpler to set up, thank you again!

[triska]

This works brilliantly now, thank you a lot!