Open JasonGross opened 8 months ago
Surely
destruct q_nice_strong with (b:=b) (k:=k) (m:=mu) (offset:=1) (a:=x) (n:=M) as [cond Hcond]; eauto using Z.lt_gt with zarith.
was not taking 95 seconds when we first wrote that line, and something is going wrong?
Originally posted by @JasonGross in https://github.com/coq/coq/issues/18818#issuecomment-2007652341
https://github.com/mit-plv/fiat-crypto/blob/a8816f08f6955709e27a39d96ac1279ff1d2ee0c/src/Arithmetic/BarrettReduction.v#L103-L104
Is it just the bench machine that is slow, I see 0m15.19s | 520360 ko | Arithmetic/BarrettReduction.vo in 9584e6ce614f9b94eb10d69a3333a31541b2661c
CI dev says 1m38.92s | 774816 ko | Arithmetic/BarrettReduction.vo but I can't find logs that stretch back far enough to see if it was always that way.
Surely
was not taking 95 seconds when we first wrote that line, and something is going wrong?
Originally posted by @JasonGross in https://github.com/coq/coq/issues/18818#issuecomment-2007652341
https://github.com/mit-plv/fiat-crypto/blob/a8816f08f6955709e27a39d96ac1279ff1d2ee0c/src/Arithmetic/BarrettReduction.v#L103-L104
Is it just the bench machine that is slow, I see 0m15.19s | 520360 ko | Arithmetic/BarrettReduction.vo in 9584e6ce614f9b94eb10d69a3333a31541b2661c
CI dev says 1m38.92s | 774816 ko | Arithmetic/BarrettReduction.vo
but I can't find logs that stretch back far enough to see if it was always that way.