lia does not work again (for a different reason)

[corwin-of-amber]

This code:

Require Import Lia.

Example silly_presburger_example : forall m n o p,
  m + n <= n + o /\ o + 3 = p + 3 ->
  m <= p.
Proof.
  intros. lia.
Qed.

Works fine until the Qed, but then throws:

Anomaly
"Uncaught exception Error: vm trap: 'coq_set_bytecode_field' not implemented."
Please report at http://coq.inria.fr/bugs/.

Somehow the bytecode compiler is invoked here. Not sure why.

[corwin-of-amber]

I think I traced it (or at least part of it): it looks like coq_mircromega.ml checks term in the environment Refiner.pf_env.

https://github.com/coq/coq/blob/282bf5806ca861ca7649bdd8555cba2b2130a3d7/plugins/micromega/coq_micromega.ml#L1673

Which is defined here.

https://github.com/coq/coq/blob/282bf5806ca861ca7649bdd8555cba2b2130a3d7/proofs/refiner.ml#L25

This last let is called before we Global.set_VM false, so probably this environment has enable_VM set.

[ejgallego]

Where is enable_VM set? IIRC configure should totally disable it.

Did you build that jscoq version with the right configure magic? If so, that'd be an upstream bug.

[ejgallego]

I see, indeed introduced in #196 , 5a2c448

[corwin-of-amber]

Thanks to @ppedrot for providing valuable counsel on Zulip 😄

[corwin-of-amber]

BTW he confirms that indeed there is a bug upstream: bytecode compiler should not have been invoked even with the mess I made, due to the configure flag -- but Vconv does not test for that flag.

[ejgallego]

Real problem is that we Coq doesn't provide the right API for toplevels to perform initialization, hopefully that will change soon.