coqbot

Comment author: @ppedrot It looks like the linear cost comes from the protect_tac function in Newring, but I do not really understand what is going on. Some fancy interaction is...

Comment author: @ppedrot FYI, setting primitive projections also restore linear time computation...

Comment author: @mattam82 It's hard to see why, because the type and all ring operations provided should be protected during computations... but this must not always be the case if...

Comment author: @mattam82 I have doubts about the protected arguments of PEeval and FEeval and PCond (defined in newring.ml) which should rather be: pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot); (* FEeval: evaluate...

Comment author: @mattam82 It could just be a conversion test using the "wrong" strategy and unfolding OpaqueF when it's not Qed.d or being much faster converting P2.q Show2.prm with itself...

Comment author: @ppedrot Created attachment 753 Dump of the implicit argument > Attached file: [dump.tar.gz](https://coq.inria.fr/bugfiles/attachment.cgi?id=753) (application/gzip, 207978 bytes) > Description: Dump of the implicit argument

Comment author: @ppedrot I've just discovered that the implicit argument of ZToField (a Z) is really HUGE. When printed normally, this is: let (q, a, d, _, _, _, _,...

Comment author: @ppedrot The problem ultimately comes from the protect_fv tactic that turns out not to protect the branches of a pattern-matching. Any reduction expert out there?

Comment author: @ppedrot Here is a reduced test case generating a huge goal, even though it does not appear without debug printing (i.e. it remains small even with the print...

Comment author: @ppedrot Gotcha. The problem is that the computing function of ring/field is marked fully reducible by protect_fv. That is, in Ring_polynom.Pphi_dev (ZToField 0) 1 add mul sub opp...