coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Clément Pit-Claudel <cpitcla AT mit.edu>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Debugging cbn's performance
- Date: Tue, 14 Apr 2020 15:16:38 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitcla AT mit.edu; spf=SoftFail smtp.mailfrom=cpitcla AT mit.edu; spf=None smtp.helo=postmaster AT mout.kundenserver.de
- Autocrypt: addr=cpitcla AT mit.edu; prefer-encrypt=mutual; keydata= xsFNBFStGiEBEAC8eHa+DdcrVtDSwYoIgoUtMfRAan4bdLxZuNIASy6iFytCHNsKqfPkq8zD YV2+uMtbdcnjapE038nidEMItNhO04JdZ+PJ6jvJo1gW+XI4fM8uzkGZauwR+d3hEq6goFSp rIlSlaVf2g5q4OKxI754yqwz00++EZhZQMntzoKQVV9stJ5eQ+gxTT1ANr7wQKbjn/8PM/Cg hBZvYLhh+WsS0Ko5qZuWdsvUBLpprmCWkP4FpZ234/tWpdVID65nlHpu25+6ajIcxfCIK+dN 2br0wN1szTeQFG19cfr3jXEvwHmLQbQqCg4UH+2b7JpMGR2/KWjqRWfWVvZMPVeJdOsZHx53 k6HIbEhvFBHbmqCI6FAZQjkgzGGkrSD92+jeMYiCTxRKqq2hFZ6xqQ6pJdXD1TXcIYPEs7rA MwcNMj8g4e6vuI+2CjHyQQkyMPAEi8guNPnyfBb648f1lxj7JiJu/ehRghIP5u/kLOsHNCKG QgCT04sawBZYHqEVYni8oHlGJcdWGT5/UI4B+wn70eXvYSScZEaB+S2s/bD0cdlSpHY5Od3l tpRZTva+ydswlrz4fxbYF45s6rFpqVwBMfNv3gqhBFXbuiEEctcTSGqhHxxT4R+24Yn+ZSBa EfUbrKnVTUmV20k+57rghiVw2wpj8v7sn3QXt96HJ9ImY4JvuwARAQABzTNDbMOpbWVudCBQ aXQtLUNsYXVkZWwgPGNsZW1lbnQucGl0Y2xhdWRlbEBsaXZlLmNvbT7CwXsEEwECACUCGyMG CwkIBwMCBhUIAgkKCwQWAgMBAh4BAheABQJUrRuVAhkBAAoJEPqg+cTm90wjResP/j6A9F81 5C78IKzYdYIa7dHNWi4djRdUd79iIHGeFrao6qf7NX3XZmWkpgWExeanaqS7MmJjyXYEh6La JnzojETK+LVYk2xOanKQch2QrxGZVsXFtp/h102J1yTkUKp4g3uyaVlMLDg1P4eHSJC2YHr2 GtE4HTMUW6SThZ1nJQTrSrVpxTL9hRU/O4VIycogD9++zQ3Y1KzGq5xEi+UbjmcycR0dhSSD vAqo3yU46rfgyKPT99JR0edvYAbJaw5uq35Y0y0L6/gV4Bj6c69TADeyc5iTvagPLUWfeWUv YS2M+j7EWRePRmkuBw1ZPxKlibhsfzZBtIt6jEFd+U8ES5ycm6LSqu3ryGlFuFvdrkWzO7Fp SsHo03r6jtc8nY2jnOzsuxVvakMW1JqAiIP2H57Xyv1gZWb60dJDy2k9M7SCONdFLSU6E3k1 ZjyVkWD2cDhoLV2jy11U9hxQt+OfH2M/f+1cZe5Fberz4ceQ0ssLdfOo4dcGd+MW1lixXYj/ VrZj+QmqOdpzjxyLlzd94Mj7cvNzn/bJV4af6fgY+zbGHj8POrIVrIVO0B2/lSLG2HqO+srI 38gpz8vsVuqtuA5QSPT58H3PeAn0uYetCYNammoPRbQadgQOa8z2Bns2c2HsDj4baMck8d+h PDf7MdiEAW7zE6pxQtdr0xo6EREczsFNBFStGiEBEADTKhFNyVXInTxg1rioBtixWbNr2yRt Wu+jR4ECvPW1rY2ThYQ/I2Z97irnhmFnuepIM/gGviXN2OG1+xSBGjJVN4i9chnhxTLHKc+d uqq01tD/OGItoH63MQekOPhsymUyd95Ci01nM18pTzZDghYal47Ex/j+rlM8AaBmtSbTNGN/ rTFGUMvregVqrnnrYfs/LlooxHtTAbpY19e/sZX5b9EWdsa6k074bt6ew3TQ9xm7/4grV06H vc1b0I79Rk8vPslXh9Wh6qS4+OLkvFWnwTUachInxlD4E0wdK33XaaSxarFSmnYcVrsW2Izy gPoRMYgB5oUPtmUE8F/WfhWZ0Z3P9cKXx3EP6Z25PN3UJFXr+kZpVow65bx0MFIu/N5ygbHX sQ482CQwgzg5rr3arxXB9AknHC753jSJeld1oAsy1J+hmY7iSGxjoZeL4Yoq8IINNeq1QbH0 vo9esK4hmUi2fXIg/GKoramWJ6DjiObuHOJvXkiV9QS7GVnlHq1Z2/HGN998n6nmUj7i70lk a1XiJ3LFtAcxqsnjc1hXdi2yuOnbHRhpVBIuCEsj3EKtp5zTVkAK77c5LOIIRoij9ACUaT6x D6r93jbuw5HbSHP3aW3P/jkQ3kgZXPaa6890kPe3eRqyf9iOYpcAWu71TSqQldaOZ1Nl2Ttk 1JY8UQARAQABwsFfBBgBAgAJBQJUrRohAhsMAAoJEPqg+cTm90wjqucP/3di/s4HIltDHvte Css8JYINdfkdfkt5ub75YLoBa5blPIMJ/E5HMiQ90dAnIlg0ZQ39AOJ0agyg7vNSi199Y1Kn 3TSpAAiTo5V8ry8CuyqJ+0t4czr5PUr6P+8ggFAXMSn5NbZPQHZRods3GFtO5pq/6gwWxBiO 6VcLEqeEdz+ZzusISIPtuz56biaeR5+lh3FVITvXzVHY/7mXeKKb/HKy4gwHmNnWAqrELjg1 vtTtJJnPyrTUE6vYzO1pfNs7ynfcylV5q6oloLNwChQweMfFtDHOiOv6wweLav43+28WAElD Saw618yT8fFSWYGl9tUmADoRgHfFrcHrcZ0v/27C4Gh/bbESUJqm4ik1wZPrEjIwSZJFAm5k 2wTlRMnuxT7cGZVYChG2awk5wbYqofwivGcpY1X+HSGivYXEGQmvPSdONFbgr1FUDXKgcsbw qsxaBtx407fDL8ohnWnsjqB0X6sWUjllm8Afxabwr2WCzdRut6/HIXcrFHIFjzHokIqartiO 0J0tmANHEACjmDgF6E1XlUi0SnNXDV0Us2z4843kEocj8Z6zFNQkuMy0ArQbuxVG0i5jaRaA nI6nLB+ouU4UJNUnzrVnVr2sQuruMIIb9u7DVTodwfkrEVw0aoiSW3D7CTATZcBihOo8NZjm hze1s8uad9n9PQF+gigV
- Ironport-phdr: 9a23:DQ7wjBE1zsMOhxN9ztkj6p1GYnF86YWxBRYc798ds5kLTJ76rs2wAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWapAQfERTnNAdzOv+9WsuL15z2hKiO/Mj4ZBwArz6ga/smJxKv6A7Vq8M+gI14K693xAGf8VVSfOED7mfpIF+VgyHE59v115pq7ihdv7p1/NZBTa7+dow9TKAeATg7ZTNmrPb3vAXOGFPcrkAXVX8bx18RW1CcsUPKG6zpuy6/jdJTnSmXOcqsF+IxXim+qaR2ThPljjwKLSA06ifbh54o1f4JkFeavxV6hrXsTsSNLvMvLKbcYZUXSXcTBp8ABRwEOZu1as40N8REOO9Zq4fnoF5f/x6/GU+hCP69kTI=
Hi all,
The manual says that 'cbn tactic is claimed to be a more principled, faster
and more predictable replacement for simpl', but I'm running into significant
performance issues with it. In our latest project we're routinely running
into cases in which a plain call to cbn takes roughly an order of magnitude
more time than a plain call to simpl, while producing the same results (simpl
is itself ~2 orders of magnitude slower than cbv, but cbv reduces too
aggressively for our use case).
Are there general guidelines that we should apply when trying to investigate
this discrepancy? I've confirmed that I don't have opaque proofs blocking
reduction, and the final term is pretty small (maybe 30 lines). It would be
great to have some way to benchmark `simpl` and `cbn`, to know what parts the
reduction machinery is spending time on.
Thanks!
Clément.
- [Coq-Club] Debugging cbn's performance, Clément Pit-Claudel, 04/14/2020
- <Possible follow-up(s)>
- [Coq-Club] Debugging cbn's performance, Clément Pit-Claudel, 04/14/2020
Archive powered by MHonArc 2.6.18.