Stream: MetaCoq

Topic: Async fails to load MetaCoq


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Oct 25 2022 at 14:32):

thanks! I have Set Default Proof Using "Type"., so that workaround won't help...

view this post on Zulip Kenji Maillard (Oct 25 2022 at 14:33):

Now reported.

view this post on Zulip Gaëtan Gilbert (Oct 25 2022 at 17:42):

nice issue number


Last updated: Mar 29 2024 at 09:02 UTC