{"push_id":622888924,"size":48,"distinct_size":48,"ref":"refs/heads/master","head":"f1b7021ed09fb4c25a6bb211e1455ad6386e0eb1","before":"8243ed63399ff15079cbec99a2e534c10a1ca660","commits":[{"sha":"3ac29fae435fdb3a8ba7e7297591e6bf2e187d27","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(util/lua.cpp): 'implicit conversion of nullptr constant to bool' warning\n\nclang-3.6.0 generated the following warning:\n\n/Users/soonhok/work/lean/src/util/lua.cpp:49:12: warning: implicit conversion of nullptr constant to 'bool' [-Wnull-conversion]\n    return nullptr;\n    ~~~~~~ ^~~~~~~\n           false","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/3ac29fae435fdb3a8ba7e7297591e6bf2e187d27"},{"sha":"47c0ae59148e72fc3c0c200df01d2b369004f755","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(bin/linja): download ninja to a temporary directory\n\nAssume that we have two linja processes running on a system where there\nis no ninja installed. Then, the first linja process downloads ninja\nfrom github. If the internet is slow, the second linja process can pick\nup the incomplete ninja binary and execute it, which causes an\nexception (i.e. \"Malformed Mach-o file\" error on OSX). An example build\ntrace is at\n\n    https://s3.amazonaws.com/archive.travis-ci.org/jobs/56366771/log.txt\n\nThis commit fixes the problem by downloading ninja to a temporary\ndirectory and copy it to \"lean/bin/ninja\" when it's completed.","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/47c0ae59148e72fc3c0c200df01d2b369004f755"},{"sha":"033f3b630dcbfae228c1e525aa71c840766bc09c","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean/scanner): allow upper-case greek letters in identifiers but Pi and Sigma","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/033f3b630dcbfae228c1e525aa71c840766bc09c"},{"sha":"cb2a5eeb3cd571e49eb7fa9b195aa9df088575bb","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean/inductive_cmd): local notation in inductive decls","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/cb2a5eeb3cd571e49eb7fa9b195aa9df088575bb"},{"sha":"ec1a60b02cdf58daf56300463bb0c2d69398ab72","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/init/logic): add helper function for proving decidable equality","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/ec1a60b02cdf58daf56300463bb0c2d69398ab72"},{"sha":"66bb22f268c17597044dc27671e1707368726ff2","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/data/list/basic): cleanup","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/66bb22f268c17597044dc27671e1707368726ff2"},{"sha":"42fe87d7cc3ae4138cd717c09396e12d596d7a8b","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/data/list/basic): add sublist predicate","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/42fe87d7cc3ae4138cd717c09396e12d596d7a8b"},{"sha":"299cbe4b25ef37b6aa5cde84ecfefb4c100c30d3","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/data/bool): add auxiliary theorems for bool","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/299cbe4b25ef37b6aa5cde84ecfefb4c100c30d3"},{"sha":"5ef88bfbc8f869c210c605edcf1ebd89fd8a520f","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/logic/examples/propositional): add example based on Floris Coq files formalizing propositional Calculus","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/5ef88bfbc8f869c210c605edcf1ebd89fd8a520f"},{"sha":"9d34431bb62ed97bc47fa0878d8acee744d5a39c","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/logic/examples/propositional/soundness): cleanup precedence levels","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/9d34431bb62ed97bc47fa0878d8acee744d5a39c"},{"sha":"3d4a02089a749b5682f6307d70af99c3cdf372f0","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/logic/examples/propositional): add different encoding","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/3d4a02089a749b5682f6307d70af99c3cdf372f0"},{"sha":"56af7ba535101b91099a86802a52e6d96344d421","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/algebra/ordered_ring): remove sorry","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/56af7ba535101b91099a86802a52e6d96344d421"},{"sha":"87f6fc6b6a8439befbe1146304c01c1c811fcd6c","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/algebra/ring): remove sorrys","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/87f6fc6b6a8439befbe1146304c01c1c811fcd6c"},{"sha":"8c76419c60b63d0d9f7bc04ebb0b99812d0ec654","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(frontends/lean/decl_cmds): error localization problem for recursive equations","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/8c76419c60b63d0d9f7bc04ebb0b99812d0ec654"},{"sha":"3132d229c099cde7bc19b3ff3e0c6cb30b041a60","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"chore(travis): change notifications, turn off cov build","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/3132d229c099cde7bc19b3ff3e0c6cb30b041a60"},{"sha":"46777fdd1d350a4efef233fbb3a90513c03c681c","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(frontends/lean/migrate_cmd): bug when using migrate command with option --to_axiom","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/46777fdd1d350a4efef233fbb3a90513c03c681c"},{"sha":"4c0ce9a6196eacb7cb564f864010eb97c83a7029","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/data/list/basic): missing theorems","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/4c0ce9a6196eacb7cb564f864010eb97c83a7029"},{"sha":"26c914173c907cbb2709af4e9de576825456efeb","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean): add --profile option","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/26c914173c907cbb2709af4e9de576825456efeb"},{"sha":"4eb270a572d1ebed37e62d774b131e2c56545ef4","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(frontends/lean/pp): extra space","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/4eb270a572d1ebed37e62d774b131e2c56545ef4"},{"sha":"e35de54cee07da2c4ed4d02fc7aefe162d9746d0","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/data/list/basic): add aux theorems","distinct":true,"url":"https://api.github.com/repos/beurdouche/lean/commits/e35de54cee07da2c4ed4d02fc7aefe162d9746d0"}]}