{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":593906274,"defaultBranch":"master","name":"cakeml","ownerLogin":"Gordon-Sau","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2023-01-27T05:29:34.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/66369887?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1710816893.0","currentOid":""},"activityList":{"items":[{"before":"6dbde1638d8954eb5b8977247e781c0e7f92246f","after":"62d6b6509f4f15779b7bcb31490eb4ac9333d41a","ref":"refs/heads/master","pushedAt":"2024-03-25T01:10:09.000Z","pushType":"push","commitsCount":508,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"Merge pull request #986 from ShunyaoLiang/scope\n\nAdd scope-checking for Pancake","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2194165372\" data-permission-text=\"Title is private\" data-url=\"https://github.com/CakeML/cakeml/issues/986\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/CakeML/cakeml/pull/986/hovercard\" href=\"https://github.com/CakeML/cakeml/pull/986\">CakeML#986</a> from ShunyaoLiang/scope"}},{"before":null,"after":"af62b90c6c6732520e8a77e253206d44c37d274d","ref":"refs/heads/pancake_shmem_syntax_new","pushedAt":"2024-03-19T02:54:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: add translation for conv_ffi_ident to from_pancake(32|64)ProgScript.sml","shortMessageHtmlLink":"pancake_shmem_syntax: add translation for conv_ffi_ident to from_panc…"}},{"before":"1cd69debc8c2d58925368d2c50d90a488f70c4c7","after":"af62b90c6c6732520e8a77e253206d44c37d274d","ref":"refs/heads/pancake_shmem_syntax","pushedAt":"2024-02-04T01:13:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: add translation for conv_ffi_ident to from_pancake(32|64)ProgScript.sml","shortMessageHtmlLink":"pancake_shmem_syntax: add translation for conv_ffi_ident to from_panc…"}},{"before":"40a79f4fd0d4050493a86c2a81d85786594ef5dc","after":"1cd69debc8c2d58925368d2c50d90a488f70c4c7","ref":"refs/heads/pancake_shmem_syntax","pushedAt":"2024-02-03T11:26:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: prove the preconditions for get_keyword to fix pancake_lexProg","shortMessageHtmlLink":"pancake_shmem_syntax: prove the preconditions for get_keyword to fix …"}},{"before":"65c8fcb6cacadfcc0e2d1399ce399d42c097d2ed","after":"40a79f4fd0d4050493a86c2a81d85786594ef5dc","ref":"refs/heads/pancake_shmem_syntax","pushedAt":"2024-01-29T11:35:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: implement a simpler way to parse shared memory instruction","shortMessageHtmlLink":"pancake_shmem_syntax: implement a simpler way to parse shared memory …"}},{"before":"07ed97951eb8101cdf930a28fefc642e87aacf3a","after":"65c8fcb6cacadfcc0e2d1399ce399d42c097d2ed","ref":"refs/heads/pancake_shmem_syntax","pushedAt":"2024-01-28T21:55:09.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: add example for shared memory instructions","shortMessageHtmlLink":"pancake_shmem_syntax: add example for shared memory instructions"}},{"before":"2a2ea93a104e80e5b12abf88adc8130c0d76e60a","after":"07ed97951eb8101cdf930a28fefc642e87aacf3a","ref":"refs/heads/pancake_shmem_syntax","pushedAt":"2024-01-28T21:07:39.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: fix concrete examples for changes in syntax for laod/store and ffi calls","shortMessageHtmlLink":"pancake_shmem_syntax: fix concrete examples for changes in syntax for…"}},{"before":"dac1ba1297245b6280e150f2673907d22fd20764","after":"2a2ea93a104e80e5b12abf88adc8130c0d76e60a","ref":"refs/heads/pancake_shmem_syntax","pushedAt":"2024-01-28T20:22:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: update Ptree conversion for shared memory","shortMessageHtmlLink":"pancake_shmem_syntax: update Ptree conversion for shared memory"}},{"before":null,"after":"dac1ba1297245b6280e150f2673907d22fd20764","ref":"refs/heads/pancake_shmem_syntax","pushedAt":"2024-01-28T19:25:27.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake_shmem_syntax: update PEG for shared memory","shortMessageHtmlLink":"pancake_shmem_syntax: update PEG for shared memory"}},{"before":"8a6be761fdcb3972113aee07c168e600dbfeabc1","after":"324347695c32eb24b717355ae122dc50d8fd7c58","ref":"refs/heads/pancake_shmem_parser","pushedAt":"2024-01-28T18:36:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"panckae_shmem_syntac: update panPEG","shortMessageHtmlLink":"panckae_shmem_syntac: update panPEG"}},{"before":"6a6ceafba86179cd5be5976e0c9efc55bb0c44cf","after":"6dbde1638d8954eb5b8977247e781c0e7f92246f","ref":"refs/heads/master","pushedAt":"2023-12-26T02:59:43.000Z","pushType":"push","commitsCount":360,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"Fix for change in HOL","shortMessageHtmlLink":"Fix for change in HOL"}},{"before":"1507e5406e761c7b2231b21dec1d36f8c69ca23f","after":"8a6be761fdcb3972113aee07c168e600dbfeabc1","ref":"refs/heads/pancake_shmem_parser","pushedAt":"2023-12-26T02:05:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"pancake new syntax: remove HashT","shortMessageHtmlLink":"pancake new syntax: remove HashT"}},{"before":"adf220344f9169aaf615ed7448122f21d8c694fd","after":"1507e5406e761c7b2231b21dec1d36f8c69ca23f","ref":"refs/heads/pancake_shmem_parser","pushedAt":"2023-12-16T14:28:47.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"shmem: update lexer for shared memory syntax","shortMessageHtmlLink":"shmem: update lexer for shared memory syntax"}},{"before":null,"after":"adf220344f9169aaf615ed7448122f21d8c694fd","ref":"refs/heads/pancake_shmem_parser","pushedAt":"2023-12-16T06:31:08.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"shmem: update lexer for shared memory syntax","shortMessageHtmlLink":"shmem: update lexer for shared memory syntax"}},{"before":"0dd162cc75b402b8253e96be62388e683a6c0795","after":"7c5315023d8490d7dac06904403ddac11dad5fac","ref":"refs/heads/share_mem","pushedAt":"2023-11-20T04:31:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"lab_to_target: change compile_lab to ensure that it raise Nothing when MappedRead/Write is found","shortMessageHtmlLink":"lab_to_target: change compile_lab to ensure that it raise Nothing whe…"}},{"before":"c2fdeac2f1a43d473109e9a351faf9c3c13f9890","after":"0dd162cc75b402b8253e96be62388e683a6c0795","ref":"refs/heads/share_mem","pushedAt":"2023-11-16T22:23:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"share_mem: data_to_word: add syntactic assumption about the ffi names","shortMessageHtmlLink":"share_mem: data_to_word: add syntactic assumption about the ffi names"}},{"before":"7868ed758d7ba34d1262b8199e20586baac814b8","after":"c2fdeac2f1a43d473109e9a351faf9c3c13f9890","ref":"refs/heads/share_mem","pushedAt":"2023-11-13T08:22:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"data_to_wordProof: add assumption that the program never contains the ffi names \"MappedRead\" or \"MappedWrite\"","shortMessageHtmlLink":"data_to_wordProof: add assumption that the program never contains the…"}},{"before":"8507758feb3bb1dc4bcc36e7f4e835f10ad644ec","after":"7868ed758d7ba34d1262b8199e20586baac814b8","ref":"refs/heads/share_mem","pushedAt":"2023-11-03T08:46:35.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"data_to_word_assign: fix data_to_word_assign proof (add the assumption that ffi names cannot be \"MappedRead\" or \"MappedWrite\" for assign_thm)","shortMessageHtmlLink":"data_to_word_assign: fix data_to_word_assign proof (add the assumptio…"}},{"before":"239e64514f8121f5863bf0eded31b3e33fccca78","after":"8507758feb3bb1dc4bcc36e7f4e835f10ad644ec","ref":"refs/heads/share_mem","pushedAt":"2023-10-24T12:46:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"word_allocProof: complete ssa_cc_trans_correct proof","shortMessageHtmlLink":"word_allocProof: complete ssa_cc_trans_correct proof"}},{"before":"cf4a5284b3496b750ec229c66b87fd154799b6b6","after":"239e64514f8121f5863bf0eded31b3e33fccca78","ref":"refs/heads/share_mem","pushedAt":"2023-10-21T06:12:27.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"word_allocProof: work in progress","shortMessageHtmlLink":"word_allocProof: work in progress"}},{"before":"287c3ddd0ca2d1cd004c05b2935e1c267d2a0fc2","after":"cf4a5284b3496b750ec229c66b87fd154799b6b6","ref":"refs/heads/share_mem","pushedAt":"2023-10-20T00:50:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"word_alloc: add ShareInst in register allocation","shortMessageHtmlLink":"word_alloc: add ShareInst in register allocation"}},{"before":"98b8c60544eeba223b9f91c24d57d7e5af73f6a6","after":"287c3ddd0ca2d1cd004c05b2935e1c267d2a0fc2","ref":"refs/heads/share_mem","pushedAt":"2023-10-17T03:14:19.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"labProps: move no_share_mem_inst","shortMessageHtmlLink":"labProps: move no_share_mem_inst"}},{"before":"a2799e14c49df5a39f2379288b15ef524b518f4a","after":"287c3ddd0ca2d1cd004c05b2935e1c267d2a0fc2","ref":"refs/heads/share_mem_v4","pushedAt":"2023-10-17T03:13:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"labProps: move no_share_mem_inst","shortMessageHtmlLink":"labProps: move no_share_mem_inst"}},{"before":"56f4137c9f9047ba41b6815cded1bc83e4a053f6","after":"a2799e14c49df5a39f2379288b15ef524b518f4a","ref":"refs/heads/share_mem_v4","pushedAt":"2023-10-16T06:34:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"prove backendProof","shortMessageHtmlLink":"prove backendProof"}},{"before":null,"after":"56f4137c9f9047ba41b6815cded1bc83e4a053f6","ref":"refs/heads/share_mem_v4","pushedAt":"2023-10-05T06:54:15.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"lab_to_targetProof: complete the proof for semantics_compile withe no_share_mem_inst assumption for compiler_oracle","shortMessageHtmlLink":"lab_to_targetProof: complete the proof for semantics_compile withe no…"}},{"before":null,"after":"339ca4b811ca81c06202cd148fc3d293bc34cee0","ref":"refs/heads/share_mem_v3","pushedAt":"2023-09-22T06:24:58.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"fixing compile_oracle: the cfg.ffi_names (ffi_names created by coracle 0) may not be equal to mc_conf.ffi_names","shortMessageHtmlLink":"fixing compile_oracle: the cfg.ffi_names (ffi_names created by coracl…"}},{"before":"beab734fe68e206b58e2b8928d0020cc60b433af","after":"98b8c60544eeba223b9f91c24d57d7e5af73f6a6","ref":"refs/heads/share_mem","pushedAt":"2023-09-22T06:24:39.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"backendProof: fixing broken lemmas","shortMessageHtmlLink":"backendProof: fixing broken lemmas"}},{"before":"29581cf0d9058961b845b805bc1f9a552c7cd31a","after":"beab734fe68e206b58e2b8928d0020cc60b433af","ref":"refs/heads/share_mem","pushedAt":"2023-09-13T17:05:21.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"backendProof: fixing broken lemmas","shortMessageHtmlLink":"backendProof: fixing broken lemmas"}},{"before":"944f7ebaa87c1bb62c37d9cc53585da4ca89d7e0","after":"29581cf0d9058961b845b805bc1f9a552c7cd31a","ref":"refs/heads/share_mem","pushedAt":"2023-09-13T16:56:55.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"backendProof: fixing broken lemmas","shortMessageHtmlLink":"backendProof: fixing broken lemmas"}},{"before":"29239f64e930fe8213042dad90cb0b846f47f250","after":"944f7ebaa87c1bb62c37d9cc53585da4ca89d7e0","ref":"refs/heads/share_mem","pushedAt":"2023-09-13T16:32:08.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"backendProof: fixing broken lemmas","shortMessageHtmlLink":"backendProof: fixing broken lemmas"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEHiDyHQA","startCursor":null,"endCursor":null}},"title":"Activity · Gordon-Sau/cakeml"}