Test perf-Sanity on CI

.github/workflows/coq.yml

@@ -53,6 +53,8 @@ jobs:
         submodules: recursive
     - name: all
       run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all
+    - name: perf-Sanity
+      run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 perf-Sanity
     - name: display timing info
       run: cat time-of-build-pretty.log
     - name: display per-line timing info

.github/workflows/docker-coq.yml

@@ -27,3 +27,4 @@ jobs:
           echo '::endgroup::'
           echo '::remove-matcher owner=coq-problem-matcher::'
           etc/ci/github-actions-make.sh --warnings -j2 all
+          etc/ci/github-actions-make.sh --warnings -j2 perf-Sanity

src/Rewriter/Language/Reify.v

@@ -543,12 +543,13 @@ Module Compilers.
       let reify_ident_preprocess := reify_ident_preprocess ctx_tys in
       let handle_eliminator (motive : constr) (rect_arrow_nodep : constr option) (rect_nodep : constr option) (rect : constr) (mid_args : constr list) (cases_to_thunk : constr list)
         := let mkApp_thunked_cases f pre_args
-             := Control.with_holes
-                  (fun () => mkApp f (List.append pre_args (List.append mid_args (List.map (fun arg => '(fun _ => $arg)) cases_to_thunk))))
-                  (fun fv => match Constr.Unsafe.check fv with
-                             | Val fv => fv
-                             | Err err => Control.throw err
-                             end) in
+             := let pr_cl := fun () => Message.of_list Message.of_constr in
+                Reify.debug_wrap
+                  "reify_ident_preprocess.mkApp_thunked_cases" (fun (f, pre_args, mid_args, cases_to_thunk) => fprintf "%t (%a) (%a) (%a)" f pr_cl pre_args pr_cl mid_args pr_cl cases_to_thunk) (f, pre_args, mid_args, cases_to_thunk)
+                  Reify.should_debug_enter_reify_preprocess Reify.should_debug_enter_reify_preprocess (Some Message.of_constr)
+                  (fun ()
+                   => let mkThunk v := Constr.Unsafe.substnl [v] 0 (mkLambda (Constr.Binder.make None 'unit) (mkRel 2)) in
+                      mkApp f (List.append pre_args (List.append mid_args (List.map mkThunk cases_to_thunk)))) in
            let opt_recr (thunked : bool) orect args :=
              match orect with
              | Some rect => (reify_ident_preprocess,

src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v

@@ -200,9 +200,9 @@ Definition max_input_of_kind (k : kind_of_rewrite) : option (Z * Z)
      | kind_red native
        => Some (110, 110) (* works with 130, 130, but we fallback to vm when native is not available *) (* stack overflows on (20880, 1) *)
      | kind_red cbv
-       => Some (140, 140) (* stack overflows on (25760, 1) *)
+       => Some (110, 110) (* stack overflows on (25760, 1) *)
      | kind_red lazy
-       => Some (140, 140) (* stack overflows on (22052, 1) *)
+       => Some (110, 110) (* stack overflows on (22052, 1) *)
      | kind_red cbn
        => None
      | kind_red simpl