Added documentation for REPL commands and :set-able options to reference manual

[pfisher-existx]

Added documentation as requested in #612

[RyanGlScott]

Thank you for writing this up!

[RyanGlScott]

This list should also include bitwuzla, sbv-bitwuzla, and w4-bitwuzla.

[RyanGlScott]

I don't think Cryptol ever displays multiple counterexamples, does it? Perhaps change the phrasing here to "will display a counterexample that returns false".

[weaversa]

Does cryptol’s ‘satnum’ option influence :prove?.

…

On Tue, Jan 14, 2025 at 7:23 AM Ryan Scott ***@***.***> wrote: ***@***.**** commented on this pull request. Thank you for writing this up! ------------------------------ In docs/RefMan/REPLCommands.rst <#1790 (comment)>: > + **Valid values:** ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``boolector``, + ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, + ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, + ``sbv-offline``, ``sbv-any``, ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, + ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any`` This list should also include bitwuzla, sbv-bitwuzla, and w4-bitwuzla <#1787>. ------------------------------ In docs/RefMan/REPLCommands.rst <#1790 (comment)>: > + +``:m [MODULE]``, ``:module [MODULE]`` + Load a module by its name. + +``:module-deps MODULE`` + Show information about the dependencies of a module. + +``:new-seed`` + Randomly generate and set a new seed for the random number generator. + +``:prove [EXPR]`` + Use an external solver to prove that the argument always returns true. (If + no argument, check all properties.) + + If the expression is successfully proven, the screen will display ``Q.E.D``. + If not, the screen will display some counterexamples that return false. I don't think Cryptol ever displays *multiple* counterexamples, does it? Perhaps change the phrasing here to "will display a counterexample that returns false". — Reply to this email directly, view it on GitHub <#1790 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABYQSOWC35T2KK34IV7PPHD2KT6U3AVCNFSM6AAAAABVEVZP32VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDKNBZGU3DAMJSGA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[RyanGlScott]

Not to my knowledge, no. The source code suggests that satNum is only used to influence the output of :sat, not :prove:

cryptol/src/Cryptol/REPL/Command.hs

Line 865 in 9e50047

qtype <- if isSat then SatQuery <$> getUserSatNum else pure ProveQuery

(getUserSatNum is the only place that reads the contents of the satNum setting, and this is the only call site for getUserSatNum.)

[RyanGlScott]

One last request: could you mention "fixes #612" somewhere in the commit message? That way, the issue will be automatically closed when the PR lands. Thanks!