Paolo Giarrusso (Oct 25 2022 at 14:14): Paolo Giarrusso (Oct 25 2022 at 14:14):with Coq 8.16, async proofs fail after Require MetaCoq.Template.Loader. with
Dynlink error: execution of module initializers in the shared library failed: Coq Error: not found in table: metacoq.ast.level.lsprop
Findlib paths: <lots of noise>
I'm interested both in a fix, and in a way to suppress the DoS attack on the error view
Paolo Giarrusso (Oct 25 2022 at 14:15):I recall I've also seen async proofs fail on metacoq fail with sth like not found in table: before — not in 8.15, but maybe in 8.13? But those errors were much shorter and easier to ignore
Kenji Maillard (Oct 25 2022 at 14:23):@Gaëtan Gilbert debugged that for me a few weeks ago but I forgot to report it yet. The bug is coming from a thunk that's forced at toplevel in metacoq's reification plugin. In sync mode, the code is evaluated in an order that evade the bug. For now the only fix I know is to prevent async mode either globally or for Qeded proofs by putting them inside a section with a non-empty but trivial context (for instance).
Paolo Giarrusso (Oct 25 2022 at 14:32):thanks! I have Set Default Proof Using "Type"., so that workaround won't help...
Kenji Maillard (Oct 25 2022 at 14:33):Now reported.
Gaëtan Gilbert (Oct 25 2022 at 17:42):nice issue number
Last updated: May 31 2023 at 09:01 UTC