Stream: jsCoq

Topic: bytecode compiler & `lia`

Shachar Itzhaky (Sep 14 2020 at 13:01):

Hi guys,

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 val_of_constr.

Pierre-Marie Pédrot (Sep 14 2020 at 13:03):

What mechanism does jsCoq rely on to turn off the VM mechanism?

Pierre-Marie Pédrot (Sep 14 2020 at 13:04):

Does it use the configure flag, or is the code modifier in a different way?

Shachar Itzhaky (Sep 14 2020 at 13:04):

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;

Shachar Itzhaky (Sep 14 2020 at 13:04):

Also Coq is configured with -native-compiler no -bytecode-compiler no.

Pierre-Marie Pédrot (Sep 14 2020 at 13:05):

This seems a bit redundant but well, you can't never be sure...

Pierre-Marie Pédrot (Sep 14 2020 at 13:06):

It's weird that even with the configure flag turned off you get the VM to run.

Pierre-Marie Pédrot (Sep 14 2020 at 13:07):

It looks like in Vconv we don't check this flag, but only the one from the environment.

Shachar Itzhaky (Sep 14 2020 at 13:07):

Yes, exactly.

Pierre-Marie Pédrot (Sep 14 2020 at 13:07):

This is the bug then.

Pierre-Marie Pédrot (Sep 14 2020 at 13:07):

It's not unheard of though, I recall that native had a similar issue.

Pierre-Marie Pédrot (Sep 14 2020 at 13:08):

Too many interfering flags and this is what happens :shrug:

Shachar Itzhaky (Sep 14 2020 at 13:08):

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.

Pierre-Marie Pédrot (Sep 14 2020 at 13:08):

Nah, I don't think that relying on Global inside a plugin initialization is safe

Pierre-Marie Pédrot (Sep 14 2020 at 13:09):

It depends exactly how it's invoked but it's likely to wreak havoc with the STM.

Pierre-Marie Pédrot (Sep 14 2020 at 13:09):

I think that the intended usage is to turn off the VM on a per-sentence basis.

Shachar Itzhaky (Sep 14 2020 at 13:11):

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.

Pierre-Marie Pédrot (Sep 14 2020 at 13:12):

Fair enough.

Pierre-Marie Pédrot (Sep 14 2020 at 13:12):

But then I don't see in the micromega code why the environment doesn't contain that flag.

Pierre-Marie Pédrot (Sep 14 2020 at 13:12):

It's calling global inside a thunk which is only going to get evaluated after the environment is set.

Shachar Itzhaky (Sep 14 2020 at 13:13):

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 let).

Pierre-Marie Pédrot (Sep 14 2020 at 13:14):

Yeah, but this is a function.

Pierre-Marie Pédrot (Sep 14 2020 at 13:14):

So by the time its body is evaluated, the environment should be the global one.

Pierre-Marie Pédrot (Sep 14 2020 at 13:15):

You can try to debug this via printf debugging and repeatedly checking the moment the global environment has its value set / accessed.

Shachar Itzhaky (Sep 14 2020 at 13:20):

Ok I'll try that

Shachar Itzhaky (Sep 14 2020 at 15:08):

Turns out I accidentally switched Global.set_VM and Lib.init, so 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)"
.

Shachar Itzhaky (Sep 14 2020 at 15:09):

...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?

Pierre-Marie Pédrot (Sep 14 2020 at 15:09):

It could be that normally the VM is bypassing an opacity flag

Shachar Itzhaky (Sep 14 2020 at 15:10):

ah hmm.

Pierre-Marie Pédrot (Sep 14 2020 at 15:10):

... but the Vconv code seems like it's passing a full transparent state to the conversion function

Shachar Itzhaky (Sep 14 2020 at 15:12):

now my 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.

Pierre-Marie Pédrot (Sep 14 2020 at 15:12):

This is indeed suspicious.

Shachar Itzhaky (Sep 14 2020 at 15:48):

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