call :prove or :check

[weaversa]

It would be nice to use the python interface for CI related things, but I can't figure out how to call the prover. Is this supported?

[pnwamk]

Those commands are not currently supported, but there’s no reason we can’t add them. I’ll make a note.

…

On Sat, Nov 14, 2020 at 2:10 PM weaversa ***@***.***> wrote: It would be nice to use the python interface this for CI related things, but I can't figure out how to call the prover. Is this supported? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#121>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA36B2VUXL6JQCC5YWKYVXDSP355VANCNFSM4TVZJHPA> .

[weaversa]

Also, please add :safe to the list.

[pnwamk]

Update: some initial work on prover interaction from the python API is here (it was already implemented in the server API but not exposed in the python API):
https://github.com/GaloisInc/argo/tree/cryptol-remote-api-sat
https://github.com/GaloisInc/cryptol/tree/cryptol-remote-api/sat

:prove should be a trivial addition to what :sat is already doing.

:check, and :safe will require just a little more work.

[atomb]

Now that GaloisInc/cryptol#1046 is merged, the equivalent of :prove and :sat are available. There's not yet an equivalent of :check or :safe, however, so I'll leave this open as a reminder.