Enrico Tassi (Oct 12 2021 at 11:59): Enrico Tassi (Oct 12 2021 at 11:59):One more comment on #15008. IMO we should make vernac/ agnostic over the storage mechanism for (delayed and not) proofs. In this way futures can be removed/hidden inside the document manager completely. As a consequence the API to execute a vernac sentence has to take a function (or some other inversion of control) to query the store of proofs. And that function return type should be an option, in case the proof is not accessible.
It is not very different from the current code which can raise an exception, it is more explicit about it. As usual, making these things explicit is a PITA, since the change in the type is going to be quite pervasive (hello monads). In this way all the clients of the API have to fixed, and behave correctly even if the proofs are not there. Eg extraction, in .vos mode, should not fail hard but just do a no-op. In the current model it is the document manager that skips the call to extraction in order to not trigger the exception...
CC @Pierre-Marie Pédrot
Last updated: Jun 04 2023 at 19:30 UTC