Stream: jsCoq

Topic: bytecode compiler & `lia`


view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 13:03):

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

view this post on Zulip 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?

view this post on Zulip 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;

view this post on Zulip Shachar Itzhaky (Sep 14 2020 at 13:04):

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

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 13:05):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Sep 14 2020 at 13:07):

Yes, exactly.

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 13:07):

This is the bug then.

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 13:07):

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

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 13:08):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 13:12):

Fair enough.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 13:14):

Yeah, but this is a function.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Sep 14 2020 at 13:20):

Ok I'll try that

view this post on Zulip 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)"
.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 15:09):

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

view this post on Zulip Shachar Itzhaky (Sep 14 2020 at 15:10):

ah hmm.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 15:12):

This is indeed suspicious.

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC