{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":26978879,"defaultBranch":"master","name":"VST","ownerLogin":"PrincetonUniversity","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-11-21T21:36:24.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/1919273?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1714071984.0","currentOid":""},"activityList":{"items":[{"before":"221345c5cc7ba9a4582ba0079301eeb80606dff7","after":"ebccd3ec0b8fc7999cc0a0a1738b86b81ed170f4","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-21T20:17:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"halfway through own","shortMessageHtmlLink":"halfway through own"}},{"before":"8ebe9a6935df6b86c0da792aacdf168146d4030e","after":"221345c5cc7ba9a4582ba0079301eeb80606dff7","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-21T20:00:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"finished constrained with add Affine for P","shortMessageHtmlLink":"finished constrained with add Affine for P"}},{"before":"c340f6a2aeb82346f69cb7752cf1ff947daec5ed","after":"8ebe9a6935df6b86c0da792aacdf168146d4030e","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-21T19:52:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"WIP more on constrained.v","shortMessageHtmlLink":"WIP more on constrained.v"}},{"before":"59bfac8e832f15d6de104d57b662ee76f0ef1d32","after":"c340f6a2aeb82346f69cb7752cf1ff947daec5ed","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-21T18:48:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"owning a val is not necessarily affine","shortMessageHtmlLink":"owning a val is not necessarily affine"}},{"before":"491aca039cc4518e763deca1d3acb7f93c43bcde","after":"59bfac8e832f15d6de104d57b662ee76f0ef1d32","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-21T18:17:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"updated singleton","shortMessageHtmlLink":"updated singleton"}},{"before":"43b2ffa1ed4d6facd6425fafc0edb53354e3384d","after":"491aca039cc4518e763deca1d3acb7f93c43bcde","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-20T21:18:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"resolved Optional stuff","shortMessageHtmlLink":"resolved Optional stuff"}},{"before":"ba3bffe8c9d09b92bbdc12b7dce55ee6c000e648","after":"43b2ffa1ed4d6facd6425fafc0edb53354e3384d","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-20T21:17:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"Commented read_optionalO_case lemma","shortMessageHtmlLink":"Commented read_optionalO_case lemma"}},{"before":"4fe3a521fd5cbd34dda2c13d0ffe0d0ab49edd30","after":"ba3bffe8c9d09b92bbdc12b7dce55ee6c000e648","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-20T20:08:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"ported optional, tweaked basic definitions","shortMessageHtmlLink":"ported optional, tweaked basic definitions"}},{"before":"769a670a6349dbed0cc16ecdce6401b7c2da20da","after":"4fe3a521fd5cbd34dda2c13d0ffe0d0ab49edd30","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-20T01:31:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"Finished constrained.v and exist.v expect Optional stuff, since optional.v has not ported in VST.","shortMessageHtmlLink":"Finished constrained.v and exist.v expect Optional stuff, since optio…"}},{"before":"2ec7032026dd8df679c5fecbd180c0fbbfad2cdb","after":"769a670a6349dbed0cc16ecdce6401b7c2da20da","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-20T01:28:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"Finished all except , since opetion.v has not ported","shortMessageHtmlLink":"Finished all except , since opetion.v has not ported"}},{"before":"2926dc4e94c03c404f32d23cf88fd4ca56d726bb","after":"2ec7032026dd8df679c5fecbd180c0fbbfad2cdb","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-20T01:09:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"Finished all except , since opetion.v has not ported.","shortMessageHtmlLink":"Finished all except , since opetion.v has not ported."}},{"before":"53c27d238e16a43b1115efffee9e2b770f634520","after":"2926dc4e94c03c404f32d23cf88fd4ca56d726bb","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-20T00:31:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"Finished porting locked from RefinedC","shortMessageHtmlLink":"Finished porting locked from RefinedC"}},{"before":"ba7447665a98cb9e6e275f25df28e53dfc099838","after":"53c27d238e16a43b1115efffee9e2b770f634520","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-19T12:55:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"Finished all except the one lemma for locked","shortMessageHtmlLink":"Finished all except the one lemma for locked"}},{"before":"23858fe75edd48df19593f7b9b2865a95d9f0bb8","after":"ba7447665a98cb9e6e275f25df28e53dfc099838","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-19T04:15:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"almost done porting RefinedC's locked.","shortMessageHtmlLink":"almost done porting RefinedC's locked."}},{"before":"71824623aa71188ef4da3161513d78dd318b1c7b","after":"23858fe75edd48df19593f7b9b2865a95d9f0bb8","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-18T22:52:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"WIP in porting RefinedC's locked.","shortMessageHtmlLink":"WIP in porting RefinedC's locked."}},{"before":"fc0c7d942133ffdadaa06634b521f5a916b5648e","after":"71824623aa71188ef4da3161513d78dd318b1c7b","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-18T22:31:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ducthann","name":"Duc-Than Nguyen","path":"/ducthann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32882068?s=80&v=4"},"commit":{"message":"intial try to port RefinedC's locked.","shortMessageHtmlLink":"intial try to port RefinedC's locked."}},{"before":"bb6a413d76ea4d291c08b98e8afcc1a12c4354c6","after":"fc0c7d942133ffdadaa06634b521f5a916b5648e","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-18T16:47:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"Create overview.md","shortMessageHtmlLink":"Create overview.md"}},{"before":"350e50874201d3c08a06a601c046050699da1107","after":"0eed04f85ecfa9607d200b37aa69ac0fb39a1071","ref":"refs/heads/master","pushedAt":"2024-06-12T14:30:42.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #777 from SkySkimmer/make-profiling\n\nbuild: support PROFILING and TIMED like coq_makefile","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2346327411\" data-permission-text=\"Title is private\" data-url=\"https://github.com/PrincetonUniversity/VST/issues/777\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/PrincetonUniversity/VST/pull/777/hovercard\" href=\"https://github.com/PrincetonUniversity/VST/pull/777\">#777</a> from SkySkimmer/make-profiling"}},{"before":"05acc45cb7905b9a031c33d7fa717793b3afffb5","after":"bb6a413d76ea4d291c08b98e8afcc1a12c4354c6","ref":"refs/heads/vst_on_iris","pushedAt":"2024-06-05T14:36:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"Update ivst.md","shortMessageHtmlLink":"Update ivst.md"}},{"before":"411744beb4df2def4e025e0eeec7578df971c6a8","after":"350e50874201d3c08a06a601c046050699da1107","ref":"refs/heads/master","pushedAt":"2024-05-31T11:40:42.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #774 from ppedrot/abstract-functor-lemmas\n\nWrap functor facts in abstract lemmas.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2317784408\" data-permission-text=\"Title is private\" data-url=\"https://github.com/PrincetonUniversity/VST/issues/774\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/PrincetonUniversity/VST/pull/774/hovercard\" href=\"https://github.com/PrincetonUniversity/VST/pull/774\">#774</a> from ppedrot/abstract-functor-lemmas"}},{"before":"56e6886288918f1b78ad53dd3dcdb1a58a9916cb","after":"411744beb4df2def4e025e0eeec7578df971c6a8","ref":"refs/heads/master","pushedAt":"2024-05-30T20:22:45.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #771 from PrincetonUniversity/funcptr_validpointer\n\nChanged definition of valid_pointer' wrt locations with PURE resource…","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2264322814\" data-permission-text=\"Title is private\" data-url=\"https://github.com/PrincetonUniversity/VST/issues/771\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/PrincetonUniversity/VST/pull/771/hovercard\" href=\"https://github.com/PrincetonUniversity/VST/pull/771\">#771</a> from PrincetonUniversity/funcptr_validpointer"}},{"before":"7bfc4ac026b516914540ba98ed9a9db190e0aed0","after":"05acc45cb7905b9a031c33d7fa717793b3afffb5","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-22T18:24:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"proved typing rules for int ops","shortMessageHtmlLink":"proved typing rules for int ops"}},{"before":"ab5c00b29029e6f3b3467f0d32687c2c2c398e0a","after":"7bfc4ac026b516914540ba98ed9a9db190e0aed0","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-21T15:59:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"progress on int ops","shortMessageHtmlLink":"progress on int ops"}},{"before":"c3df6881b671eadb98fc3fd5716970f803833727","after":"ab5c00b29029e6f3b3467f0d32687c2c2c398e0a","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-19T14:48:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"a bit more progress on lithium instance","shortMessageHtmlLink":"a bit more progress on lithium instance"}},{"before":"a02cb908973ac457f7d3411be984a9fe74859f38","after":"c3df6881b671eadb98fc3fd5716970f803833727","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-14T17:44:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Remove coq 8.18 from CI, no need to support that in this branch","shortMessageHtmlLink":"Remove coq 8.18 from CI, no need to support that in this branch"}},{"before":"4e34ca84c3a2e8f9fb60bc3f7fd7f56f361b9eb5","after":"a02cb908973ac457f7d3411be984a9fe74859f38","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-14T14:24:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"each closed_lemma takes only the implicit arguments it really needs, which makes 'auto with closed' work better in edge cases","shortMessageHtmlLink":"each closed_lemma takes only the implicit arguments it really needs, …"}},{"before":"0acc02a7a3d1c6901e443fd388d3706ee522a429","after":"4e34ca84c3a2e8f9fb60bc3f7fd7f56f361b9eb5","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-13T17:45:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Update ora submodule; carefully suppress warnings; fix a couple of broken proofs.","shortMessageHtmlLink":"Update ora submodule; carefully suppress warnings; fix a couple of br…"}},{"before":"d44b24889778c772e6164de40a601a1a2d4def53","after":"0acc02a7a3d1c6901e443fd388d3706ee522a429","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-12T19:16:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"fix DrySafe proofs","shortMessageHtmlLink":"fix DrySafe proofs"}},{"before":"0bda31abfc9b42baf647ef9af8bafefbac3e3a20","after":"d44b24889778c772e6164de40a601a1a2d4def53","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-11T21:08:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"fix implicits in examples","shortMessageHtmlLink":"fix implicits in examples"}},{"before":"605c90ecff91d3f9eff47186d2a5908b0e1e112e","after":"0bda31abfc9b42baf647ef9af8bafefbac3e3a20","ref":"refs/heads/vst_on_iris","pushedAt":"2024-05-11T19:06:31.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mansky1","name":"William Mansky","path":"/mansky1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/154122?s=80&v=4"},"commit":{"message":"Merge branch 'vst_on_iris' of https://github.com/PrincetonUniversity/VST into vst_on_iris","shortMessageHtmlLink":"Merge branch 'vst_on_iris' of <a href=\"https://github.com/PrincetonUniversity/VST\">https://github.com/PrincetonUniversity/VST</a>"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEa_AQ2wA","startCursor":null,"endCursor":null}},"title":"Activity · PrincetonUniversity/VST"}