Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

perf: simp_arith: faster denote through Lean.RArray #6068

Merged
merged 3 commits into from
Nov 14, 2024
Merged

perf: simp_arith: faster denote through Lean.RArray #6068

merged 3 commits into from
Nov 14, 2024

Commits on Nov 14, 2024

  1. perf: use RArray in simp_arith meta code (#6068 part 1) 

    This PR prepares #6068 by using the `RArray` data structure in
`simp_arith` the simp-arith meta code.

After the subsequent stage0 we can change the simp-arith theorems in
`Init`.
    @nomeata
    nomeata committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    86e3675 View commit details
    Browse the repository at this point in the history

  2. chore: update stage0

    @nomeata
    nomeata committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    d94a6dc View commit details
    Browse the repository at this point in the history

  3. perf: use RArray in simp_arith meta code (#6068 part 2) 

    This PR makes `simp_arith` use `RArray` for the context of the
reflection proofs, which scales better when there are many variables.

On our synthetic benchmark:
```
simp_arith1               instructions    -25.1% (-4892.6 σ)
```

No effect on mathlib, though, guess it’s not used much on large goals there:
http://speed.lean-fro.org/mathlib4/compare/873b982b-2038-462a-9b68-0c0fc457f90d/to/56e66691-2f1f-4947-a922-37b80680315d
    @nomeata
    nomeata committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    725d59e View commit details
    Browse the repository at this point in the history