Asserting outputs of vernacular commands and tactics

[radrow]

Render: https://github.com/radrow/rfcs/blob/vernact-output-assert/text/000-vernac-output-assert.md

Referenced issue: rocq-prover/rocq#20688

[Alizter]

This will act similarly to ppx expect for OCaml I suppose? https://github.com/janestreet/ppx_expect

[radrow]

This will act similarly to ppx expect for OCaml I suppose? https://github.com/janestreet/ppx_expect

Pretty much. That looks like a good source of further ideas.

[gares]

I like this proposal. I prefer Assert Output rather than With Output, or #[expected(output="...")].

[ybertot]

I think the proposal can also be very useful to write tutorials. I have two improvements to suggest:

• the expected output should appear in the script after the command that is concerned, so that the flow of reading looks more chronological
• It would be nice to be able to include a filter, a unix command that treats the both output string and the expected text and removes irrelevant information (I used such a filter in the Coq'Art book, where the aim was to be independent from spacing and indentation).

[radrow]

the expected output should appear in the script after the command

I'd also prefer the output to go after the command, but I can't come up with nice syntax for it (e.g. so that the desired output doesn't look like a parameter to the command and especially isn't confused with optional parameters). Maybe the command could be wrapped with some tokens, but that might look weird as afaik no existing commands use such syntax. You can throw ideas if you have any

[SkySkimmer]

Maybe we could separate into 2 commands, looking like

Capture Output Check foo.
Assert Output "foo : nat".

The original issue had

Check foo.
Output "foo : nat".

ie implicit capture with the assert applying to the previous command, but this wouldn't work well with eg proof general inserting arbitrary commands for itself between the user's commands.

With explicit capture we can insert non-captured commands without issue:

Capture Output Check foo.
Check bar.
Assert Output "foo : nat".

we can also combine outputs:

Capture Output Check foo.
Capture Output Check bar.
Assert Output "
foo : nat
bar : bool
".

To prevent forgetting outputs, if there is a Capture Output but no Assert Output before the end of the file compilation fails (like with leaving open proofs). We could also fail if there is no Assert Output before a End (not sure if desired).

It would be nice to be able to include a filter, a unix command that treats the both output string and the expected text and removes irrelevant information

I don't think we want to be able to call unix commands from Rocq code (security issues, not portable...). We should probably normalize whitespace by default (maybe with an option to disable normalization) (eg Printing Width depends on user settings so would make things non reproducible).

We could also have a way to call Rocq code on the output string (ie expose it as a primitive string) somehow. eg Process Output msg Using code. would bind msg to the current output, evaluate code and set the result as the new output. code could be a regular rocq term eg PrimString.sub msg 0 4 to get the first 4 chars, or it could use tactics in terms eg ltac2:(do_stuff msg).

[ybertot]

I like the Capture/Assert pair. I understand the reluctance to depend on platform dependent filters.

[radrow]

That's a great idea, I really like the ability to combine two outputs. To that I would also add

• Drop Output. — if you change your mind (useful in coqtop).
• Show Output. — to print the contents of the output (Print would make clashes)

Also a fun trick: if you want to assert output without flushing it, you can do Fail Fail Assert Output.

This could be later extended to more advanced output caching with assignable buffers that can be managed more precisely (dumping to files, combining, whatever).

[TheoWinterhalter]

Note that Fail Fail can be replaced by Succeed already.