From f89f0eb4717b64f10bdd0a0edc9e93b949bcb33d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 12 Feb 2021 18:11:52 +0100
Subject: Normalize evars during bytecode compilation (fix #13841).

Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.

This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.
---
 kernel/vmbytegen.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'kernel/vmbytegen.ml')

diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 20de4bc81b..7d3b3469b0 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -840,21 +840,21 @@ let dump_bytecodes init code fvs =
      prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
      fnl ())
 
-let compile ~fail_on_error ?universes:(universes=0) env c =
+let compile ~fail_on_error ?universes:(universes=0) env sigma c =
   init_fun_code ();
   Label.reset_label_counter ();
   let cont = [Kstop] in
   try
     let cenv, init_code =
       if Int.equal universes 0 then
-        let lam = lambda_of_constr ~optimize:true env c in
+        let lam = lambda_of_constr ~optimize:true env sigma c in
         let cenv = empty_comp_env () in
         cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont
       else
         (* We are going to generate a lambda, but merge the universe closure
          * with the function closure if it exists.
          *)
-        let lam = lambda_of_constr ~optimize:true env c in
+        let lam = lambda_of_constr ~optimize:true env sigma c in
         let params, body = decompose_Llam lam in
         let arity = Array.length params in
         let cenv = empty_comp_env () in
@@ -896,7 +896,8 @@ let compile_constant_body ~fail_on_error env univs = function
             let con= Constant.make1 (Constant.canonical kn') in
               Some (BCalias (get_alias env con))
         | _ ->
-            let res = compile ~fail_on_error ~universes:instance_size env body in
+            let sigma _ = assert false in
+            let res = compile ~fail_on_error ~universes:instance_size env sigma body in
               Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
-- 
cgit v1.2.3