Add profiling for cbn, drop support for Coq < 8.17 (#141)

* Add profiling for cbn

Seems to be responsible for 23.0% of the cost of rewrite rules in
mit-plv/fiat-crypto#1778, with a single call
taking 168.429s.

* Drop Coq < 8.17

The Ltac2 support is not good enough.

Author: JasonGross

.github/workflows/coq-docker.yml

@@ -17,8 +17,8 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ '8.16' ]
-        extra-gh-reportify: [ '' ]
+        #coq-version: [ '8.16' ]
+        #extra-gh-reportify: [ '' ]
         include:
         - coq-version: 'dev'
           extra-gh-reportify: '--warnings'

.github/workflows/coq.yml

@@ -20,16 +20,9 @@ jobs:
         env:
          - { COQ_VERSION: "8.18.0", COQ_PACKAGE: "coq-8.18.0 libcoq-8.18.0-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" }
          - { COQ_VERSION: "8.17.1", COQ_PACKAGE: "coq-8.17.1 libcoq-8.17.1-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" }
-         # Ltac2 is broken in the 8.16 package
-         #- { COQ_VERSION: "8.16.1", COQ_PACKAGE: "coq-8.16.1 libcoq-8.16.1-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" }
-         - { COQ_VERSION: "8.15.2", COQ_PACKAGE: "coq-8.15.2 libcoq-8.15.2-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08" }
-        os: [ ubuntu-latest ]
-        include:
-        - env: { COQ_VERSION: "v8.15" , COQ_PACKAGE: "coq libcoq-ocaml-dev"              , SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/coq-8.15-daily" }
-          os: ubuntu-20.04
 
     env: ${{ matrix.env }}
-    runs-on: ${{ matrix.os }}
+    runs-on: ubuntu-latest
 
     concurrency:
       group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }}

README.md

@@ -8,7 +8,7 @@ Publications
 
 Building
 -----
-This repository requires Coq 8.15 or later, and requires that the version of OCaml used to build Coq be installed and accessible on the system.
+This repository requires Coq 8.17 or later, and requires that the version of OCaml used to build Coq be installed and accessible on the system.
 
 Git submodules are used for some dependencies. If you did not clone with `--recursive`, run
 

src/Rewriter/Language/PreCommon.v

@@ -21,6 +21,7 @@ Module Export Pre.
   (** Change this with [Ltac2 Set reify_debug_level ::= 1.] to get
       more debugging. *)
   Ltac2 mutable reify_debug_level : int := 0.
+  Ltac2 mutable reify_profile_cbn : bool := false.
 
   Module ScrapedData.
     Local Set Primitive Projections.

src/Rewriter/Language/Reify.v

@@ -96,6 +96,7 @@ Module Compilers.
 
   Module Reify.
     Ltac2 Notation debug_level := Pre.reify_debug_level.
+    Ltac2 Notation should_profile_cbn := Pre.reify_profile_cbn.
 
     Ltac2 mutable should_debug_enter_reify () := Int.le 3 debug_level.
     Ltac2 mutable should_debug_enter_reify_preprocess () := Int.le 3 debug_level.
@@ -125,6 +126,19 @@ Module Compilers.
       then tac ()
       else default.
 
+    Ltac2 debug_profile_if (descr : string) (pr_a : 'a -> message) (pr_b : 'b -> message) (cond : unit -> bool) (tac : 'a -> 'b) (val : 'a) :=
+      if cond ()
+      then (let c' := Control.time (Some descr) (fun () => tac val) in
+            printf "Info: %s from %a to %a" descr (fun () => pr_a) val (fun () => pr_b) c';
+            c')
+      else tac val.
+
+    Ltac2 debug_profile_eval_cbn descr s c :=
+      let descr := String.concat " " ["eval cbn"; descr] in
+      debug_profile_if
+        descr Message.of_constr Message.of_constr
+        (fun () => should_profile_cbn) (Std.eval_cbn s) c.
+
     Ltac2 debug_typing_failure (funname : string) (x : constr) (err : exn)
       := debug_if should_debug_typing_failure (fun () => printf "Warning: %s: failure to typecheck %t: %a" funname x (fun () => Message.of_exn) err) ().
     Ltac2 debug_typing_failure_assume_well_typed (funname : string) (v : constr) (term : constr) (ctx_tys : binder list) (ty : constr)
@@ -285,6 +299,11 @@ Module Compilers.
            e.
     Ltac2 debug_Constr_check (funname : string) (descr : constr -> constr -> exn -> message) (var : constr) (cache : (unit -> binder) list) (var_ty_ctx : constr list) (e : constr)
       := Constr.debug_assert_hole_free funname (debug_Constr_check_allow_holes funname descr var cache var_ty_ctx e).
+
+    Module Export Notations.
+      Ltac2 Notation "debug" "(" descr(tactic) ")" "profile" "eval" "cbn" s(strategy) "in" c(tactic(6)) :=
+        debug_profile_eval_cbn descr s c.
+    End Notations.
   End Reify.
 
   Module type.

src/Rewriter/Rewriter/Reify.v

@@ -49,6 +49,7 @@ Module Compilers.
   Export IdentifiersBasicGenerate.Compilers.
   Import invert_expr.
   Export Rewriter.Compilers.
+  Import Language.Reify.Compilers.Reify.Notations.
 
   Module RewriteRules.
     Export Rewriter.Compilers.RewriteRules.
@@ -317,7 +318,7 @@ Module Compilers.
           (fun ()
            => let s := strategy:([pattern.type.relax pattern.type.subst_default pattern.type.subst_default_relax pattern.type.unsubst_default_relax]) in
               let pat := Std.eval_cbv s pat in
-              let pat := Std.eval_cbn s pat in
+              let pat := Reify.debug_profile_eval_cbn "preadjust_pattern_type_variables" s pat in
               pat).
 
       Ltac2 rec adjust_pattern_type_variables' (pat : constr) : constr :=
@@ -693,10 +694,10 @@ Module Compilers.
           Reify.should_debug_fine_grained Reify.should_debug_fine_grained (Some Message.of_constr)
           (fun ()
            => let term := lazy_match! (eval pattern 'andb, '(andb true) in term) with
-                          | ?f _ _ => (eval cbn [andb] in constr:($f (fun x y => andb y x) (fun b => b)))
+                          | ?f _ _ => (debug ("remove_andb_true:1") profile eval cbn [andb] in constr:($f (fun x y => andb y x) (fun b => b)))
                           end in
               let term := lazy_match! (eval pattern 'andb, '(andb true) in term) with
-                          | ?f _ _ => (eval cbn [andb] in constr:($f (fun x y => andb y x) (fun b => b)))
+                          | ?f _ _ => (debug ("remove_andb_true:2") profile eval cbn [andb] in constr:($f (fun x y => andb y x) (fun b => b)))
                           end in
               term).
       Ltac2 rec adjust_if_negb (term : constr) : constr :=
@@ -781,7 +782,7 @@ Module Compilers.
           Reify.should_debug_fine_grained Reify.should_debug_fine_grained (Some Message.of_constr)
           (fun ()
            => let base_interp_beq_head := head_reference base_interp_beq in
-              let term := (eval cbn [Prod.prod_beq] in term) in
+              let term := (debug ("clean_beq:Prod.prod_beq") profile eval cbn [Prod.prod_beq] in term) in
               let term := (eval cbv [ident.literal] in term) in
               let term := deep_substitute_beq base_interp_beq avoid only_eliminate_in_ctx term in
               let term := (eval cbv [base.interp_beq $base_interp_beq_head] in term) in
@@ -884,7 +885,7 @@ Module Compilers.
                                    let pident_type_of_list_arg_types_beq := head_reference pident_type_of_list_arg_types_beq in
                                    let pident_arg_types_of_typed_ident := head_reference pident_arg_types_of_typed_ident in
                                    (eval cbv [expr_to_pattern_and_replacement_unfolded_split $pident_arg_types $pident_of_typed_ident $pident_type_of_list_arg_types_beq $pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in
-                        let res := (eval cbn [fst snd andb pattern.base.relax pattern.base.subst_default pattern.base.subst_default_relax] in res) in
+                        let res := (debug ("reify_to_pattern_and_replacement_in_context:1") profile eval cbn [fst snd andb pattern.base.relax pattern.base.subst_default pattern.base.subst_default_relax] in res) in
                         let res := change_pattern_base_subst_default_relax res in
                         let (p, res) := lazy_match! res with
                                         | existT _ ?p ?res => (p, res)
@@ -913,7 +914,7 @@ Module Compilers.
                                                      res)))) in
                         let res := debug_Constr_check res in
                         let res := (eval cbv [UnderLets.map UnderLets.flat_map reify_expr_beta_iota reflect_expr_beta_iota reify_to_UnderLets] in res) in
-                        let res := (eval cbn [reify reflect UnderLets.of_expr UnderLets.to_expr UnderLets.splice value' Base_value invert_Literal invert_ident_Literal splice_under_lets_with_value] in res) in
+                        let res := (debug ("reify_to_pattern_and_replacement_in_context:2") profile eval cbn [reify reflect UnderLets.of_expr UnderLets.to_expr UnderLets.splice value' Base_value invert_Literal invert_ident_Literal splice_under_lets_with_value] in res) in
                         let res := strip_invalid_or_fail res in
                         (* cbv here not strictly needed *)
                         let res := (eval cbv [partial_lam_unif_rewrite_ruleTP_gen_unfolded]
@@ -922,7 +923,7 @@ Module Compilers.
                                                   $p
                                                   ($cpartial_lam_unif_rewrite_ruleTP_gen _ $p $res))) in
                         (* not strictly needed *)
-                        let res := (eval cbn [pattern.base.subst_default pattern.base.lookup_default PositiveMap.find type.interp base.interp $base_interp_head] in res) in
+                        let res := (debug ("reify_to_pattern_and_replacement_in_context:3") profile eval cbn [pattern.base.subst_default pattern.base.lookup_default PositiveMap.find type.interp base.interp $base_interp_head] in res) in
                         let res := (eval cbv [projT1 projT2]
                                      in constr:(existT
                                                   (@rewrite_ruleTP $base $ident $var $pident $pident_arg_types)