Stream: Coq devs & plugin devs

Topic: Trying to migrate to Coq 8.18.0 -- anomaly error


view this post on Zulip Audrey Seo (Apr 12 2024 at 05:03):

Hi! I'm writing a Coq plugin. Originally, it was on Coq 8.16.1 I was able to upgrade it to 8.17.1 seemingly without a hitch. Now I'm updating it to 8.18.0, and after fixing all of the deprecation warnings, I get the following error when I try to load my plugin.

File "./plugin/theories/Loader.v", line 3, characters 0-40:
Error:
Dynlink error: execution of module initializers in the shared library failed: "Anomaly: The global environment cannot be accessed during the syntactic interpretation
phase."

This is on the

Declare ML Module "my_module.plugin".

line in Loader.v. Does anyone have any insights as to where this error could be coming from? I have a feeling that it might be coming from the following call to Global.env, but I am not sure how to fix this. (We want to maintain a table of names to treat as not-unfoldable to speed up some of our algorithms. Originally the QGlobRef.equal call was for Names.GlobRef.equal, but the latter was deprecated.)

(* Cache for opaques *)
type key_typ = Names.GlobRef.t
module OpaquesCache =
  Hashtbl.Make
    (struct
      type t = key_typ
      let equal =
        (* this didn't use to have a reference to the environment, but Names.GlobRef.equal was deprecated, in favor of QGlobRef.equal *)
        (fun t t' -> QGlobRef.equal (Global.env ()) t t')
      let hash =
        (fun t ->
          let open Globnames in
          (ExtRefOrdered.hash (TrueGlobal t)))
    end)

I might try to make our own table (as in the Goptions.MakeRefTable), but I'm unsure if this is the intended use-case for MakeRefTable. (Or if doing so will fix this issue).
Thank you in advance!

view this post on Zulip Gaëtan Gilbert (Apr 12 2024 at 07:48):

If you do Set Debug "backtrace". before the Declare ML Module you may get more information

view this post on Zulip Gaëtan Gilbert (Apr 12 2024 at 07:50):

the Goptions table declares a table that the user may put names into, like Printing Let https://coq.inria.fr/doc/master/refman/language/extensions/match.html#coq:table.Printing-Let

view this post on Zulip Gaëtan Gilbert (Apr 12 2024 at 07:50):

I don't think that table is the issue unless you use it at plugin linking time

view this post on Zulip Matthieu Sozeau (Apr 12 2024 at 10:58):

I had the same error when porting Goptions code in MetaCoq, you can maybe get a hint by looking at the commits in the main branch of MetaCoq. Gaëtan knows about that issue too :)

view this post on Zulip Audrey Seo (Apr 12 2024 at 21:03):

Thanks @Gaëtan Gilbert and @Matthieu Sozeau! I'll look through the metacoq commits and see what I can find.

Gaëtan Gilbert said:

I don't think that table is the issue unless you use it at plugin linking time

It turned out to indeed not be this table, though a different table is giving me issues. We pre-populate hash tables of constructors for Coq inductive types (for ease of use, so we can just grab the desired constructor by using `Hashtbl.find coq_bool_constructors_tbl "false"), which must be happening at plugin linking time because the second line of code is what is producing the error.

let coq_bool = get_inductive "Coq.Init.Datatypes.bool" ~index:0
let coq_bool_constructors_tbl =
  get_constructors_hashtbl ~env:(Global.env ()) ~trm:(EConstr.UnsafeMonomorphic.mkInd coq_bool) ~sigma:Evd.empty

Is there any way that I can delay the call to Global.env () until after linking time?

view this post on Zulip Rodolphe Lepigre (Apr 12 2024 at 21:37):

Can't you just thunk that expression with:

let coq_bool_constructors_tbl =
  lazy (get_constructors_hashtbl ...)

and corresponding call to Lazy.force on use sites?

view this post on Zulip Gaëtan Gilbert (Apr 12 2024 at 22:42):

to be more correct you would also thunk the coq_bool definition (assuming get_inductive accesses the nametab or other global state)
since you don't I imagine your code is incompatible with async proofs getting issues like https://github.com/MetaCoq/metacoq/issues/777
using lazy is not fully correct if the user backtracks and changes one of the globals you statically lookup, but for stuff from Init this may be considered unrealistic


Last updated: Oct 13 2024 at 01:02 UTC