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!
If you do Set Debug "backtrace".
before the Declare ML Module you may get more information
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
I don't think that table is the issue unless you use it at plugin linking time
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 :)
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?
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?
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