{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":42843402,"defaultBranch":"master","name":"PG","ownerLogin":"ProofGeneral","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-09-21T04:13:36.000Z","ownerAvatar":"https://github.com/avatars/u/12037073?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726041407.0","currentOid":""},"activityList":{"items":[{"before":"5e14b97eae05d3253e6d70c8ba7b77243933e1a1","after":"1ffca70b2fcfd1c524f9b9e5ceebae07d3b745b6","ref":"refs/heads/master","pushedAt":"2024-09-12T15:58:25.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"Merge pull request #785 from hendriktews/paren\n\nCoq: make printing parentheses flag accessible","shortMessageHtmlLink":"Merge pull request #785 from hendriktews/paren"}},{"before":"a36eb9bed9b8f7f63943fd2e0d505ad34e426136","after":null,"ref":"refs/heads/fix-indent-backslashid","pushedAt":"2024-09-11T07:56:47.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"}},{"before":null,"after":"a36eb9bed9b8f7f63943fd2e0d505ad34e426136","ref":"refs/heads/fix-indent-backslashid","pushedAt":"2024-09-11T07:55:48.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Fix #757 indentation of \"\\in\"\n\nThe lexer now glues a \"\\\" to an immediately following word if it is\nitself preceded by a space.\n\nNote that for really good indentation you should try to add something\nlike this to your configuration:\n\n(setq coq-smie-user-tokens '((\"\\\\in\" . \"=\")))\n\nto tell the indentation grammar that \\in has the same precedence as\n\"=\".\n\nTest added.","shortMessageHtmlLink":"Fix #757 indentation of \"\\in\""}},{"before":"3a99da275523c8f844fdfa3dd073295eece939f3","after":"5e14b97eae05d3253e6d70c8ba7b77243933e1a1","ref":"refs/heads/master","pushedAt":"2024-09-09T14:09:04.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"Merge pull request #787 from hendriktews/8.20\n\nCI: add Coq 8.20","shortMessageHtmlLink":"Merge pull request #787 from hendriktews/8.20"}},{"before":"734bcdb27fdcf54fbe6ab05bf957408e70c69748","after":"3a99da275523c8f844fdfa3dd073295eece939f3","ref":"refs/heads/master","pushedAt":"2024-09-05T11:05:28.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #741 from hoheinzollern/patch-1\n\nAdding unicode arrow >->","shortMessageHtmlLink":"Merge pull request #741 from hoheinzollern/patch-1"}},{"before":"1b89aa361149dac88005d491894f21a8d83df6fc","after":"734bcdb27fdcf54fbe6ab05bf957408e70c69748","ref":"refs/heads/master","pushedAt":"2024-09-05T10:34:35.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #776 from jgarte/jgarte-patch-1\n\nUpdate Makefile","shortMessageHtmlLink":"Merge pull request #776 from jgarte/jgarte-patch-1"}},{"before":"11dcebe247632f91c162392b4b7b3c37a9ded44a","after":"1b89aa361149dac88005d491894f21a8d83df6fc","ref":"refs/heads/master","pushedAt":"2024-09-05T10:34:19.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #783 from ruipedro16/add-ecall-keyword\n\nEasyCrypt: add `ecall` keyword","shortMessageHtmlLink":"Merge pull request #783 from ruipedro16/add-ecall-keyword"}},{"before":"067bffa4bb0f11f163a7c47b4cb562e37b1fbe46","after":"11dcebe247632f91c162392b4b7b3c37a9ded44a","ref":"refs/heads/master","pushedAt":"2024-09-05T10:34:06.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #784 from Columbus240/CoqProject\n\nChange _CoqProject separator settings","shortMessageHtmlLink":"Merge pull request #784 from Columbus240/CoqProject"}},{"before":"c3e6c391e7eeb6f495327eae4fab8619fed70748","after":"067bffa4bb0f11f163a7c47b4cb562e37b1fbe46","ref":"refs/heads/master","pushedAt":"2024-09-05T10:31:38.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #782 from Matafou/fix-no-strip-newlines\n\nFix #781 PG does not position to error + other buggy locations.","shortMessageHtmlLink":"Merge pull request #782 from Matafou/fix-no-strip-newlines"}},{"before":"eca47ea8afdfcd94b4c8d88ee640f6631cfe5c5d","after":"c3e6c391e7eeb6f495327eae4fab8619fed70748","ref":"refs/heads/master","pushedAt":"2024-09-02T11:21:59.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"Merge pull request #778 from hendriktews/ci-rc\n\nCI: add Coq 8.20+rc1","shortMessageHtmlLink":"Merge pull request #778 from hendriktews/ci-rc"}},{"before":"eca47ea8afdfcd94b4c8d88ee640f6631cfe5c5d","after":null,"ref":"refs/heads/fix-no-strip-newlines","pushedAt":"2024-07-09T14:27:33.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"}},{"before":null,"after":"eca47ea8afdfcd94b4c8d88ee640f6631cfe5c5d","ref":"refs/heads/fix-no-strip-newlines","pushedAt":"2024-07-09T14:13:13.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #780 from Matafou/fix-779-regression-cannot-step-Fail-correctly\n\nFixes #779 regression cannot step Fail correctly.","shortMessageHtmlLink":"Merge pull request #780 from Matafou/fix-779-regression-cannot-step-F…"}},{"before":"837f587bd5801b8b1ca30734abf3a59194959e24","after":"eca47ea8afdfcd94b4c8d88ee640f6631cfe5c5d","ref":"refs/heads/master","pushedAt":"2024-07-08T15:25:47.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #780 from Matafou/fix-779-regression-cannot-step-Fail-correctly\n\nFixes #779 regression cannot step Fail correctly.","shortMessageHtmlLink":"Merge pull request #780 from Matafou/fix-779-regression-cannot-step-F…"}},{"before":"99f91e873ec2fdc41079555db1130f07d9a9ce89","after":"837f587bd5801b8b1ca30734abf3a59194959e24","ref":"refs/heads/master","pushedAt":"2024-07-06T17:33:34.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"Merge pull request #777 from hendriktews/ci-update\n\nCI: update to Coq 8.19.2 and Emacs 29.4","shortMessageHtmlLink":"Merge pull request #777 from hendriktews/ci-update"}},{"before":"ffd7000505bbca3f52df36ed4a025e2bdcea07d3","after":null,"ref":"refs/heads/coq-dont-strip-cr","pushedAt":"2024-06-19T12:10:02.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"erikmd","name":"Erik Martin-Dorel","path":"/erikmd","primaryAvatarUrl":"https://github.com/avatars/u/10367254?s=80&v=4"}},{"before":"0e0170f96f5feaeefe59052a08373080acc20393","after":"99f91e873ec2fdc41079555db1130f07d9a9ce89","ref":"refs/heads/master","pushedAt":"2024-06-19T12:09:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"erikmd","name":"Erik Martin-Dorel","path":"/erikmd","primaryAvatarUrl":"https://github.com/avatars/u/10367254?s=80&v=4"},"commit":{"message":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil) (#774)\n\nRelated: https://github.com/ProofGeneral/PG/issues/773","shortMessageHtmlLink":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil) (#774)"}},{"before":"b9fdbbf0b50fc2c0c2ef799d05b9c6c1019d17aa","after":"0e0170f96f5feaeefe59052a08373080acc20393","ref":"refs/heads/master","pushedAt":"2024-06-19T08:41:03.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"proof-stat: admitted proofs count as failing\n\nChange `proof-check-chunks' such that Admitted proofs are reported as\nfailing.","shortMessageHtmlLink":"proof-stat: admitted proofs count as failing"}},{"before":"cb23709ad0c9a9ca0ee48b3ee73c29caea243b98","after":"b9fdbbf0b50fc2c0c2ef799d05b9c6c1019d17aa","ref":"refs/heads/master","pushedAt":"2024-06-15T15:46:55.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://github.com/avatars/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #768 from Matafou/splash-time","shortMessageHtmlLink":"Merge pull request #768 from Matafou/splash-time"}},{"before":null,"after":"ffd7000505bbca3f52df36ed4a025e2bdcea07d3","ref":"refs/heads/coq-dont-strip-cr","pushedAt":"2024-06-15T14:28:22.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"erikmd","name":"Erik Martin-Dorel","path":"/erikmd","primaryAvatarUrl":"https://github.com/avatars/u/10367254?s=80&v=4"},"commit":{"message":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil)\n\nRelated: https://github.com/ProofGeneral/PG/issues/773","shortMessageHtmlLink":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil)"}},{"before":"1adcaaf4f0d09a29977d45fe5360fb1dce381803","after":"cb23709ad0c9a9ca0ee48b3ee73c29caea243b98","ref":"refs/heads/master","pushedAt":"2024-05-13T07:20:08.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"proof-stat: add test for proof-check-annotate","shortMessageHtmlLink":"proof-stat: add test for proof-check-annotate"}},{"before":"afae49509f5cf06bb8a9573444dbf0137adfd6e0","after":"1adcaaf4f0d09a29977d45fe5360fb1dce381803","ref":"refs/heads/master","pushedAt":"2024-05-02T07:46:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"CI: update CI config to include Emacs 29.3","shortMessageHtmlLink":"CI: update CI config to include Emacs 29.3"}},{"before":"6cace58d0d632c4eafa18959319a484fb5c07238","after":"afae49509f5cf06bb8a9573444dbf0137adfd6e0","ref":"refs/heads/master","pushedAt":"2024-04-29T14:11:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"update Coq ignored extensions and add dired-x compatibility","shortMessageHtmlLink":"update Coq ignored extensions and add dired-x compatibility"}},{"before":"1f0c75788a70fc206a060394d92736e51ccc6a9d","after":"6cace58d0d632c4eafa18959319a484fb5c07238","ref":"refs/heads/master","pushedAt":"2024-04-25T09:39:47.000Z","pushType":"pr_merge","commitsCount":9,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"proof-stat: address review comments\n\n- read-only and no undo in report buffer\n- add a batch mode test for proof-check-proofs; require seq library to\n make this work in Emacs 26","shortMessageHtmlLink":"proof-stat: address review comments"}},{"before":"7a28fa207a5992224c32abc988f936596f13a6b2","after":"1f0c75788a70fc206a060394d92736e51ccc6a9d","ref":"refs/heads/master","pushedAt":"2024-04-25T07:57:01.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"ignore 3-pane mode if frame is too small\n\nFixes #760.","shortMessageHtmlLink":"ignore 3-pane mode if frame is too small"}},{"before":"d30569d8c56629cfa93fcd46e59cb52e863fe77a","after":"7a28fa207a5992224c32abc988f936596f13a6b2","ref":"refs/heads/master","pushedAt":"2024-04-20T12:54:54.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"proof-shell, pg-response: indentation fixes","shortMessageHtmlLink":"proof-shell, pg-response: indentation fixes"}},{"before":"1a37480857b6408b0c57e655ceb302ce8f884833","after":"d30569d8c56629cfa93fcd46e59cb52e863fe77a","ref":"refs/heads/master","pushedAt":"2024-04-18T09:06:09.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"CI: extend goals present tests with Search and Check commdands\n\n- After Search and Check the goals should be up-to-date and the\n response should be visible, also in two-pane mode.\n- Extend existing tests to check that the response is also visible in\n two-pane mode, if applicable.\n- Use Proof General variables containing the buffer instead of buffer\n names.","shortMessageHtmlLink":"CI: extend goals present tests with Search and Check commdands"}},{"before":"1566fd882e1618d0843cb5930632fe00b681167f","after":"1a37480857b6408b0c57e655ceb302ce8f884833","ref":"refs/heads/master","pushedAt":"2024-04-06T17:07:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"coq: clear goals buffer after admitted\n\nOnly add the declaration info message to the right regular expression\nand generic Proof General will clear the goals buffer. As a side\neffect the declaration info message won't show up in the response\nbuffer any more. Need to change the tests that rely on this.","shortMessageHtmlLink":"coq: clear goals buffer after admitted"}},{"before":"2637216deea35e4a91b14c7d61a20328fe6dad84","after":"1566fd882e1618d0843cb5930632fe00b681167f","ref":"refs/heads/master","pushedAt":"2024-03-31T19:08:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"CI: fix workflow problem in cipg and sync currently used containers","shortMessageHtmlLink":"CI: fix workflow problem in cipg and sync currently used containers"}},{"before":"01aa3173419ea9349ae00d3bd2b14264dd6d6c47","after":"2637216deea35e4a91b14c7d61a20328fe6dad84","ref":"refs/heads/master","pushedAt":"2024-03-28T23:44:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"Revert \"texi-docstring-magic.el: Fix regression in last change\"\n\nThis reverts commit f620526756c6f24ddf40c515c6cc9bba969a6535 which was\npushed directly without running CI.","shortMessageHtmlLink":"Revert \"texi-docstring-magic.el: Fix regression in last change\""}},{"before":"f620526756c6f24ddf40c515c6cc9bba969a6535","after":"01aa3173419ea9349ae00d3bd2b14264dd6d6c47","ref":"refs/heads/master","pushedAt":"2024-03-28T22:58:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://github.com/avatars/u/16718397?s=80&v=4"},"commit":{"message":"Revert \"(texi-docstring-magic-texi-for): Use `help-function-arglist`\"\n\nThis reverts commit a63a9b13185b0a2f13eb417165708f9cf38cc827 because\nit breaks CI.","shortMessageHtmlLink":"Revert \"(texi-docstring-magic-texi-for): Use help-function-arglist\""}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xMlQxNTo1ODoyNS4wMDAwMDBazwAAAAS0lzGL","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xMlQxNTo1ODoyNS4wMDAwMDBazwAAAAS0lzGL","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMy0yOFQyMjo1ODoxOC4wMDAwMDBazwAAAAQiOy2T"}},"title":"Activity · ProofGeneral/PG"}