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
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
@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).
thanks! I have
Set Default Proof Using "Type"., so that workaround won't help...
nice issue number
Last updated: Feb 04 2023 at 02:03 UTC