Stream: Coq users

Topic: "not found in table: metacoq.bool.false"


view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 10:11):

Hi! I joined a new project, and sometimes I get the error in the subject:

not found in table: metacoq.bool.false

but only when using async proofs in the IDE, and not in normal compilation (or even in make vos). Some code from MetaCoq is transitively required:

Require Import MetaCoq.Template.All.
Require Import MetaCoq.Template.TemplateMonad.Extractable.

Does that sound like a potential MetaCoq bug?

view this post on Zulip Yannick Forster (Jul 14 2020 at 15:53):

Hi Paolo, that could well be a MetaCoq bug. Do you use commands like MetaCoq Run in the script?

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 16:07):

Not MetaCoq Run — the offending files load files that use Run TemplateProgram and template-coq — BTW, we only depend on coq-metacoq-template.

view this post on Zulip Yannick Forster (Jul 14 2020 at 16:16):

Run TemplateProgram is the old syntax for what is now MetaCoq Run :) You have installed MetaCoq from opam I suppose?

view this post on Zulip Yannick Forster (Jul 14 2020 at 16:20):

It's very well possible that the problem goes away on the current version of MetaCoq. We unfortunately do not have a more recent opam release. If it's not bugging you too much I'd suggest to wait for the new release (which hopefully will also support OCaml 4.10). If it's bugging you a lot I can try to help you port to the current github version

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 16:28):

It's not bugging me overly much

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 16:29):

But down the line I'd like to experiment with async proofs, make vos and all that

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 16:30):

FWIW, I just saw this on a lemma whose statement is entirely MetaCoq free (arithmetic on Z with functions from the stdlib)

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 16:30):

How many of you use async IDEs (CoqIde/VsCoq/.../ anything but Emacs)

view this post on Zulip Théo Winterhalter (Jul 14 2020 at 17:34):

Paolo Giarrusso said:

How many of you use async IDEs (CoqIde/VsCoq/.../ anything but Emacs)

You mean on the MetaCoq project? I know Matthieu and myself use VSCoq.


Last updated: Mar 28 2024 at 13:01 UTC