From 26db829d932c69e4cab90f0a0e5e51dd71a8395a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 19 Nov 2022 14:20:03 -0500 Subject: [PATCH 1/6] Test perf-SuperFast on CI To prevent things like https://github.com/coq/coq/pull/16853 --- .github/workflows/coq.yml | 2 ++ .github/workflows/docker-coq.yml | 1 + 2 files changed, 3 insertions(+) diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 237caa636..5156d3c90 100644 --- a/.github/workflows/coq.yml +++ b/.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-SuperFast + run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 perf-SuperFast - name: display timing info run: cat time-of-build-pretty.log - name: display per-line timing info diff --git a/.github/workflows/docker-coq.yml b/.github/workflows/docker-coq.yml index 0f99cd634..766dab9d9 100644 --- a/.github/workflows/docker-coq.yml +++ b/.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-SuperFast From 3ad6fc53678cc88e179145a80cba0e5d88beb066 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 19 Nov 2022 16:29:20 -0500 Subject: [PATCH 2/6] Fix de Bruijn index bug in preprocess --- src/Rewriter/Language/Reify.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Rewriter/Language/Reify.v b/src/Rewriter/Language/Reify.v index 242deaa4d..7b8d252fe 100644 --- a/src/Rewriter/Language/Reify.v +++ b/src/Rewriter/Language/Reify.v @@ -544,7 +544,7 @@ Module Compilers. 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 () => mkApp f (List.append pre_args (List.append mid_args (List.map (fun arg => '(match $arg with v => fun _ => v end)) cases_to_thunk)))) (fun fv => match Constr.Unsafe.check fv with | Val fv => fv | Err err => Control.throw err From 214b0bb5c450baea06492067a52014747b8a52bd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 19 Nov 2022 19:00:52 -0500 Subject: [PATCH 3/6] Fix thunking --- src/Rewriter/Language/Reify.v | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Rewriter/Language/Reify.v b/src/Rewriter/Language/Reify.v index 7b8d252fe..01dfc0e42 100644 --- a/src/Rewriter/Language/Reify.v +++ b/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 => '(match $arg with v => fun _ => v end)) 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, From 58ee8407e0e1fb2842f84311a2790bc076715c81 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 19 Nov 2022 19:10:58 -0500 Subject: [PATCH 4/6] Make stack overflow less likely --- src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v b/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v index ee49bc4cb..b94c517d4 100644 --- a/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v +++ b/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 From 84df3fa139eea5064ea75378d38079b75516ab42 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 19 Nov 2022 19:11:28 -0500 Subject: [PATCH 5/6] Only test perf-Sanity, not perf-SuperFast --- .github/workflows/coq.yml | 2 +- .github/workflows/docker-coq.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 5156d3c90..96713b4cf 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -54,7 +54,7 @@ jobs: - name: all run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all - name: perf-SuperFast - run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 perf-SuperFast + 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 diff --git a/.github/workflows/docker-coq.yml b/.github/workflows/docker-coq.yml index 766dab9d9..9f06559f5 100644 --- a/.github/workflows/docker-coq.yml +++ b/.github/workflows/docker-coq.yml @@ -27,4 +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-SuperFast + etc/ci/github-actions-make.sh --warnings -j2 perf-Sanity From ddb0dc059c5833ee20ec897b5f428b34cf47ffa1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 20 Nov 2022 07:28:49 -0500 Subject: [PATCH 6/6] Fix step naming on CI --- .github/workflows/coq.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 96713b4cf..088ac55e1 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -53,7 +53,7 @@ jobs: submodules: recursive - name: all run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all - - name: perf-SuperFast + - 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