Skip to main content

Questions tagged [performance]

For questions pertaining to the measurement or improvement of code and application efficiency.

Filter by
Sorted by
Tagged with
20 votes
0 answers
233 views

What is known about performance bottlenecks in proof assistants?

Background In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for ...
Jason Gross's user avatar
  • 1,537
12 votes
2 answers
203 views

Are there any proof assistants which integrate JITs?

Has there been notable research or attempts to integrate a JIT compiler into a proof assistant in order to achieve performance gains for proof verification, or general programming? Whilst it may seem ...
Julian's user avatar
  • 576
10 votes
1 answer
251 views

Performance of de Bruijn indices?

Can any of you refer me to documented results of experiments on the performance of provers using de Bruijn indices to represent references to bound variables versus mentions of names or other simple ...
Cris P's user avatar
  • 345
9 votes
2 answers
271 views

Are search heuristics the main bottleneck for automated theorem provers?

My understanding of most automated theorem provers (which is possibly an incorrect understanding!) is that they start with some premises stored as unprocessed statements, and repeatedly select one to &...
Reubend's user avatar
  • 519
7 votes
0 answers
99 views

How to improve/understand typechecking performance in Agda?

I've recently been trying to do some basic formalization of category theory in Agda. As part of this I need to prove a bunch of basic properties around products/monoidal categories. A bunch of these ...
Eric Dobson's user avatar
6 votes
2 answers
901 views

Speeding up large data structures in Lean

Consider a simple inductive data structure of binary trees, and a type of pairs of integers: ...
Andrej Bauer's user avatar
  • 9,553
3 votes
1 answer
94 views

Are there squeeze-versions of ring and abel?

In Lean, it is recommended to use squeeze_simp to generate simp only [a bunch of lemmas] for two reasons: (1) Otherwise the ...
Strichcoder's user avatar