Zero-terminated REPL

[digama0]

This adds a new flag --zero to hol, which when enabled in conjunction with --repl causes HOL to use a zero-terminated REPL. This has the following semantics:

• User commands are separated by \0. All open lexer state is reset between blocks.
• Response from ML is terminated by \0. (The end of input counts as one additional input terminator, so if the input contains n \0's then the output contains n+1 \0's unless there is an abnormal exit.)
• As with the usual REPL, ML can begin processing commands as soon as it sees a complete command terminated by ;, but it will not send a \0 until the full block is concluded, and when timing is enabled, the timing will be aggregated over all commands in the block.

This resolves some parsing issues I encountered when writing the VSCode wrapper over the REPL.

[mn200]

Nice!

[mn200]

This may well turn out to be something that is constantly exercised, making explicit tests unnecessary, but just in case, can you think about putting something into a test directory for the regression machinery to check please?

[digama0]

Sure, although you'll have to walk me through what that entails

[digama0]

(I'm going to start working on the vscode parser for this format shortly, which may uncover more bugs.)

[mn200]

For a shell-level thing like this, I guess you could just add a Holmakefile target that runs a specified file into a built --zero REPL and then compares the result of the output with an "expected" file. E.g., in tools/Holmake/tests/quote-filter, we have

all: $(DEPS)
        $(protect $(HOLDIR)/bin/unquote) < input > output
        $(protect $(HOLDIR)/tools/cmp/cmp.exe) output expected-$(ML_SYSNAME)