Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
It seems that `rewrite` by `linearZ`, `linearB`, `linear0`, etc. are sometimes too slow now. I will check if this is the case in the master branch (and open another cherry-pick...
Bench (b174dacb..2e8c0a63): ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------- 33m51.69s |...
I ran it on Coq 8.19.0, Coq-Elpi 2.2.0, and HB 1.7.0.
BTW, it took me a while to figure out how to do per-file and per-line performance comparisons of two branches of MathComp at the same time. Here is the solution...
New bench (https://github.com/math-comp/math-comp/compare/3ac1089f..3a85d090): ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------- 32m22.15s...
Same comparison with Coq and HB master: ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | %...
Some authors write "left semi-module" and it seems natural to me. So I proceed with `lSemiModType`.
I thought that the point of `fun_scope` is to locally increase the priority of the notations defined in `fun_scope` in a context where a function is expected, e.g., the third...
https://github.com/math-comp/math-comp/pull/1145#issuecomment-1895355450