[wip] Incorrect experiment to clean up some code in the stm #18976
Conversation
It seems these files were never used?
ejgallego
added
kind: cleanup
coqbot-app
bot
added
the
needs: full CI
| | `Not -> Leaks | ||
|
|
||
| let () = register_proof_block_delimiter | ||
| "bullet" static_bullet dynamic_bullet |
There was a problem hiding this comment.
I think this file is here for the effects like this one.
There was a problem hiding this comment.
Indeed I don't think we test that in test-suite.
I'll move this PR to draft for now; we could gain a bit from removing the error recovery thing of the STM, which AFAICT newer worked too well (at least in SerAPI / jsCoq we had to disable it, otherwise things got really flaky)
On the other hand that's not a super gain from my own experiments.
There was a problem hiding this comment.
IIRC the advantage of having the analysis of "sub proof boxes" in Coq proper rather than the document manager is that one needs the internals of the proof engine. In particular it makes sense to recover/admit a broken proof as in { broken proof } .. { another proof } only if the type of the broken proof is ground (no evar the broken proof should be filled occur in it) and if the proof term itself is not occurring in any other goal.
Maybe the code is ugly or broken, but doing it naively in the DM by putting admit when the structure allows for it is not sound.
There was a problem hiding this comment.
We can of course say it is not the STM that lets one skip over broken sub-proofs, but the code doing the analysis really belongs to Coq's proof model.
There was a problem hiding this comment.
What's you definition of "sound" in this context?
ejgallego
added
needs: progress
ejgallego
changed the title
It seems these files were never used?