Is anyone here familiar with the inner workings of Coq? I am trying to debug an issue where the bytecode compiler is invoked even though it seemingly shouldn't. In jsCoq, both native and bytecode compilers are disabled (since they are written in C), so this situation leads to a fatal error.
This is the issue: https://github.com/jscoq/jscoq/issues/201
I can confirm that
vm_conv_gen is called, which in turn invokes
What mechanism does jsCoq rely on to turn off the VM mechanism?
Does it use the configure flag, or is the code modifier in a different way?
The initialization looks like this:
Global.set_engagement Declarations.PredicativeSet; Global.set_VM false; Global.set_native_compiler false; Flags.set_native_compiler false; CWarnings.set_flags default_warning_flags;
Also Coq is configured with
-native-compiler no -bytecode-compiler no.
This seems a bit redundant but well, you can't never be sure...
It's weird that even with the configure flag turned off you get the VM to run.
It looks like in Vconv we don't check this flag, but only the one from the environment.
This is the bug then.
It's not unheard of though, I recall that native had a similar issue.
Too many interfering flags and this is what happens :shrug:
Pierre-Marie Pédrot said:
This is the bug then.
There are two bugs then :) because the global environment flag should have been in effect as well.
Nah, I don't think that relying on Global inside a plugin initialization is safe
It depends exactly how it's invoked but it's likely to wreak havoc with the STM.
I think that the intended usage is to turn off the VM on a per-sentence basis.
Ok, although to clarify, the initialization code does not happen inside a plugin. jsCoq has its own toplevel, which sets these flags before initializing the STM.
But then I don't see in the micromega code why the environment doesn't contain that flag.
It's calling global inside a thunk which is only going to get evaluated after the environment is set.
I still think that the "rogue" environment in
proofs/refiner.ml has the flag set; because that environment is created before jsCoq's initialization code (it's a globally-scoped
Yeah, but this is a function.
So by the time its body is evaluated, the environment should be the global one.
You can try to debug this via printf debugging and repeatedly checking the moment the global environment has its value set / accessed.
Ok I'll try that
Turns out I accidentally switched
Lib.init was called last and negated all the global env settings :face_palm:
However, when I switch it back,
lia just fails with a type error!
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints: In environment: m, n, o, p : nat H : m + n <= n + o /\ o + 3 = p + 3 ?s : "RelationClasses.subrelation iff (Basics.flip Basics.impl)" .
...and the weirdest thing is, I commented out
if ... enable_VM in
vconv.ml -- so this flag should not even have any effect anymore... what's happening?
It could be that normally the VM is bypassing an opacity flag
... but the Vconv code seems like it's passing a full transparent state to the conversion function
vconv.v has this code:
let vm_conv_gen cv_pb env univs t1 t2 = (* if not (typing_flags env).Declarations.enable_VM then *) Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) TransparentState.full env univs t1 t2 (*else try let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) TransparentState.full env univs t1 t2 *)
And still it works without
set_VM false and fails with it! This seems to be the only place
enable_VM is even tested... something really weird is going on. I think I have to make a clean build without any patches.
This is indeed suspicious.
Ok, whew, now it works. I think I had a leftover
failwith that I added for debugging somewhere.
Last updated: May 31 2023 at 02:31 UTC