{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":259489943,"defaultBranch":"main","name":"lean-playground","ownerLogin":"utensil","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2020-04-28T00:31:50.000Z","ownerAvatar":"https://github.com/avatars/u/64258?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1715477258.0","currentOid":""},"activityList":{"items":[{"before":"838f6257c719985033cb299032e2fd26d203a5aa","after":"1d59f39e9e16f3178fb76efadffab4eb30d11ad9","ref":"refs/heads/main","pushedAt":"2024-06-15T10:08:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Add more docs about tactics","shortMessageHtmlLink":"Add more docs about tactics"}},{"before":"92a586d8828667db911525b1d7f44b0d49bd5614","after":"838f6257c719985033cb299032e2fd26d203a5aa","ref":"refs/heads/main","pushedAt":"2024-06-13T09:22:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Add Json experiments","shortMessageHtmlLink":"Add Json experiments"}},{"before":"2bc3ddeec5b92f5fba43a0cf079e4ba7ad0d704a","after":"92a586d8828667db911525b1d7f44b0d49bd5614","ref":"refs/heads/main","pushedAt":"2024-06-12T13:40:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Try mk_all with the linker flag on all OSes","shortMessageHtmlLink":"Try mk_all with the linker flag on all OSes"}},{"before":"3c0027e18a20c7898a08978e04fb03429b94b029","after":"2bc3ddeec5b92f5fba43a0cf079e4ba7ad0d704a","ref":"refs/heads/main","pushedAt":"2024-06-12T13:31:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Should be `weakLinkArgs`","shortMessageHtmlLink":"Should be <code>weakLinkArgs</code>"}},{"before":"f770e70d0ba133b45f836ac05a5095b27bf0e7b7","after":"3c0027e18a20c7898a08978e04fb03429b94b029","ref":"refs/heads/main","pushedAt":"2024-06-12T13:25:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"`lake -R`","shortMessageHtmlLink":"<code>lake -R</code>"}},{"before":"0dde8efe7d9085d50d3186d1613776c20c6335c5","after":"f770e70d0ba133b45f836ac05a5095b27bf0e7b7","ref":"refs/heads/main","pushedAt":"2024-06-12T13:21:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Try add `weakLeancArgs := #[\"-lLake\"]`","shortMessageHtmlLink":"Try add <code>weakLeancArgs := #[\"-lLake\"]</code>"}},{"before":"9390014ae8be843a5fb2db8da386fd494aa45f71","after":"0dde8efe7d9085d50d3186d1613776c20c6335c5","ref":"refs/heads/main","pushedAt":"2024-06-12T13:17:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Try bash","shortMessageHtmlLink":"Try bash"}},{"before":"2e053a39e2a605a7b997318e8a36ae80273264aa","after":"9390014ae8be843a5fb2db8da386fd494aa45f71","ref":"refs/heads/main","pushedAt":"2024-06-12T12:44:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Try `lake env lake exe mk_all` on Windows","shortMessageHtmlLink":"Try <code>lake env lake exe mk_all</code> on Windows"}},{"before":"1720ad72e9b9f9d57e6ad2b00e44395d050e9ed2","after":"2e053a39e2a605a7b997318e8a36ae80273264aa","ref":"refs/heads/main","pushedAt":"2024-06-12T12:39:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Try `lake env lake exe mk_all`","shortMessageHtmlLink":"Try <code>lake env lake exe mk_all</code>"}},{"before":"cb78fd94f448bb07d76edf11d1b9609b9c9c83d5","after":"1720ad72e9b9f9d57e6ad2b00e44395d050e9ed2","ref":"refs/heads/main","pushedAt":"2024-06-12T12:18:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Try mk_all","shortMessageHtmlLink":"Try mk_all"}},{"before":"0ef9f6526a0c209b7f7df4c3813ab373767a75b0","after":"cb78fd94f448bb07d76edf11d1b9609b9c9c83d5","ref":"refs/heads/main","pushedAt":"2024-06-12T12:16:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Bump to leanprover/lean4:v4.9.0-rc1","shortMessageHtmlLink":"Bump to leanprover/lean4:v4.9.0-rc1"}},{"before":"8c46d8bb51ebf1951da4f18318cd650852069a2a","after":"0ef9f6526a0c209b7f7df4c3813ab373767a75b0","ref":"refs/heads/main","pushedAt":"2024-06-12T11:37:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Add some experiments","shortMessageHtmlLink":"Add some experiments"}},{"before":"e716bdeda376ee728657bd6c4730735c0f6e5ab3","after":"8c46d8bb51ebf1951da4f18318cd650852069a2a","ref":"refs/heads/main","pushedAt":"2024-05-28T04:47:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Run `lake build Duper` first","shortMessageHtmlLink":"Run <code>lake build Duper</code> first"}},{"before":"4e732ebd38e6db410b6efeef84ea7966f4031e49","after":"e716bdeda376ee728657bd6c4730735c0f6e5ab3","ref":"refs/heads/main","pushedAt":"2024-05-27T09:12:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Bump mathlib","shortMessageHtmlLink":"Bump mathlib"}},{"before":"a9b1c5913baf0323a6c5f5f82ec9d300be22c262","after":"4e732ebd38e6db410b6efeef84ea7966f4031e49","ref":"refs/heads/main","pushedAt":"2024-05-27T08:33:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Partially recover Duper examples","shortMessageHtmlLink":"Partially recover Duper examples"}},{"before":"9188be68974023d153be035abae05e0410ef75a9","after":"a9b1c5913baf0323a6c5f5f82ec9d300be22c262","ref":"refs/heads/main","pushedAt":"2024-05-22T13:01:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Bump to leanprover/lean4:v4.8.0-rc2 [annotate]","shortMessageHtmlLink":"Bump to leanprover/lean4:v4.8.0-rc2 [annotate]"}},{"before":"e10ea0a1ed5161c030767ee30f6a9dc55675327c","after":"9188be68974023d153be035abae05e0410ef75a9","ref":"refs/heads/main","pushedAt":"2024-05-22T08:50:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Extract fillLeft","shortMessageHtmlLink":"Extract fillLeft"}},{"before":"60790037b8b3c9259d3506ebe8bfc97a1e96ba6d","after":"e10ea0a1ed5161c030767ee30f6a9dc55675327c","ref":"refs/heads/main","pushedAt":"2024-05-22T07:21:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Fix filling 0 [annotate]","shortMessageHtmlLink":"Fix filling 0 [annotate]"}},{"before":"08e2d9973fc1635cad2e075fde6e4a3bade929bd","after":"60790037b8b3c9259d3506ebe8bfc97a1e96ba6d","ref":"refs/heads/main","pushedAt":"2024-05-22T06:57:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Add Zulip/Float.lean [annotate]","shortMessageHtmlLink":"Add Zulip/Float.lean [annotate]"}},{"before":"5a3183d430bbc1eb3334f9a24e03a65ed6f45fad","after":"08e2d9973fc1635cad2e075fde6e4a3bade929bd","ref":"refs/heads/main","pushedAt":"2024-05-20T12:30:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Add `--toc` [annotate]","shortMessageHtmlLink":"Add <code>--toc</code> [annotate]"}},{"before":"fc726ca7b9eeffaa340d64f4ecd13f1809f6f6c1","after":"5a3183d430bbc1eb3334f9a24e03a65ed6f45fad","ref":"refs/heads/main","pushedAt":"2024-05-20T12:09:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Fix cp order [annotate]","shortMessageHtmlLink":"Fix cp order [annotate]"}},{"before":"5aba82f5997ec04f3e754fc01c3bb302ff772db2","after":"fc726ca7b9eeffaa340d64f4ecd13f1809f6f6c1","ref":"refs/heads/main","pushedAt":"2024-05-20T11:59:14.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Move some root files into Zulip and revamp annotation script [annotate]","shortMessageHtmlLink":"Move some root files into Zulip and revamp annotation script [annotate]"}},{"before":"fd4d1d47013ef6df4e9ff072c64770194e953eb4","after":"5aba82f5997ec04f3e754fc01c3bb302ff772db2","ref":"refs/heads/main","pushedAt":"2024-05-20T09:45:46.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Move examples into a package, and adjust accordingly [annotate]","shortMessageHtmlLink":"Move examples into a package, and adjust accordingly [annotate]"}},{"before":"dada6dbb1325739e4bdc62f3544a36ccc6bdf04f","after":"fd4d1d47013ef6df4e9ff072c64770194e953eb4","ref":"refs/heads/main","pushedAt":"2024-05-20T09:16:05.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Distinguish tests with warnings, and support `--verbose`","shortMessageHtmlLink":"Distinguish tests with warnings, and support <code>--verbose</code>"}},{"before":"93fbef523ec8b4a6faf1e4f2250d5acf46c00e86","after":"dada6dbb1325739e4bdc62f3544a36ccc6bdf04f","ref":"refs/heads/main","pushedAt":"2024-05-20T06:55:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"[annotate]","shortMessageHtmlLink":"[annotate]"}},{"before":"bd80303874aa410dd183ed522b49ae125737dc85","after":"93fbef523ec8b4a6faf1e4f2250d5acf46c00e86","ref":"refs/heads/main","pushedAt":"2024-05-20T06:46:50.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Use `lake test`","shortMessageHtmlLink":"Use <code>lake test</code>"}},{"before":"c27f1728eb118caa905a6afb8a1be025ca90bdcf","after":"bd80303874aa410dd183ed522b49ae125737dc85","ref":"refs/heads/main","pushedAt":"2024-05-13T05:04:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Improve index.lean for debugging","shortMessageHtmlLink":"Improve index.lean for debugging"}},{"before":"7b4755a8f8af6890a0a67960ce19512b800198bf","after":"c27f1728eb118caa905a6afb8a1be025ca90bdcf","ref":"refs/heads/main","pushedAt":"2024-05-13T04:58:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Add CurrentModule.lean [annotate]","shortMessageHtmlLink":"Add CurrentModule.lean [annotate]"}},{"before":"d68d6e33074d3cfb0ac9ebab5332b70197584471","after":"7b4755a8f8af6890a0a67960ce19512b800198bf","ref":"refs/heads/main","pushedAt":"2024-05-13T04:47:40.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Bump [annotate]","shortMessageHtmlLink":"Bump [annotate]"}},{"before":"4212481a11580acac678578f38b65e8b023892d3","after":"d68d6e33074d3cfb0ac9ebab5332b70197584471","ref":"refs/heads/main","pushedAt":"2024-05-12T03:38:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"utensil","name":"Utensil","path":"/utensil","primaryAvatarUrl":"https://github.com/avatars/u/64258?s=80&v=4"},"commit":{"message":"Update examples/Hierarchies.lean [annotate]","shortMessageHtmlLink":"Update examples/Hierarchies.lean [annotate]"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEZhzPQwA","startCursor":null,"endCursor":null}},"title":"Activity · utensil/lean-playground"}