{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":106680408,"defaultBranch":"main","name":"bolts","ownerLogin":"epfl-lara","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2017-10-12T10:48:10.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/3035238?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1724662426.0","currentOid":""},"activityList":{"items":[{"before":"1b4745d851ee7de068fc7fb4536d275b4f075073","after":"b2094225386d74654bc781f526ac2f5e54c42c73","ref":"refs/heads/main","pushedAt":"2024-09-09T16:24:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Add a verified HashSet implementation + refactor package name of map + add script (#106)\n\n* renaming of package in the maps\r\n\r\n* add mutable sets project and start working on the implementation\r\n\r\n* working on hashset\r\n\r\n* add new lemmas about getKeysList to reuse in the set\r\n\r\n* working on listmap to use it for hashset\r\n\r\n* finished the Set\r\n\r\n* add a few properties\r\n\r\n* remove benchmark results\r\n\r\n* restore deleted file\r\n\r\n* change name package in lexers\r\n\r\n* rename map package in caching functions\r\n\r\n* finish renaming map package to map\r\n\r\n* Add script that runs all verify.sh scripts\r\n\r\n* scala version 3.5.0 for sbt projects\r\n\r\n* fail if one fails\r\n\r\n* config + remove useless file\r\n\r\n* add main class + method to get an empty set\r\n\r\n* filter hashset to not verify the maps\r\n\r\n* make it compile with SBT and add a Main\r\n\r\n* rename interfaces to avoid confusion with immutable structures\r\n\r\n* remove benchmark result files\r\n\r\n* add $1 at the end of verify.sh scripts to be able to pass --compact when running tests\r\n\r\n* add a success message in run-tests so that we can export the log to PR as long as the CI is dead\r\n\r\n* add unfold to make ConstFold verify\r\n\r\n* message out of the loop\r\n\r\n* typo in script\r\n\r\n* add mutablesets in the tests nightly\r\n\r\n* error in verify script for set + error in run-test scripts making all passing\r\n\r\n* run all tests once\r\n\r\n* run on laraquad2\r\n\r\n* remove laraquad2 requirement\r\n\r\n* with VCs admit back\r\n\r\n* remove cache","shortMessageHtmlLink":"Add a verified HashSet implementation + refactor package name of map …"}},{"before":"3e965c6788c3331e95e4840192cfec08668e8b4e","after":"1b4745d851ee7de068fc7fb4536d275b4f075073","ref":"refs/heads/main","pushedAt":"2024-09-09T13:31:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Move sbt installation to install script instead of yml","shortMessageHtmlLink":"Move sbt installation to install script instead of yml"}},{"before":"c0cd6ea73a82f92180603c69379ca5039bd4ceb2","after":"3e965c6788c3331e95e4840192cfec08668e8b4e","ref":"refs/heads/main","pushedAt":"2024-09-09T12:29:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"CI: tweaks to verbosity","shortMessageHtmlLink":"CI: tweaks to verbosity"}},{"before":"cf392b52da5d594a611eb2f6f45d1221115feb76","after":"c0cd6ea73a82f92180603c69379ca5039bd4ceb2","ref":"refs/heads/main","pushedAt":"2024-09-09T12:19:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"CI: Report sbt version and add shorten download progress","shortMessageHtmlLink":"CI: Report sbt version and add shorten download progress"}},{"before":"13be6ea2cd367f59078f59455ab01d0962abfd0d","after":"cf392b52da5d594a611eb2f6f45d1221115feb76","ref":"refs/heads/main","pushedAt":"2024-09-09T12:07:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Update README.md with CI status badge","shortMessageHtmlLink":"Update README.md with CI status badge"}},{"before":"f7116ed40a89a9d49ac103451feb31354da336f3","after":"13be6ea2cd367f59078f59455ab01d0962abfd0d","ref":"refs/heads/main","pushedAt":"2024-09-08T12:10:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Download sbt in CI","shortMessageHtmlLink":"Download sbt in CI"}},{"before":"be4bf04a0cc638f9ecdea6520243d4101fff8a62","after":"f7116ed40a89a9d49ac103451feb31354da336f3","ref":"refs/heads/main","pushedAt":"2024-09-06T11:50:22.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"run stainless with admit VCs in the CI","shortMessageHtmlLink":"run stainless with admit VCs in the CI"}},{"before":"1fce69f6adebd1878cf97218885c068076d7305c","after":"be4bf04a0cc638f9ecdea6520243d4101fff8a62","ref":"refs/heads/main","pushedAt":"2024-09-06T07:12:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"samuelchassot","name":"Samuel Chassot","path":"/samuelchassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14821693?s=80&v=4"},"commit":{"message":"Fix CI (#110)","shortMessageHtmlLink":"Fix CI (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2509645979\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/bolts/issues/110\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/bolts/pull/110/hovercard\" href=\"https://github.com/epfl-lara/bolts/pull/110\">#110</a>)"}},{"before":"f25137c4e62d0d6bbd030f7c1c0167c414d09fc8","after":"1fce69f6adebd1878cf97218885c068076d7305c","ref":"refs/heads/main","pushedAt":"2024-09-06T06:36:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"samuelchassot","name":"Samuel Chassot","path":"/samuelchassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14821693?s=80&v=4"},"commit":{"message":"Typo in script","shortMessageHtmlLink":"Typo in script"}},{"before":"f58cc7f32d9db5ba847ddae48f1576946627a812","after":"f25137c4e62d0d6bbd030f7c1c0167c414d09fc8","ref":"refs/heads/main","pushedAt":"2024-09-06T06:31:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"samuelchassot","name":"Samuel Chassot","path":"/samuelchassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14821693?s=80&v=4"},"commit":{"message":"missing recursive clone","shortMessageHtmlLink":"missing recursive clone"}},{"before":"bcbc6f8b5e11bb37957f9e5337c734067bdec96e","after":"f58cc7f32d9db5ba847ddae48f1576946627a812","ref":"refs/heads/main","pushedAt":"2024-09-06T06:19:33.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"samuelchassot","name":"Samuel Chassot","path":"/samuelchassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14821693?s=80&v=4"},"commit":{"message":"add a CI (#109)","shortMessageHtmlLink":"add a CI (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2509612769\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/bolts/issues/109\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/bolts/pull/109/hovercard\" href=\"https://github.com/epfl-lara/bolts/pull/109\">#109</a>)"}},{"before":"57baf5e85193d012cc48b8b1f42b5fcd313969dc","after":"bcbc6f8b5e11bb37957f9e5337c734067bdec96e","ref":"refs/heads/main","pushedAt":"2024-08-30T19:47:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Indicate current date when running a test","shortMessageHtmlLink":"Indicate current date when running a test"}},{"before":"7ff3fe1ce5201e921e12b5653aec564a92ba8073","after":"57baf5e85193d012cc48b8b1f42b5fcd313969dc","ref":"refs/heads/main","pushedAt":"2024-08-28T14:43:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Int to BigInt for ConstFold","shortMessageHtmlLink":"Int to BigInt for ConstFold"}},{"before":"6d088a9376d51d8a6d4af192596d21cdefbaf9be","after":"7ff3fe1ce5201e921e12b5653aec564a92ba8073","ref":"refs/heads/main","pushedAt":"2024-08-28T14:12:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"use vc cache more","shortMessageHtmlLink":"use vc cache more"}},{"before":"c4e5c5970aa5616685ff5da4a3ae6b78ee415b67","after":null,"ref":"refs/heads/const-fold","pushedAt":"2024-08-26T08:53:46.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"}},{"before":"a85089a8eafeefd7277a36748412fa2f20bbcd7f","after":null,"ref":"refs/heads/vk/dispenser-conf","pushedAt":"2024-08-26T08:50:26.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"}},{"before":"9f33e05099838ecd6a8a755c0e864d78227e36d7","after":null,"ref":"refs/heads/vk/dispenser-conf2","pushedAt":"2024-08-26T08:50:23.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"}},{"before":"8ef1a18a020bf42e6d6107f8d7b6c070947f4755","after":"6d088a9376d51d8a6d4af192596d21cdefbaf9be","ref":"refs/heads/main","pushedAt":"2024-08-26T08:29:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Dispenser with --solvers=eval,smt-cvc5. Fixed to .holdsFrom","shortMessageHtmlLink":"Dispenser with --solvers=eval,smt-cvc5. Fixed to .holdsFrom"}},{"before":null,"after":"9f33e05099838ecd6a8a755c0e864d78227e36d7","ref":"refs/heads/vk/dispenser-conf2","pushedAt":"2024-08-26T08:24:09.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Dispenser with --solvers=eval,smt-cvc5. Fixed to .holdsFrom","shortMessageHtmlLink":"Dispenser with --solvers=eval,smt-cvc5. Fixed to .holdsFrom"}},{"before":null,"after":"8055565b525ce77603a70b31a00fecde81e891ae","ref":"refs/heads/vk/encoders","pushedAt":"2024-08-23T22:30:32.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Simple encoders and decoders without traits and type encoding","shortMessageHtmlLink":"Simple encoders and decoders without traits and type encoding"}},{"before":"28667b596e80548f507bf46854af3d3853190976","after":"8ef1a18a020bf42e6d6107f8d7b6c070947f4755","ref":"refs/heads/main","pushedAt":"2024-08-23T15:13:13.000Z","pushType":"pr_merge","commitsCount":7,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"migration","shortMessageHtmlLink":"migration"}},{"before":"04904d055c95e4c5801476418dfa5f5fb9cdca2b","after":"28667b596e80548f507bf46854af3d3853190976","ref":"refs/heads/main","pushedAt":"2024-08-16T08:01:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"samuelchassot","name":"Samuel Chassot","path":"/samuelchassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14821693?s=80&v=4"},"commit":{"message":"Update verify.sh","shortMessageHtmlLink":"Update verify.sh"}},{"before":"5460f63f614acea76b2f864a4fe7cda22b59f8f8","after":"04904d055c95e4c5801476418dfa5f5fb9cdca2b","ref":"refs/heads/main","pushedAt":"2024-08-15T07:21:50.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"samuelchassot","name":"Samuel Chassot","path":"/samuelchassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14821693?s=80&v=4"},"commit":{"message":"typo in path (#105)","shortMessageHtmlLink":"typo in path (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2467556034\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/bolts/issues/105\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/bolts/pull/105/hovercard\" href=\"https://github.com/epfl-lara/bolts/pull/105\">#105</a>)"}},{"before":"732e5d5731ec442b062ababdc8bded2309761e0b","after":"5460f63f614acea76b2f864a4fe7cda22b59f8f8","ref":"refs/heads/main","pushedAt":"2024-08-14T18:48:09.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"cleanup Lexer and regex, add them to the nightly (#104)","shortMessageHtmlLink":"cleanup Lexer and regex, add them to the nightly (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2466216546\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/bolts/issues/104\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/bolts/pull/104/hovercard\" href=\"https://github.com/epfl-lara/bolts/pull/104\">#104</a>)"}},{"before":"480ee123700e1dcb1a09eef0d9b90db9938bcb4b","after":"732e5d5731ec442b062ababdc8bded2309761e0b","ref":"refs/heads/main","pushedAt":"2024-08-13T13:00:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Adding memoisation to regex matching, and a simplification function proven to be sound (#102)\n\n* add sbt project with plugin\r\n\r\n* move regex to an sbt project\r\n\r\n* original version\r\n\r\n* working on the memoisation\r\n\r\n* not working\r\n\r\n* add longMap + work on cache\r\n\r\n* for now issue with illegal capturing\r\n\r\n* to specific, not working but almost\r\n\r\n* working on memoised regex\r\n\r\n* working\r\n\r\n* cached version proven\r\n\r\n* working examples\r\n\r\n* new hashmap without ordering\r\n\r\n* add new lemmas in ListMaps for forall\r\n\r\n* Formally verified cache for regex\r\n\r\n* add removeUselessConcat simplification for regex + equivalence proof\r\n\r\n* add a simplification function that is sound\r\n\r\n* working on regex\r\n\r\n* as symlink\r\n\r\n* ensuring as method and not infix\r\n\r\n---------\r\n\r\nCo-authored-by: Samuel Chassot <samuel@tsf-476-wpa-1-098.epfl.ch>","shortMessageHtmlLink":"Adding memoisation to regex matching, and a simplification function p…"}},{"before":"b4fd45b76ced4b62fc181f09ddc9c2337337e973","after":"480ee123700e1dcb1a09eef0d9b90db9938bcb4b","ref":"refs/heads/main","pushedAt":"2024-08-13T12:55:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Using ignore models and cvc5 for now on dispenser (#103)","shortMessageHtmlLink":"Using ignore models and cvc5 for now on dispenser (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2463290263\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/bolts/issues/103\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/bolts/pull/103/hovercard\" href=\"https://github.com/epfl-lara/bolts/pull/103\">#103</a>)"}},{"before":null,"after":"a85089a8eafeefd7277a36748412fa2f20bbcd7f","ref":"refs/heads/vk/dispenser-conf","pushedAt":"2024-08-13T12:54:09.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Using ignore models and cvc5 for now on dispenser","shortMessageHtmlLink":"Using ignore models and cvc5 for now on dispenser"}},{"before":"895aed1a34ecb80fac47fe9c8fc172f9d7baf26f","after":"b4fd45b76ced4b62fc181f09ddc9c2337337e973","ref":"refs/heads/main","pushedAt":"2024-08-09T07:38:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Add a trait interface to the `MutableLongMap` as a first step towards modular proofs (#96)\n\n* add trait interface\r\n\r\n* sealed in the same file\r\n\r\n* remove file from verify.sh\r\n\r\n* non sealed\r\n\r\n* trait for mutable longmap\r\n\r\n* trait for hashtable\r\n\r\n* error in spec\r\n\r\n* error in spec\r\n\r\n* invariant list\r\n\r\n* add post codnition to abstract map function to ease verification\r\n\r\n* add post codnition to abstract map function to ease verification","shortMessageHtmlLink":"Add a trait interface to the <code>MutableLongMap</code> as a first step towards…"}},{"before":"8d770dc9aef7dd9105c60fbcf1db6fb25fcabbc5","after":"f10df7d68a55aa3097f22ec97a21366b10a8f7ac","ref":"refs/heads/vk/abstract-classes","pushedAt":"2024-08-05T20:32:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Also made toSet non-abstract from the point of dotty","shortMessageHtmlLink":"Also made toSet non-abstract from the point of dotty"}},{"before":"895aed1a34ecb80fac47fe9c8fc172f9d7baf26f","after":"8d770dc9aef7dd9105c60fbcf1db6fb25fcabbc5","ref":"refs/heads/vk/abstract-classes","pushedAt":"2024-08-05T20:24:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Example of using abstract classes. Requires stainless to detect when methods are abstract by way of containing ??? symbol","shortMessageHtmlLink":"Example of using abstract classes. Requires stainless to detect when …"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0wOVQxNjoyNDo0NC4wMDAwMDBazwAAAASxH__z","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOC0wNVQyMDoyNDo1My4wMDAwMDBazwAAAASSav7B"}},"title":"Activity · epfl-lara/bolts"}