Paolo Giarrusso (Jul 14 2020 at 10:11): 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?
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?
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.
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?
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
Paolo Giarrusso (Jul 14 2020 at 16:28):It's not bugging me overly much
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
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)
Paolo Giarrusso (Jul 14 2020 at 16:30):How many of you use async IDEs (CoqIde/VsCoq/.../ anything but Emacs)
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: Oct 13 2024 at 01:02 UTC