{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":339542872,"defaultBranch":"main","name":"carcara","ownerLogin":"ufmg-smite","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-02-16T22:01:03.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/93679751?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1718008188.0","currentOid":""},"activityList":{"items":[{"before":"97ca7926218f2a18a2a5c31caf56f915c9b8a15f","after":"224058116c0f0a07516b8a90790e1c9e30affdbd","ref":"refs/heads/journal-paper","pushedAt":"2024-06-20T08:26:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Fix `subproof` unit test","shortMessageHtmlLink":"Fix <code>subproof</code> unit test"}},{"before":"d04b5e6427964deae2b6684425e1785a58afec1d","after":"97ca7926218f2a18a2a5c31caf56f915c9b8a15f","ref":"refs/heads/journal-paper","pushedAt":"2024-06-20T08:20:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Fix clippy lints","shortMessageHtmlLink":"Fix clippy lints"}},{"before":"d5bc6f2ab802d3265844bbb5d6f081ed90232fac","after":"d04b5e6427964deae2b6684425e1785a58afec1d","ref":"refs/heads/journal-paper","pushedAt":"2024-06-20T08:10:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Deal with GMP constants when elaborating polyequal","shortMessageHtmlLink":"Deal with GMP constants when elaborating polyequal"}},{"before":"937cb9c36825ed5aa230382f1de51892c432f9f7","after":"d5bc6f2ab802d3265844bbb5d6f081ed90232fac","ref":"refs/heads/journal-paper","pushedAt":"2024-06-13T19:51:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"Fixes related to printing valid SMT-LIB for calling external solvers","shortMessageHtmlLink":"Fixes related to printing valid SMT-LIB for calling external solvers"}},{"before":"c4a8c719269e53469134d9eef03d7444619cac00","after":"937cb9c36825ed5aa230382f1de51892c432f9f7","ref":"refs/heads/journal-paper","pushedAt":"2024-06-12T17:17:46.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"Merge branch 'elab-simp' into journal-paper","shortMessageHtmlLink":"Merge branch 'elab-simp' into journal-paper"}},{"before":"7ce9e9ebd5f7782d9e3a26103f7bfb2fda6dfcec","after":"c4a8c719269e53469134d9eef03d7444619cac00","ref":"refs/heads/journal-paper","pushedAt":"2024-06-12T15:14:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Measure duration of each pipeline step","shortMessageHtmlLink":"Measure duration of each pipeline step"}},{"before":"3c66b18f4a555abce8d9fd0fe4dec137093565c3","after":"7ce9e9ebd5f7782d9e3a26103f7bfb2fda6dfcec","ref":"refs/heads/journal-paper","pushedAt":"2024-06-12T10:10:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Implement premise rotation in resolution uncrowding","shortMessageHtmlLink":"Implement premise rotation in resolution uncrowding"}},{"before":"8e12e6a8e444e7eb0f3de47c963e265d9a0ac1c6","after":"02b3a8a8aa65d4ed5497a37559ac3bba34d4ac38","ref":"refs/heads/main","pushedAt":"2024-06-12T07:15:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"fix prelude printing\n\nThe names are symbols that can be quoted.","shortMessageHtmlLink":"fix prelude printing"}},{"before":"3d192247c75db5ee23aca5b91c2c62c95f54a40b","after":"3c66b18f4a555abce8d9fd0fe4dec137093565c3","ref":"refs/heads/journal-paper","pushedAt":"2024-06-11T15:41:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Refactor resolution uncrowding module","shortMessageHtmlLink":"Refactor resolution uncrowding module"}},{"before":"fe9c3c638c28697ea50673bbc6e8c46b09b49e4b","after":"3d192247c75db5ee23aca5b91c2c62c95f54a40b","ref":"refs/heads/journal-paper","pushedAt":"2024-06-11T13:32:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Adapt `generate-benchmarks.sh` to also use cvc5","shortMessageHtmlLink":"Adapt <code>generate-benchmarks.sh</code> to also use cvc5"}},{"before":"144f04551c0632235e83c5d026e4c6353e7d5327","after":"fe9c3c638c28697ea50673bbc6e8c46b09b49e4b","ref":"refs/heads/journal-paper","pushedAt":"2024-06-10T13:32:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Fix bug in elaborator pipeline","shortMessageHtmlLink":"Fix bug in elaborator pipeline"}},{"before":null,"after":"5fc5e47082acd756d914891f53ae7bd384c81723","ref":"refs/heads/journal-paper-squashed","pushedAt":"2024-06-10T08:29:48.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Add graph-based representation for proof\n\nAdd conversion methods for `ProofNode`\n\nOrganize `ast` module\n\nStore depth in node itself\n\nDon't store duplicate outbound premises\n\nRemove unnecessary cloning in `proof_node_to_list`\n\nTest node proof conversion in integration tests\n\nFix lint\n\nMove old elaborator to separate module\n\nAdd proof-of-concept functional elaborator\n\nRecompute outbound premises when elaborating\n\nMigrate \"eq_transitive\" elaboration to new elaborator\n\nAdd struct to help create new step ids\n\nMigrate `refl` elaboration to new elaborator\n\nMigrate `assume` elaboration to new elaborator\n\nMove resolution utilities to separate file\n\nFix visibility leaking error\n\nMigrate `resolution` elaboration to new elaborator\n\nMigrate `lia_generic` elaboration to new elaborator\n\nUse new elaborator in public API\n\nRemove old elaborator\n\nChange API of node proof conversion\n\nFix slice command\n\nMove benchmarks to new elaborator\n\nRename `ResolutionTerm` to `Literal`\n\nAdd function to uncrowd resolution steps\n\nAdd tests\n\nIntegrate resolution uncrowding into elaborator\n\nAdd `or_intro` and `reordering` steps if needed\n\nImplement removal of reordering steps\n\nRename `unremove_all_negations`\n\nAdd option to control granularity of resolution elaboration\n\nFix bug in reordering elaboration\n\nFix measurement of elaboration time\n\nRecord all steps when producing benchmark csv\n\nAllow real arguments to `to_real` operator\n\nFix when parser should interpret integer constants as reals\n\nhave elaboration print if the proof is valid/holey etc\n\nRefactor configuration structs\n\nUse pipeline system in elaborator\n\nRefactor elaborator module\n\nFix conflict in argument names\n\nAdd CLI option to control elaborator pipeline\n\nRemove `lia_generic` elaboration from default pipeline\n\nAdd `lia-generic` to elaboration pipeline if solver was passed\n\nDon't use sharing on terms that are not closed\n\nKeep `define-fun`s when printing proof\n\nAdd option to specify which unknown rules are allowed\n\nReplace `--strict` option by `--check-granularity elaborated`\n\nMake parser `strict` option enforce anchor arguments style\n\nUse `eq_symmetric` rule in elaboration","shortMessageHtmlLink":"Add graph-based representation for proof"}},{"before":"ccf724ad854f78a106982097795a092d612f1167","after":"144f04551c0632235e83c5d026e4c6353e7d5327","ref":"refs/heads/journal-paper","pushedAt":"2024-06-07T13:17:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Use `eq_symmetric` rule in elaboration","shortMessageHtmlLink":"Use <code>eq_symmetric</code> rule in elaboration"}},{"before":"8d1c089e892dd18e304b1e4fc339f631e9aca48b","after":"ccf724ad854f78a106982097795a092d612f1167","ref":"refs/heads/journal-paper","pushedAt":"2024-06-07T12:49:29.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Make parser `strict` option enforce anchor arguments style","shortMessageHtmlLink":"Make parser <code>strict</code> option enforce anchor arguments style"}},{"before":"2ca602c4fa328f58c6a4503a287948df3f96c10f","after":"8d1c089e892dd18e304b1e4fc339f631e9aca48b","ref":"refs/heads/journal-paper","pushedAt":"2024-06-06T07:41:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Add option to specify which unknown rules are allowed","shortMessageHtmlLink":"Add option to specify which unknown rules are allowed"}},{"before":"38f63ca37f23f4af7df7ece2b0fe657696e25747","after":"2ca602c4fa328f58c6a4503a287948df3f96c10f","ref":"refs/heads/journal-paper","pushedAt":"2024-06-05T07:38:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Keep `define-fun`s when printing proof","shortMessageHtmlLink":"Keep <code>define-fun</code>s when printing proof"}},{"before":"c424a590b1280e07f8938bf26ab9579912676e23","after":"38f63ca37f23f4af7df7ece2b0fe657696e25747","ref":"refs/heads/journal-paper","pushedAt":"2024-06-04T09:29:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Don't use sharing on terms that are not closed","shortMessageHtmlLink":"Don't use sharing on terms that are not closed"}},{"before":"a016d0e7c9c60b8cab866748042b2f8c4d135472","after":"c424a590b1280e07f8938bf26ab9579912676e23","ref":"refs/heads/journal-paper","pushedAt":"2024-06-03T09:42:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Add `lia-generic` to elaboration pipeline if solver was passed","shortMessageHtmlLink":"Add <code>lia-generic</code> to elaboration pipeline if solver was passed"}},{"before":"c5f6028c2b1bedaa688214217c5bd6f3e631bae5","after":"a016d0e7c9c60b8cab866748042b2f8c4d135472","ref":"refs/heads/journal-paper","pushedAt":"2024-06-03T09:18:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Remove `lia_generic` elaboration from default pipeline","shortMessageHtmlLink":"Remove <code>lia_generic</code> elaboration from default pipeline"}},{"before":"cafa17aef92785f2195d6cf2404ea6fe3104834c","after":"c5f6028c2b1bedaa688214217c5bd6f3e631bae5","ref":"refs/heads/journal-paper","pushedAt":"2024-06-03T09:13:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Add CLI option to control elaborator pipeline","shortMessageHtmlLink":"Add CLI option to control elaborator pipeline"}},{"before":"f380239f850d951615f4ded05eab10c85e161091","after":"cafa17aef92785f2195d6cf2404ea6fe3104834c","ref":"refs/heads/journal-paper","pushedAt":"2024-06-03T09:03:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Fix conflict in argument names","shortMessageHtmlLink":"Fix conflict in argument names"}},{"before":"6b46f67ef6b2ad05198b5aaf1a26aef29920fec3","after":"f380239f850d951615f4ded05eab10c85e161091","ref":"refs/heads/journal-paper","pushedAt":"2024-06-03T08:35:15.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Refactor elaborator module","shortMessageHtmlLink":"Refactor elaborator module"}},{"before":"fc8a42172dc759dab35965dd0f63f89ecc6fbaba","after":"6b46f67ef6b2ad05198b5aaf1a26aef29920fec3","ref":"refs/heads/journal-paper","pushedAt":"2024-05-31T13:31:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"have elaboration print if the proof is valid/holey etc","shortMessageHtmlLink":"have elaboration print if the proof is valid/holey etc"}},{"before":"579b512758950c7a3af1db2f6a5562eea6aae444","after":"fc8a42172dc759dab35965dd0f63f89ecc6fbaba","ref":"refs/heads/journal-paper","pushedAt":"2024-05-29T14:13:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Fix when parser should interpret integer constants as reals","shortMessageHtmlLink":"Fix when parser should interpret integer constants as reals"}},{"before":"ede8df5b9938a9243bb8070d412d098768483100","after":"579b512758950c7a3af1db2f6a5562eea6aae444","ref":"refs/heads/journal-paper","pushedAt":"2024-05-29T12:16:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Allow real arguments to `to_real` operator","shortMessageHtmlLink":"Allow real arguments to <code>to_real</code> operator"}},{"before":"751a33073a1918b7f30bdf4348d6a2c86f086577","after":"ede8df5b9938a9243bb8070d412d098768483100","ref":"refs/heads/journal-paper","pushedAt":"2024-05-28T15:04:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Record all steps when producing benchmark csv","shortMessageHtmlLink":"Record all steps when producing benchmark csv"}},{"before":"69cffbbbd6c9bf9996ee5a185854b281a2ef1e35","after":"751a33073a1918b7f30bdf4348d6a2c86f086577","ref":"refs/heads/journal-paper","pushedAt":"2024-05-27T20:29:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Fix measurement of elaboration time","shortMessageHtmlLink":"Fix measurement of elaboration time"}},{"before":"782868c39321bdbedd341b99497ae68f5a892cc4","after":"69cffbbbd6c9bf9996ee5a185854b281a2ef1e35","ref":"refs/heads/journal-paper","pushedAt":"2024-05-27T12:49:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Fix bug in reordering elaboration","shortMessageHtmlLink":"Fix bug in reordering elaboration"}},{"before":"742aba55be6e7b4625e291f2d04a6a2501b061fa","after":"782868c39321bdbedd341b99497ae68f5a892cc4","ref":"refs/heads/journal-paper","pushedAt":"2024-05-25T15:53:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Add option to control granularity of resolution elaboration","shortMessageHtmlLink":"Add option to control granularity of resolution elaboration"}},{"before":"7e8d326e16560124847db185844ffc01019e1344","after":"742aba55be6e7b4625e291f2d04a6a2501b061fa","ref":"refs/heads/journal-paper","pushedAt":"2024-05-25T14:56:40.000Z","pushType":"push","commitsCount":23,"pusher":{"login":"bpandreotti","name":"Bruno Andreotti","path":"/bpandreotti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25663412?s=80&v=4"},"commit":{"message":"Rename `unremove_all_negations`","shortMessageHtmlLink":"Rename <code>unremove_all_negations</code>"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEak7c5QA","startCursor":null,"endCursor":null}},"title":"Activity · ufmg-smite/carcara"}