Capture Output command modified

[SkySkimmer]

cf rocq-prover/rfcs#107 #20688 #20873

The captured output is not in the summary, it's in a more explicitly handled state (next to proof state and program state).
The Capture Output command modifier accumulates the output to a fresh ref, then when the command is done adds it to the state. This makes it immune to Vernacstate.System.protect and similar, can capture output from an inner Fail/Succeed, but still respects surrounding Fail/Succeed.
eg Succeed Capture Output Check 0. does not add to the state (Succeed prevents it), but Capture Output Succeed Check 0. does add to the state.

TODO:

• [] the Assert Output command to make this actually useful
• [] figure out some way to get consistent results regardless of Flags.quiet, test_mode and anything else that may differ between interactive and compile modes
• [] test with modules
• [] error if non dropped outputs remain at end of file

For Assert Output for reliable results we shouldn't depend on the current printing width setting, but we may still want to assert that line breaks are nice somehow.
I guess we could pass a printing width to Assert Output? (eg Assert Output (printing width 42) "expected".) and compare collapsing whitespace if no printing width is given? not sure

Maybe:

• [] some commands to programmatically process the output (Ltac2 Process Captured Output ltac2 code? Process Captured Output some constr?)
• [] compare up to regex in Assert Output
• [] quickfix when it fails

[SkySkimmer]

currently I don't print locations in Print Captured Output
notably they would be inconsistent in proof general (which gets some "toplevel input" location)

TODO make this more explicit in the doc

[SkySkimmer]

This is the full info we save currently (although as mentioned the location may not be useable to be consistent beween evaluation in a file and evaluation in eg proof general).
This means we could expose something to check the feedback level. Not sure if that would be useful.

[SkySkimmer]

If we redesigned locations to be relative to a command it might be possible to use them reliably but that could be a lot of work and certainly out of scope for this PR.

(This would mean in Check 0. Check 1. the "1" is char 7 in the second command, with commands having unique ids (that would be ignored by output checks since I don't think they can be made consistent across interfaces or even interactive backtracking in a given session). Then the UI would relocate based on the command id, so "7 chars after command deadbeef" becomes "char whatever in open buffer for foo.v" or some such thing)