{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6700","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6700/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6700/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6700/events","html_url":"https://github.com/coq/coq/pull/6700","id":294751365,"number":6700,"title":"[ssr] rewrite Ssripats and Ssrview in the tactic monad","user":{"login":"gares","id":1013846,"avatar_url":"https://avatars2.githubusercontent.com/u/1013846?v=4","gravatar_id":"","url":"https://api.github.com/users/gares","html_url":"https://github.com/gares","followers_url":"https://api.github.com/users/gares/followers","following_url":"https://api.github.com/users/gares/following{/other_user}","gists_url":"https://api.github.com/users/gares/gists{/gist_id}","starred_url":"https://api.github.com/users/gares/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gares/subscriptions","organizations_url":"https://api.github.com/users/gares/orgs","repos_url":"https://api.github.com/users/gares/repos","events_url":"https://api.github.com/users/gares/events{/privacy}","received_events_url":"https://api.github.com/users/gares/received_events","type":"User","site_admin":false},"labels":[{"id":396673733,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20redesign","name":"kind: redesign","color":"0052cc","default":false},{"id":762376854,"url":"https://api.github.com/repos/coq/coq/labels/needs:%20merge%20of%20dependency","name":"needs: merge of dependency","color":"cc3b6b","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/5","html_url":"https://github.com/coq/coq/milestone/5","labels_url":"https://api.github.com/repos/coq/coq/milestones/5/labels","id":2550427,"number":5,"title":"8.8+beta1","description":"","creator":{"login":"maximedenes","id":647105,"avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false},"open_issues":152,"closed_issues":375,"state":"open","created_at":"2017-05-30T13:02:47Z","updated_at":"2018-02-25T09:38:23Z","due_on":"2018-03-15T07:00:00Z","closed_at":null},"comments":32,"created_at":"2018-02-06T13:02:44Z","updated_at":"2018-02-26T09:21:20Z","closed_at":null,"author_association":"OWNER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/6700","html_url":"https://github.com/coq/coq/pull/6700","diff_url":"https://github.com/coq/coq/pull/6700.diff","patch_url":"https://github.com/coq/coq/pull/6700.patch"},"body":"depends on #6676\r\ndepended upon by #6705\r\n\r\n##  ssr: rewrite Ssripats and Ssrview in the tactic monad\r\n\r\n`Ssripat`s and `Ssrview` are now written in the Tactic Monad.\r\n`Ssripats` implements the `=>` tactical.\r\n`Ssrview` implements the application of forward views.\r\n\r\nThe code is, according to my tests, 100% backward compatible.\r\nThe code is much more documented than before.\r\nMoreover the `ist` (ltac context) used to interpret views is the correct\r\none (the one at `ARGUMENT EXTEND` interp time, not the one at `TACTIC\r\nEXTEND` execution time).  Some of the code not touched by this commit\r\nstill uses the incorrect `ist`, so its visibility in `TACTIC EXTEND`\r\ncan't be removed yet.\r\n\r\nThe main changes in the code are:\r\n- intro patterns are implemented using a state machine (a goal comes\r\n  with a state). `Ssrcommon.MakeState` provides an easy way for a tactic\r\n  to enrich the goal with with data of interest, such as the set of\r\n  hyps to be cleared.  This cleans up the old implementation that, in\r\n  order to thread the state, that to redefine a bunch of tclSTUFF\r\n- the interpretation of (multiple) forward views uses the state to\r\n  accumulate intermediate results\r\n- the bottom of `Sscommon` collects a bunch of utilities written in the\r\n  tactic monad. Most of them are the rewriting of already existing\r\n  utilities.  When possible the old version was removed.\r\n\r\n## Bench\r\nThe final bench is at\r\n  https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/343/console\r\n```\r\n┌──────────────────────────┬─────────────────────────┬─────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬─────────────────┐\r\n│                          │      user time [s]      │             CPU cycles              │           CPU instructions            │  max resident mem [KB]   │   mem faults    │\r\n│                          │                         │                                     │                                       │                          │                 │\r\n│             package_name │     NEW     OLD PDIFF   │           NEW           OLD PDIFF   │            NEW            OLD PDIFF   │     NEW     OLD  PDIFF   │ NEW OLD PDIFF   │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│                coq-flocq │   59.28   59.79 -0.85 % │  163360961987  164130189895 -0.47 % │   209817098860   209928779194 -0.05 % │  661724  662028  -0.05 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│              coq-bignums │   75.43   75.60 -0.22 % │  209795361790  210105426772 -0.15 % │   282973447933   283097398279 -0.04 % │  524316  524064  +0.05 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│                 coq-corn │ 1488.82 1491.98 -0.21 % │ 4134652361208 4142647619037 -0.19 % │  6386604329003  6388790265638 -0.03 % │  828000  827896  +0.01 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│     coq-mathcomp-algebra │  169.60  169.87 -0.16 % │  471186959143  469528041062 +0.35 % │   660937779861   654968488065 +0.91 % │  649912  587096 +10.70 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│              coq-unimath │ 1197.26 1199.06 -0.15 % │ 3329747275201 3329945987975 -0.01 % │  5739017885925  5734923718832 +0.07 % │  956524 1022956  -6.49 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│                coq-color │  569.62  570.36 -0.13 % │ 1589743770149 1590307788530 -0.04 % │  1979950285536  1980272711262 -0.02 % │ 1437660 1437176  +0.03 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│                  coq-vst │ 2920.91 2922.24 -0.05 % │ 8142944302234 8152735836904 -0.12 % │ 11781160570278 11783642046504 -0.02 % │ 2221056 2220156  +0.04 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│    coq-mathcomp-fingroup │   61.05   61.03 +0.03 % │  168790803006  167542227156 +0.75 % │   234364944596   230821564726 +1.54 % │  593120  528676 +12.19 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│               coq-geocoq │ 3045.76 3044.44 +0.04 % │ 8474815873935 8475251963555 -0.01 % │ 13957211859192 13961632218507 -0.03 % │ 1205328 1206040  -0.06 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│      coq-formal-topology │   33.96   33.94 +0.06 % │   94401259874   94469027451 -0.07 % │   123984963326   124055727019 -0.06 % │  481968  481944  +0.00 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│         coq-fiat-parsers │  653.72  653.33 +0.06 % │ 1822993805663 1822521509106 +0.03 % │  2946440807755  2945756573347 +0.02 % │ 2972504 2972552  -0.00 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│                 coq-hott │  315.86  315.07 +0.25 % │  860207048464  858544147367 +0.19 % │  1374343701278  1374550105658 -0.02 % │  497024  496952  +0.01 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│            coq-fiat-core │  102.44  101.99 +0.44 % │  289651316397  289064811919 +0.20 % │   373990504395   374250719307 -0.07 % │  499912  500112  -0.04 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│             coq-compcert │  809.28  805.16 +0.51 % │ 2256060420160 2247041484804 +0.40 % │  3416045599562  3413777934426 +0.07 % │ 1369756 1370160  -0.03 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│       coq-mathcomp-field │  443.25  440.75 +0.57 % │ 1232378182451 1225106305951 +0.59 % │  2037560374969  2022361811598 +0.75 % │  812044  717828 +13.13 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│           coq-coquelicot │   76.33   75.84 +0.65 % │  210079002765  207784885497 +1.10 % │   264293519353   258292008807 +2.32 % │  713664  657304  +8.57 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│   coq-mathcomp-character │  266.43  264.52 +0.72 % │  739760358681  733145050660 +0.90 % │  1083365378211  1073975712248 +0.87 % │ 1121544  978308 +14.64 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│    coq-mathcomp-solvable │  191.86  190.18 +0.88 % │  531748923791  528800354872 +0.56 % │   764120864069   761578892782 +0.33 % │  848456  708744 +19.71 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│   coq-mathcomp-odd_order │ 1384.46 1370.92 +0.99 % │ 3846233316511 3808422797770 +0.99 % │  6666192488494  6590508255997 +1.15 % │ 1368592 1081716 +26.52 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│ coq-mathcomp-real_closed │  168.70  166.62 +1.25 % │  467025749357  462193447032 +1.05 % │   707084547538   699173048256 +1.13 % │  847704  716848 +18.25 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤\r\n│   coq-mathcomp-ssreflect │   41.60   40.44 +2.87 % │  114154621950  111840028077 +2.07 % │   141332091469   137041182630 +3.13 % │  536780  477624 +12.39 % │   0   0  +nan % │\r\n└──────────────────────────┴─────────────────────────┴─────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴─────────────────┘\r\n```"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/368437484","html_url":"https://github.com/coq/coq/pull/6700#issuecomment-368437484","issue_url":"https://api.github.com/repos/coq/coq/issues/6700","id":368437484,"user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars1.githubusercontent.com/u/460771?v=4","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"created_at":"2018-02-26T09:21:20Z","updated_at":"2018-02-26T09:21:20Z","author_association":"OWNER","body":"I just had a look at this, considering the questions around #6676. As far as I understand, the main motivation for the added business of #6676 is to have a function `ipat_tac1` of the short type `ssripat -> unit tactic` (*) rather than, say, `ssripat -> to_clear * unit tactic`, or, say, `ssripat -> kont:unit tactic -> unit tactic`, and to use the `Proofview.<*>` (to the price of hard-wiring a new kind of side effect `goal_with_state` in `Proofview`) rather than a custom (and local) `<*>` which would work on type `to_clear * unit tactic` or `kont:unit tactic -> unit tactic` rather than `unit tactic` (compare to the custom and local `tclTHEN_a`-style composition operators of the previous implementation).\r\n\r\nI appreciate the effort of the author to think in term of compositionality. The code produced is well-structured and I would be tempted to acknowledge this effort and to recommend the work as it is. I would however recommend for the longer term, that the author try to also think in terms of factorizability of code, which is another important aspect of a sustainable maintenance.\r\n\r\n(*) up to the `future_ipats` thing."}}
{"actor":{"display_login":"herbelin"}}