{"push_id":1422422628,"size":33,"distinct_size":33,"ref":"refs/heads/parbld","head":"a9727a2e24029e64a29caed824df1eb9a2fefccd","before":"5332d1a1d2cefc058cfc394c80b5eb85b3f093d5","commits":[{"sha":"3b098656843a46ddaed825f97dea7ad599e82190","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/meta/simp_tactic): add tactics for validating simp lemmas","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/3b098656843a46ddaed825f97dea7ad599e82190"},{"sha":"701fa0d1f46846fbed84898a88245052a958d347","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(frontends/lean/builtin_cmds): make sure declarations generated by run_command get line/col info","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/701fa0d1f46846fbed84898a88245052a958d347"},{"sha":"a4f491a3add9d6a4233ebcec36add327a3f06268","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/meta/interactive): add rename tactic to interactive mode","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/a4f491a3add9d6a4233ebcec36add327a3f06268"},{"sha":"0554fd59972dd95e0901b9cdfe91f328e670b5e6","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(frontends/lean): name resolution at tactic execution time\n\nThis commit also adds a new tactic: tactic.resolve_name\n\ncloses #1201","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/0554fd59972dd95e0901b9cdfe91f328e670b5e6"},{"sha":"50f350f832efdd84314acb2d476c7de5cc28c945","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/ring): add ring -> semiring instance","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/50f350f832efdd84314acb2d476c7de5cc28c945"},{"sha":"25639f0b723124a95dd9a0827604837d351f2163","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/meta): add 'pose' tactic","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/25639f0b723124a95dd9a0827604837d351f2163"},{"sha":"2135d499570811108cbc1ba20a3988055af27959","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/ordered_group): add more aux lemmas","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/2135d499570811108cbc1ba20a3988055af27959"},{"sha":"baed136148e36e863676f25f2b8c999081b44635","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/ordered_ring): add ordered_ring -> ordered_semiring instance","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/baed136148e36e863676f25f2b8c999081b44635"},{"sha":"4d36effe85fee2879b17e5925836a3c8d86bf391","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/ordered_ring): add linear_ordered_ring","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/4d36effe85fee2879b17e5925836a3c8d86bf391"},{"sha":"a009541b6ee091a6c4e3dadd72fc14f7dc1fdde2","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"test(tests/lean/run): add test for issue #1089\n\nSee #1089","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/a009541b6ee091a6c4e3dadd72fc14f7dc1fdde2"},{"sha":"402b8692aaa4f9e4f15345ae2dde7f4b6fecd244","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"feat(*): parallel compilation","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/402b8692aaa4f9e4f15345ae2dde7f4b6fecd244"},{"sha":"5599fdea2e7ef609935cd2a770c2a32218374184","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"chore(shell/lean): clean up command-line arguments","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/5599fdea2e7ef609935cd2a770c2a32218374184"},{"sha":"50fc8bc779ce808414c3cef091f6327f3439aa78","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/50fc8bc779ce808414c3cef091f6327f3439aa78"},{"sha":"57a5b02c49811308bcfeaac37d9565ff852fae1f","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"fix(util/mt_task_queue): fix segfault","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/57a5b02c49811308bcfeaac37d9565ff852fae1f"},{"sha":"3fa7ff808effcd69d0bb331ad47b02bea0c7ee1a","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"fix(kernel/type_checker): fix dangling reference that lead to segfault","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/3fa7ff808effcd69d0bb331ad47b02bea0c7ee1a"},{"sha":"f827c07492324632a014acd1feac87d12c9a65a7","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"fix(frontend/lean/print_cmd): make print work with incorrect proofs","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/f827c07492324632a014acd1feac87d12c9a65a7"},{"sha":"6ad10a0f0f870ae429de281ef0757a4b4df099ac","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(shell/server): gcc compilation error","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/6ad10a0f0f870ae429de281ef0757a4b4df099ac"},{"sha":"7125e6a1fbf6138fe5611b59f28d0a1b8184f767","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(frontends/lean/definition_cmds): implicit universe theorem parameters bug\n\nSee discussion at #1178","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/7125e6a1fbf6138fe5611b59f28d0a1b8184f767"},{"sha":"ba70505db59ae633fdd605c7d44b64ca3563fef2","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"feat(util/task_queue): make task_result accesses lock-free","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/ba70505db59ae633fdd605c7d44b64ca3563fef2"},{"sha":"ed63b75d088509fcebc4e549e671cc02d7809571","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"fix(kernel/type_checker): do not wait for proof","distinct":true,"url":"https://api.github.com/repos/gebner/lean/commits/ed63b75d088509fcebc4e549e671cc02d7809571"}]}
{"actor":{"display_login":"gebner"}}