1ab4c9f8bf
The over-application doesn't occur very often in practice. The new version adds an extra "copy" step, but it avoids the quadratic blowup in code size. Xavier Leroy reports that only 5% of all calls are over-applications in his experiments. In Lean3, 6.59% of all calls performed to compile corelib are "over", and we did not implement any fancy optimization. |
||
|---|---|---|
| .. | ||
| checker | ||
| cmake | ||
| frontends/lean | ||
| init | ||
| kernel | ||
| library | ||
| shared | ||
| shell | ||
| tests | ||
| util | ||
| CMakeLists.txt | ||
| CTestConfig.cmake | ||
| CTestCustom.cmake.in | ||
| Doxyfile | ||
| githash.h.in | ||
| memcheck.supp | ||
| version.h.in | ||