{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":566014973,"defaultBranch":"master","name":"pmGenerator","ownerLogin":"xamidi","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2022-11-14T19:51:16.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/3799257?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1725110989.0","currentOid":""},"activityList":{"items":[{"before":"bfc9d7d276babb097d505a76652dd2eb87a2551f","after":"bb832ea33a9214fbeb862639c89d6e381877d2d8","ref":"refs/heads/master","pushedAt":"2024-08-30T21:31:41.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"link to mirror repository at codeberg.org/xamidi/pmGenerator in readme\n\n+ remove helper tools' code\n+ remove unused variable","shortMessageHtmlLink":"link to mirror repository at codeberg.org/xamidi/pmGenerator in readme"}},{"before":"9d4bd396add7b5f50b7d1dff2b30db878492e994","after":"bfc9d7d276babb097d505a76652dd2eb87a2551f","ref":"refs/heads/master","pushedAt":"2024-08-30T20:58:00.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"link to mirror repository at codeberg.org/xamidi/pmGenerator in readme\n\n+ remove helper tools' code\n+ remove unused variable","shortMessageHtmlLink":"link to mirror repository at codeberg.org/xamidi/pmGenerator in readme"}},{"before":"3fbcb77f93aa7e2dacc10cb38c22e0bac114b9a8","after":"9d4bd396add7b5f50b7d1dff2b30db878492e994","ref":"refs/heads/master","pushedAt":"2024-08-30T19:54:34.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"link to mirror on codeberg.org in readme, remove helper tools' code","shortMessageHtmlLink":"link to mirror on codeberg.org in readme, remove helper tools' code"}},{"before":"c5b888c643d9c4791a2ecc0710c5eb5b2762fada","after":"3fbcb77f93aa7e2dacc10cb38c22e0bac114b9a8","ref":"refs/heads/master","pushedAt":"2024-08-15T10:23:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"found 19 shorter proofs for minimal 1-base proof minimization challenge\n\n- solution from https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-10345891 (discussions)\n- m:(A2:7001↦5401,L1:619↦459)\n- w1:A2:1925↦1763\n- w2:(A2:1264633↦27599,A3:1153↦1007,L1:588991↦11703,L2:405↦367)\n- w3:(A2:254925↦14557,A3:23321↦4821,L1:16469↦3227,L2:1331↦1283)\n- w4:(A2:13917↦13819,A3:10779↦10719,L1:12081↦11989,L2:1709↦1703)\n- w5:(A1:83↦75,A2:157↦153)\n- w6:(A2:18339↦10343,L1:2743↦1821)","shortMessageHtmlLink":"found 19 shorter proofs for minimal 1-base proof minimization challenge"}},{"before":"652a46fecc0e35f1a68dd5451049b798b2f85c03","after":"c5b888c643d9c4791a2ecc0710c5eb5b2762fada","ref":"refs/heads/master","pushedAt":"2024-08-08T19:58:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"add time measurements to proof compression output","shortMessageHtmlLink":"add time measurements to proof compression output"}},{"before":"9c758dfb4d0e716d62297d2c57d329726596645c","after":"652a46fecc0e35f1a68dd5451049b798b2f85c03","ref":"refs/heads/master","pushedAt":"2024-08-08T16:10:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"--extract -z: force redundant schema removal for '-t'\n\n+ fix output\n+ update comments for 'auto parse' in DRuleParser::parseAbstractDProof()\n  and 'auto explore' in DRuleParser::compressAbstractDProof()","shortMessageHtmlLink":"--extract -z: force redundant schema removal for '-t'"}},{"before":"12a50bdd51954fece5b80003e3e4dde075fa13b1","after":"9c758dfb4d0e716d62297d2c57d329726596645c","ref":"refs/heads/master","pushedAt":"2024-08-06T05:14:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"'--transform -b -e' fix: unfold correct rules in case they were shifted","shortMessageHtmlLink":"'--transform -b -e' fix: unfold correct rules in case they were shifted"}},{"before":"4ecf8cb727069de18a5efaaf51ee1d8aa941385f","after":"12a50bdd51954fece5b80003e3e4dde075fa13b1","ref":"refs/heads/master","pushedAt":"2024-08-04T01:07:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"--transform -b: duplicate conclusion removal via subproof replacements\n\n- useful to speed up proof compression, for which it preserves all\n  relevant information (assuming full detail and '-t .')","shortMessageHtmlLink":"--transform -b: duplicate conclusion removal via subproof replacements"}},{"before":"0f0a99a46c18a02c515ac04a1094318b3d7ec561","after":"4ecf8cb727069de18a5efaaf51ee1d8aa941385f","ref":"refs/heads/master","pushedAt":"2024-08-01T05:12:26.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'\n\n- new option '-g -f' for old default, which seems mostly pointless","shortMessageHtmlLink":"proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'"}},{"before":"68d05f89bffe486a11568a77774d8b82d2379dfb","after":"0f0a99a46c18a02c515ac04a1094318b3d7ec561","ref":"refs/heads/master","pushedAt":"2024-08-01T04:45:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'\n\n- new option '-g -f' for old default, which seems mostly pointless","shortMessageHtmlLink":"proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'"}},{"before":"97de261ebfcd3882389e354c7d536d377f0bea23","after":"68d05f89bffe486a11568a77774d8b82d2379dfb","ref":"refs/heads/master","pushedAt":"2024-07-31T11:52:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"allow redundant references in proof summaries to be parsed","shortMessageHtmlLink":"allow redundant references in proof summaries to be parsed"}},{"before":"d8ce4b7c95df3511ac4c6af27426e3747a614f0d","after":"97de261ebfcd3882389e354c7d536d377f0bea23","ref":"refs/heads/master","pushedAt":"2024-07-31T02:42:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"make '--transform -z' multi-threaded (with single-threaded option)\n\n+ custom tool ./excludeLists","shortMessageHtmlLink":"make '--transform -z' multi-threaded (with single-threaded option)"}},{"before":"8f19350a408e5e7d8f26a89697381cafbcc6de48","after":"d8ce4b7c95df3511ac4c6af27426e3747a614f0d","ref":"refs/heads/master","pushedAt":"2024-07-29T17:51:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"custom tools ./formulasFromSummaries and ./uniteLists\n\n+ make convertProofSummaryToAbstractDProof() output arguments optional","shortMessageHtmlLink":"custom tools ./formulasFromSummaries and ./uniteLists"}},{"before":"ecd734e99e098c619913e9be0157ae9d1de9cab3","after":"8f19350a408e5e7d8f26a89697381cafbcc6de48","ref":"refs/heads/master","pushedAt":"2024-07-27T12:50:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"--assess: feature to assist with assessments of generation expenditures\n\n+ update description for '--iterate'\n+ code style","shortMessageHtmlLink":"--assess: feature to assist with assessments of generation expenditures"}},{"before":"9d121a9fc0eb0ed030031bbdbf94b6dde6aa04e4","after":"ecd734e99e098c619913e9be0157ae9d1de9cab3","ref":"refs/heads/master","pushedAt":"2024-07-25T10:08:12.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"-g: precise iteration limit calculations for timing estimations\n\n- based on loaded proof collections\n- allows better predictions, tolerates manual modifications\n- remove stored iteration limits\n+ warn in case of deviations","shortMessageHtmlLink":"-g: precise iteration limit calculations for timing estimations"}},{"before":"3f44a65cdf724ebbb0733d12035e06485a51c3e1","after":"9d121a9fc0eb0ed030031bbdbf94b6dde6aa04e4","ref":"refs/heads/master","pushedAt":"2024-07-17T00:14:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"filter out duplicate abstract summary indices (in case of redundancies)\n\n- e.g. such that '--unfold' cannot create empty extra entries\n+ D-rule parser: detect empty D-proofs in input","shortMessageHtmlLink":"filter out duplicate abstract summary indices (in case of redundancies)"}},{"before":"c0c7cfb99e8f2ab4fda740505579b619656a3354","after":"3f44a65cdf724ebbb0733d12035e06485a51c3e1","ref":"refs/heads/master","pushedAt":"2024-07-14T23:10:06.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"--search -t: look for formulas of given schemas (typed search)","shortMessageHtmlLink":"--search -t: look for formulas of given schemas (typed search)"}},{"before":"ae09cc2d4d8abbe5efe0ea63babfacaa5ed2a6cd","after":"c0c7cfb99e8f2ab4fda740505579b619656a3354","ref":"refs/heads/master","pushedAt":"2024-07-14T22:53:35.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"--search -t: look for formulas of given schemas (typed search)","shortMessageHtmlLink":"--search -t: look for formulas of given schemas (typed search)"}},{"before":"9e703cf029c70c5e904bdc59cce2d56df8632c87","after":"ae09cc2d4d8abbe5efe0ea63babfacaa5ed2a6cd","ref":"refs/heads/master","pushedAt":"2024-07-14T21:18:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"--search -t: look for formulas of given schemas (typed search)","shortMessageHtmlLink":"--search -t: look for formulas of given schemas (typed search)"}},{"before":"26bc11a6a8d706b1301c7d6a99a4af58a60903d9","after":"9e703cf029c70c5e904bdc59cce2d56df8632c87","ref":"refs/heads/master","pushedAt":"2024-07-13T19:01:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"w2:(A2:2602085↦1264633,L1:1228561↦588991)\n\n- solution from https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-10039205 and https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-10040068 (discussions)\n- use manual proof of a1dt from https://github.com/icecream17/Stuff/blob/119ddcdf4ed500b6e12d1a80827e334d711ece2c/math/~w2.mm#L440-L441 + proof compression\n- based on https://github.com/xamidi/pmGenerator/commit/26bc11a6a8d706b1301c7d6a99a4af58a60903d9\n\nCo-authored-by: Steven Nguyen <nguyeste008@students.garlandisd.net>","shortMessageHtmlLink":"w2:(A2:2602085↦1264633,L1:1228561↦588991)"}},{"before":"f06cb6eff0f4248fd6c7d8492301eb4716d725f4","after":"26bc11a6a8d706b1301c7d6a99a4af58a60903d9","ref":"refs/heads/master","pushedAt":"2024-07-13T05:09:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"w2:(A2:ω↦2602085,A3:1877↦1153,L1:ω↦1228561,L2:417↦405)\n\n- solution from https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-10037153 (discussions)\n- Prover9 with all hints from w2.txt + extraction search + proof compression\n- based on https://github.com/xamidi/pmGenerator/commit/f06cb6eff0f4248fd6c7d8492301eb4716d725f4","shortMessageHtmlLink":"w2:(A2:ω↦2602085,A3:1877↦1153,L1:ω↦1228561,L2:417↦405)"}},{"before":"694d018b17c0aa1de6550270aed66a72ab9a88de","after":"f06cb6eff0f4248fd6c7d8492301eb4716d725f4","ref":"refs/heads/master","pushedAt":"2024-07-10T23:35:04.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"w2:A3:ω↦1877\n\n- solution from https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-10014766 (discussions)\n- manual composition of known proofs to useful derivations and theorems in Metamath\n- generation based on CpCCqCprCCNrCCNstqCsr,CCCpqrCqr,CCNppp (i.e. w2,jarr,L2)\n  led to DDD1DD2DD1D233321:CpCCCqqNpr\n\nCo-authored-by: Steven Nguyen <nguyeste008@students.garlandisd.net>","shortMessageHtmlLink":"w2:A3:ω↦1877"}},{"before":"0ae9ca6a81bff5e93b93dccfdb08eb4b6d8722b0","after":"694d018b17c0aa1de6550270aed66a72ab9a88de","ref":"refs/heads/master","pushedAt":"2024-07-10T23:27:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"w2:A3:ω↦1877\n\n- solution from https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-10014766 (discussions)\n- manual composition of known proofs to useful derivations and theorems in Metamath\n- generation based on CpCCqCprCCNrCCNstqCsr,CCCpqrCqr,CCNppp (i.e. w2,jarr,L2)\n  lead to DDD1DD2DD1D233321:CpCCCqqNpr\n\nCo-authored-by: Steven Nguyen <nguyeste008@students.garlandisd.net>","shortMessageHtmlLink":"w2:A3:ω↦1877"}},{"before":"942a57901e386a63e8e0895f5c80c75fcdc08bf3","after":"0ae9ca6a81bff5e93b93dccfdb08eb4b6d8722b0","ref":"refs/heads/master","pushedAt":"2024-07-10T18:21:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"-g: set default candidate queue capacity to 50 (for each worker thread)","shortMessageHtmlLink":"-g: set default candidate queue capacity to 50 (for each worker thread)"}},{"before":"212afec3fe19ef922f160804a9950813b5627b05","after":"942a57901e386a63e8e0895f5c80c75fcdc08bf3","ref":"refs/heads/master","pushedAt":"2024-07-04T10:53:28.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"'-g -k' and '--extract -k' : limit lengths of consequents in conclusions\n\n+ improve comments for string schema search\n+ make rAcc read-only as it should be","shortMessageHtmlLink":"'-g -k' and '--extract -k' : limit lengths of consequents in conclusions"}},{"before":"57f90897af5ec705d8c6e5bd6e28d7fd19d16472","after":"212afec3fe19ef922f160804a9950813b5627b05","ref":"refs/heads/master","pushedAt":"2024-07-04T10:25:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"'-g -k' and '--extract -k' : limit lengths of consequents in conclusions\n\n+ improve comments for string schema search","shortMessageHtmlLink":"'-g -k' and '--extract -k' : limit lengths of consequents in conclusions"}},{"before":"88e60d868e90510e43d2113365a972c6ed16816f","after":"57f90897af5ec705d8c6e5bd6e28d7fd19d16472","ref":"refs/heads/master","pushedAt":"2024-07-01T20:15:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"proof collection: use concurrent_hash_map, not concurrent_unordered_map\n\n- internal locks for each element for thread-safe read- and write access\n- performance slightly decreased for collection; improved for filtration\n- memory consumption marginally increased\n- fixes defect where two different collected D-proofs with equal\n  conclusions that are parsed by two threads at the same time could\n  possibly result in a faulty parallel overwrite of the D-proof string\n  - could previously rule out such issues by parsing D-proofs from files\n    and comparing results with given conclusions (e.g. via '--variate')\n+ debug code to print inconsistencies of input vs. utilized","shortMessageHtmlLink":"proof collection: use concurrent_hash_map, not concurrent_unordered_map"}},{"before":"b9caaabbf6b71b317ceefcde72a60882e1d31a51","after":"88e60d868e90510e43d2113365a972c6ed16816f","ref":"refs/heads/master","pushedAt":"2024-06-23T12:37:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"-g: parallelize loader for '-b' and '-v', so it cannot be a bottleneck","shortMessageHtmlLink":"-g: parallelize loader for '-b' and '-v', so it cannot be a bottleneck"}},{"before":"5f6f798c0ee604244bc0d908836fcac88c221804","after":"b9caaabbf6b71b317ceefcde72a60882e1d31a51","ref":"refs/heads/master","pushedAt":"2024-06-20T21:35:23.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"'-g -b' and '-g -v' options to speed up proof collection\n\n- options to balance space vs. time efficiency; default to '-b' to '-v'\n- default: full D-proof parse — space-optimized but slow\n- '-b' seemingly great compromise; might become default option later on\n  - pro: much faster\n    - for '-g -l': increased relevance of speed as opposed to space\n  - contra: less resilient (adopts errors from files), less tested\n- '-v' rather space inefficient, but about as fast as it gets","shortMessageHtmlLink":"'-g -b' and '-g -v' options to speed up proof collection"}},{"before":"5d4c97a0977631fe4126c66ffe47bc0fb2166569","after":"5f6f798c0ee604244bc0d908836fcac88c221804","ref":"refs/heads/master","pushedAt":"2024-06-16T20:25:01.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xamidi","name":null,"path":"/xamidi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3799257?s=80&v=4"},"commit":{"message":"--transform -z: avoid duplicate registrations of evaluation indices\n\n- fixes that duplicate empty rules would be generated upon compression\n+ make steps in w3.txt well-ordered (according to fix; [43] called [52])\n  - files were previously generated without 'indexEvalSequence'\n    rebuilding, of which files other than w3.txt were not affected","shortMessageHtmlLink":"--transform -z: avoid duplicate registrations of evaluation indices"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOC0zMFQyMTozMTo0MS4wMDAwMDBazwAAAASpDnKp","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNi0xNlQyMDoyNTowMS4wMDAwMDBazwAAAARmzB1n"}},"title":"Activity · xamidi/pmGenerator"}