Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
I will cut this PR into smaller pieces. The `poly.v` part might already be ready. I should redo the `matrix.v` part (almost from scratch) based on #1385.
For vector.v, I hope its generalization to semi-vector spaces will further mitigate the issue. Most `GRing.semilinear_linear` should disappear anyway thanks to #1269.
I discarded the changes to `poly.v` and `matrix.v`: they were just removal of `GRing.semilinear_linear` which has been done in #1395 and #1398 (in the right way). I hope this will...
This PR can probably be merged safely now. It would be nice to compare the performance of the `(* slow *)` lines before/after this PR using a recent version of...
I rebenched this PR with Rocq 9.1.0. To sum up, I don't see any slowdown in `vector.v` anymore. However, `mxrepresentation.v` has become slower for unclear reasons. (It's a bit concerning...
I believe that `floorP` and `truncP` should be restated using a `spec` datatype.
Hi @CohenCyril, any news on this front? @affeldt-aist If we have some time, I suggest taking a look at this issue again after merging #1469.
FTR, Cyril's feedback on locking was that we should probably switch from keyed locking to module locking (like `HB.lock`). We can still keep the key by module-locking the definitions that...
The breakage of multinomials should be fixed by math-comp/multinomials#118.
In the end, locking `fun_of_fsfun` does not seem to fix the issue in multinomials. So, I leave it unlocked here. In any case, this PR reduces some boilerplate code.