{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":32018344,"defaultBranch":"master","name":"math-comp","ownerLogin":"math-comp","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-03-11T13:13:27.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/11424151?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1716799055.0","currentOid":""},"activityList":{"items":[{"before":"758f98ed5497651c2e9123b8a02c56ff383b316e","after":"70e584295e98308050f24f0a6d08186822b61eda","ref":"refs/heads/experiment/forms","pushedAt":"2024-05-29T14:41:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"affeldt-aist","name":null,"path":"/affeldt-aist","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33154536?s=80&v=4"},"commit":{"message":"mv code","shortMessageHtmlLink":"mv code"}},{"before":"468e59542ea057f43726c08924807cd2b788f9a8","after":"758f98ed5497651c2e9123b8a02c56ff383b316e","ref":"refs/heads/experiment/forms","pushedAt":"2024-05-29T14:38:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"affeldt-aist","name":null,"path":"/affeldt-aist","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33154536?s=80&v=4"},"commit":{"message":"tentative rebase on MathComp 2's master","shortMessageHtmlLink":"tentative rebase on MathComp 2's master"}},{"before":"7a4e882945ee7de1cce72e72e890629d6acabf37","after":null,"ref":"refs/heads/sorted_cat_rcons","pushedAt":"2024-05-27T08:37:35.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"}},{"before":null,"after":"7a4e882945ee7de1cce72e72e890629d6acabf37","ref":"refs/heads/sorted_cat_rcons","pushedAt":"2024-05-27T08:36:43.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"},"commit":{"message":"Adds a lemma to reason by equivalence on paths cut in the middle\ngeneralization of cat_path, but accepts the case where the prefix could\nbe empty (requires a proof by cases)","shortMessageHtmlLink":"Adds a lemma to reason by equivalence on paths cut in the middle"}},{"before":"936a3fd89c621caec7bae631147234f2e4d389f7","after":"6a2791d233a529d7d11d697e917669bbd26cb545","ref":"refs/heads/master","pushedAt":"2024-05-27T07:24:07.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #1216 from jouvelot/big_mknat\n\nAdding big_mknat.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2275722716\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/1216\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/math-comp/math-comp/pull/1216/hovercard\" href=\"https://github.com/math-comp/math-comp/pull/1216\">#1216</a> from jouvelot/big_mknat"}},{"before":"bfc9d750ca1a33768ed1a701efaa74544490c5fd","after":"72442734d4fb2bb105c9832ef41d8ef1c5a51f87","ref":"refs/heads/semi-modules","pushedAt":"2024-05-23T13:28:53.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"[WIP] Generalize linear maps to semilinear maps","shortMessageHtmlLink":"[WIP] Generalize linear maps to semilinear maps"}},{"before":"b63f9082704a434b4c78d9eeb3f5d38918f25261","after":"bfc9d750ca1a33768ed1a701efaa74544490c5fd","ref":"refs/heads/semi-modules","pushedAt":"2024-05-23T12:21:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"[WIP] Generalize linear maps to semilinear maps","shortMessageHtmlLink":"[WIP] Generalize linear maps to semilinear maps"}},{"before":"07fa6f9bb70159ce51412b6970103f535a4720d3","after":"a6d3168427b2e5d65e6e387f92e27bbf758bccc3","ref":"refs/heads/ssralg-function-notation-scope","pushedAt":"2024-05-13T13:50:39.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Fix the notation scope of function notations in ssralg (#978)","shortMessageHtmlLink":"Fix the notation scope of function notations in ssralg (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1614971804\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/978\" data-hovercard-type=\"issue\" data-hovercard-url=\"/math-comp/math-comp/issues/978/hovercard\" href=\"https://github.com/math-comp/math-comp/issues/978\">#978</a>)"}},{"before":"0482738c97b707c65074c5be165e3ed5de46e92a","after":"b63f9082704a434b4c78d9eeb3f5d38918f25261","ref":"refs/heads/semi-modules","pushedAt":"2024-05-13T13:50:39.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Fix the Scale.isLaw factory","shortMessageHtmlLink":"Fix the Scale.isLaw factory"}},{"before":"39c9fafbc32e0e78d89126bed90d08d51cc54f56","after":"936a3fd89c621caec7bae631147234f2e4d389f7","ref":"refs/heads/master","pushedAt":"2024-04-24T17:25:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Add finset lemmas (#1214)\n\nAdd lemmas about finset has, all and bigop","shortMessageHtmlLink":"Add finset lemmas (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2261082933\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/1214\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/math-comp/math-comp/pull/1214/hovercard\" href=\"https://github.com/math-comp/math-comp/pull/1214\">#1214</a>)"}},{"before":"10b6dc65705f3f2e0cc97a9563e4d2a2ae1a856f","after":null,"ref":"refs/heads/fix_changelog","pushedAt":"2024-04-24T14:16:47.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"}},{"before":"c8a578d413fe348fb4361d5266847e09899272e2","after":"39c9fafbc32e0e78d89126bed90d08d51cc54f56","ref":"refs/heads/master","pushedAt":"2024-04-24T14:16:09.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"affeldt-aist","name":null,"path":"/affeldt-aist","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33154536?s=80&v=4"},"commit":{"message":"Fix forgotten entry in changelog (#1215)\n\nEntry from https://github.com/math-comp/math-comp/pull/1094 aht got\r\naccidentaly erased when preparing the changelog of 2.1.0 in\r\nhttps://github.com/math-comp/math-comp/pull/1100","shortMessageHtmlLink":"Fix forgotten entry in changelog (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2261371544\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/1215\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/math-comp/math-comp/pull/1215/hovercard\" href=\"https://github.com/math-comp/math-comp/pull/1215\">#1215</a>)"}},{"before":null,"after":"10b6dc65705f3f2e0cc97a9563e4d2a2ae1a856f","ref":"refs/heads/fix_changelog","pushedAt":"2024-04-24T13:56:13.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Fix forgotten entry in changelog\n\nEntry from https://github.com/math-comp/math-comp/pull/1094 aht got\naccidentaly erased when preparing the changelog of 2.1.0 in\nhttps://github.com/math-comp/math-comp/pull/1100","shortMessageHtmlLink":"Fix forgotten entry in changelog"}},{"before":"ca2eda641699ef1e98bb6743d260b0ef932ce169","after":null,"ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-24T11:28:03.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"}},{"before":"984d7f1f0d6c204d86466f4e501979e4148f265d","after":"c8a578d413fe348fb4361d5266847e09899272e2","ref":"refs/heads/master","pushedAt":"2024-04-24T11:27:59.000Z","pushType":"pr_merge","commitsCount":17,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #1166 from math-comp/hb-semilattices\n\nSemilattices and definitional duality","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2112455204\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/1166\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/math-comp/math-comp/pull/1166/hovercard\" href=\"https://github.com/math-comp/math-comp/pull/1166\">#1166</a> from math-comp/hb-semilattices"}},{"before":"00e2527ce6d2e31428127cad2a743114305ad119","after":"f64815b8bfc5d93a3f6673fbcb63c64bd5ab2e55","ref":"refs/heads/finmap","pushedAt":"2024-04-24T09:58:29.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"CohenCyril","name":"Cyril Cohen","path":"/CohenCyril","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/298705?s=80&v=4"},"commit":{"message":"Starting porting finset","shortMessageHtmlLink":"Starting porting finset"}},{"before":"b5f7d62e3929a0440f9efe0260ad9691c6f7d56f","after":"07fa6f9bb70159ce51412b6970103f535a4720d3","ref":"refs/heads/ssralg-function-notation-scope","pushedAt":"2024-04-23T12:15:36.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Fix the notation scope of function notations in ssralg (#978)","shortMessageHtmlLink":"Fix the notation scope of function notations in ssralg (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1614971804\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/978\" data-hovercard-type=\"issue\" data-hovercard-url=\"/math-comp/math-comp/issues/978/hovercard\" href=\"https://github.com/math-comp/math-comp/issues/978\">#978</a>)"}},{"before":null,"after":"b5f7d62e3929a0440f9efe0260ad9691c6f7d56f","ref":"refs/heads/ssralg-function-notation-scope","pushedAt":"2024-04-23T12:09:47.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Fix the notation scope of function notations in ssralg (#978)","shortMessageHtmlLink":"Fix the notation scope of function notations in ssralg (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1614971804\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/978\" data-hovercard-type=\"issue\" data-hovercard-url=\"/math-comp/math-comp/issues/978/hovercard\" href=\"https://github.com/math-comp/math-comp/issues/978\">#978</a>)"}},{"before":"aeaea040823a4cfac7de16cd29f357793c8f7a5d","after":"0482738c97b707c65074c5be165e3ed5de46e92a","ref":"refs/heads/semi-modules","pushedAt":"2024-04-23T11:46:28.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Fix the Scale.isLaw factory","shortMessageHtmlLink":"Fix the Scale.isLaw factory"}},{"before":"9e172823d668538dd4e8b878fe86ccb436c00b4c","after":"ca2eda641699ef1e98bb6743d260b0ef932ce169","ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-23T11:24:40.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"CHANGELOG","shortMessageHtmlLink":"CHANGELOG"}},{"before":"e9e467b7c5c66439d7fa910d567988d11d3cb26f","after":"984d7f1f0d6c204d86466f4e501979e4148f265d","ref":"refs/heads/master","pushedAt":"2024-04-23T06:28:32.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #1212 from affeldt-aist/typo_20240423\n\nfixes #1211","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2258012315\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/1212\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/math-comp/math-comp/pull/1212/hovercard\" href=\"https://github.com/math-comp/math-comp/pull/1212\">#1212</a> from affeldt-aist/typo_20240423"}},{"before":"3a3216ec586b6166fa0b76d80740fa14e29425a6","after":"9e172823d668538dd4e8b878fe86ccb436c00b4c","ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-22T14:02:14.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Add overlays","shortMessageHtmlLink":"Add overlays"}},{"before":"af8ec1db2fff0d8a93e2dd4e842216a56a78b5e1","after":"3a3216ec586b6166fa0b76d80740fa14e29425a6","ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-22T13:47:48.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Add overlays","shortMessageHtmlLink":"Add overlays"}},{"before":"ac092f5509a0325566b795104b3c840c059cbd33","after":"af8ec1db2fff0d8a93e2dd4e842216a56a78b5e1","ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-18T16:12:08.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Add overlays","shortMessageHtmlLink":"Add overlays"}},{"before":"a0787f210df8144fd7a037256fe01e774a91574b","after":"ac092f5509a0325566b795104b3c840c059cbd33","ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-15T13:11:31.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Add overlays","shortMessageHtmlLink":"Add overlays"}},{"before":"0d82d1a88c218ce90bf5b6f9d899abb76e03bb0c","after":"a0787f210df8144fd7a037256fe01e774a91574b","ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-15T12:28:17.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Add overlays","shortMessageHtmlLink":"Add overlays"}},{"before":"545ed19ba35e02adec531aca9d52766d006b81e6","after":"0d82d1a88c218ce90bf5b6f9d899abb76e03bb0c","ref":"refs/heads/hb-semilattices","pushedAt":"2024-04-12T15:03:49.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pi8027","name":"Kazuhiko Sakaguchi","path":"/pi8027","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/111003?s=80&v=4"},"commit":{"message":"Add overlays","shortMessageHtmlLink":"Add overlays"}},{"before":"ded1f7e8195e90755b321537de2aaa13952c4446","after":null,"ref":"refs/heads/coq_18837","pushedAt":"2024-04-12T08:51:45.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"}},{"before":"da4a9964266e1583848bc75e3a0a999591cb77ba","after":"e9e467b7c5c66439d7fa910d567988d11d3cb26f","ref":"refs/heads/master","pushedAt":"2024-04-12T08:51:42.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #1210 from math-comp/coq_18837\n\nMark classic_sigW and classic_ex as bacported in Coq 8.20","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2239310013\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/1210\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/math-comp/math-comp/pull/1210/hovercard\" href=\"https://github.com/math-comp/math-comp/pull/1210\">#1210</a> from math-comp/coq_18837"}},{"before":"512e4d15e5ac7bc5eafcc2d3bf42c3b3471fd8ac","after":"da4a9964266e1583848bc75e3a0a999591cb77ba","ref":"refs/heads/master","pushedAt":"2024-04-12T07:52:08.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #1209 from affeldt-aist/CONTRIBUTING_20240412\n\nContributing 20240412","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2239175207\" data-permission-text=\"Title is private\" data-url=\"https://github.com/math-comp/math-comp/issues/1209\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/math-comp/math-comp/pull/1209/hovercard\" href=\"https://github.com/math-comp/math-comp/pull/1209\">#1209</a> from affeldt-aist/CONTRIBUTING_20240412"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEVxD5gQA","startCursor":null,"endCursor":null}},"title":"Activity · math-comp/math-comp"}