Issuing prove_print command in interpreter results in extra output

[jpziegler]

Running saw on the following file (test.saw):

let thm = {{ \x -> x+x == x*(2:[32]) }};
prove_print abc thm;

Results in the following output:

$ saw test.saw
Loading module Cryptol
Loading file "test.saw"
Loading module Main
Valid

However, running the same commands directly in the interpreter results in extra output:

sawscript> let thm = {{ \x -> x+x == x*(2:[32]) }};
sawscript> prove_print abc thm;
Valid
Theorem (let { x0 = Cryptol.TCNum 2;
      x1 = Cryptol.TCNum 32;
      x2 = Cryptol.ePArith x3;
      x3 = Cryptol.seq x1
             Prelude.Bool;
    }
 in \(x::x3) ->
      Cryptol.ecEq x3
        (Cryptol.ePCmp x3)
        (Cryptol.ecPlus x3 x2 x x)
        (Cryptol.ecMul x3 x2 x
           (Cryptol.ecDemote x0 x1
              (Cryptol.ePFin x0)
              (Cryptol.ePFin x1)
              (Cryptol.ePGeq x1
                 (Cryptol.tcWidth x0)))))

[brianhuffman]

This is by design; it's made to match the behavior of ghci. In the interpreter, if you evaluate a command that has saw-script type TopLevel a and don't bind the result to a variable, then the return value of the command is printed (unless the return value is (), which never gets printed). Otherwise the result value would be lost.

I guess what's weird about prove_print is that it prints output to the screen and has a return value. In Haskell, most library IO functions just do one or the other. The name prove_print suggests that it prints something, so maybe we should make it return (). We'll consider this when we do our overhaul of the saw-script proof commands (see #9).

[jpziegler]

I originally ran into this with one of the examples from the tutorial. In that case, the amount of output was so large that most of it scrolled completely off the buffer of my terminal. Only after I increased the buffer size was I able to scroll up and see that "Valid" was printed at all.

I suggest adding variable bindings to the tutorial examples that use prove_print so that the code generates the same output in the interpreter as it does in a script. This would result in less confusion for new learners (like myself) who go off-book from time to time. Like so:

result <- prove_print abc thm;