Jason Gross

Profiling data ``` Reifying... Compiling decision tree... Splitting rewrite rules... Assembling rewrite_head... Reducing rewrite_head... Tactic call ran for 4.006 secs (3.997u,0.003s) (success) Tactic call ran for 225.417 secs (224.772u,0.249s) (success)...

profile of just the new rewrite rules ``` total time: 965.694s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─make_rewriter ------------------------- 0.0% 100.0% 1 965.694s ─make_rewriter_via --------------------- 0.0% 100.0% 1 965.693s ─AllTactics.Compilers.RewriteRules.Build...

With https://github.com/mit-plv/rewriter/pull/142, this commit now only makes NBE 2x slower (5m30.19s vs 2m31.42s) instead of 4x slower (9m38.79s vs 2m40.05s). This is a bit better, but probably still not good...

Of the time spent in the new rewrite rule reification, 82.7% is spent in [`replace_type_try_transport`](https://github.com/mit-plv/rewriter/blob/03889802d6ddb8dcaeb922206f07c3836d0a7b49/src/Rewriter/Rewriter/Reify.v#L597-L636) (236.006s max for a single call), which is basically "`match context[@type.try_transport ?base_type ?try_make_transport_base_type_cps ?p ?t...

For future archeologists: I'm a bit concerned that I'm seeing ``` OCAMLOPT src/ExtractionOCaml/bedrock2_dettman_multiplication.ml -o src/ExtractionOCaml/bedrock2_dettman_multiplication Warning: Stack size (8192) may be too small. Warning: To avoid stack overflows in OCaml...

There's some info [here](https://discuss.ocaml.org/t/cross-compiling-ocaml-with-github-actions/9154) on cross-compiling

GitHub actions now [provides](https://github.com/actions/runner-images#available-images) both arm64 (macos-latest, macos-14, macos-latest-xlarge or macos-14-xlarge; or macos-13-xlarge), and x86_64 (macos-latest-large or macos-14-large; macos-13 or macos-13-large; macos-12 or macos-12-large), so this should be pretty easy.

Ooh, thanks for the explanations! > My hesitance to adding this retry behavior to more layers is we quickly end up in exponential territory. For example, adding another 3-retry t...

> The benchmark baseline rules are doing ~0 work, so the slowdown here would be less visible in any real project. I encountered this when attempting to test random functions...

As came up on [Zulip just now](https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Changed.20behavior.20of.20reduction.20tactics.2E/near/234995819), I think that a reasonable way to implement this would be to augment all of the reduction strategies (`match`, `fix`, `delta`, `beta`, `iota`,...