{"push_id":916781128,"size":30,"distinct_size":30,"ref":"refs/heads/master","head":"89a5d00714b92c21f12e958735e663b916c75531","before":"649e5bafcf66f85e85aff861abf6384c8728b4f6","commits":[{"sha":"c5223d2d1967aab18afd970ff2ec2a634aa2a41c","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(emacs/load-lean.el): proceed even if logo image is not created\n\nOn OSX + emacs-24.5, pgm file is not supported in the terminal.\nThis patch ignores the error and does not show the Lean logo if it fails to create one.","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/c5223d2d1967aab18afd970ff2ec2a634aa2a41c"},{"sha":"43a8b01211e479a2978e15786d3d2786ffbbad95","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"feat(extra/depgraph): add dependency graph script","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/43a8b01211e479a2978e15786d3d2786ffbbad95"},{"sha":"f911747b604ed1324bd83fc3d21edc8b67314a2a","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(util/file_lock.cpp): add 'include <fcntl.h>'\n\n@wizardbc found that this is needed while working on lean.js.\nI think it's because of the use of O_CREAT in open system call.\n\nRelated issue: leanprover/lean.js#10","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/f911747b604ed1324bd83fc3d21edc8b67314a2a"},{"sha":"71cad16c32f2e83e199b517dbff474c72275f0fe","author":{"email":"79957c7fe85d3c95360faf96002824a5ec3eee06@gmail.com","name":"Ulrik Buchholtz"},"message":"fix(extras/depgraph): calculate lean executable path from PATH or guess","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/71cad16c32f2e83e199b517dbff474c72275f0fe"},{"sha":"f1daf8f24e0a48cc746f9238c8348b23b989e688","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(algebra/group.lean): remove unnecessary use of add.assoc from theorem bit0_add_bit1_helper","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/f1daf8f24e0a48cc746f9238c8348b23b989e688"},{"sha":"0e3b13f1a0e80c893136be2debe8ee6a65742e82","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"refactor(library/algebra): combine group_bigops and group_set_bigops","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/0e3b13f1a0e80c893136be2debe8ee6a65742e82"},{"sha":"baf11d0018b285a200661c050c9c9527de027a44","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/algebra/ring_bigops): make start on file with more properties of sums and products","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/baf11d0018b285a200661c050c9c9527de027a44"},{"sha":"8ccafc426778297eacb280dc7481291f18429e38","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"fix(library/init/function): fix typo","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/8ccafc426778297eacb280dc7481291f18429e38"},{"sha":"8d50405e682fbe123cceaec1a1ba80f85bd52c5e","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"chore(library/extras/latex/lstlean.text): update lists for syntax highlighting","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/8d50405e682fbe123cceaec1a1ba80f85bd52c5e"},{"sha":"68ecdc4c26cca38247dc1eebdf6d29cb571e3bf7","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(src/emacs/README.md): expand instructions slightly","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/68ecdc4c26cca38247dc1eebdf6d29cb571e3bf7"},{"sha":"6913eb0c768d65260c2857a7d6c6c0d6095bacf5","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"refactor(library/init/subtype.lean): put subtype notation in the namespace\n\nThe notation { x : A | P x } is overloaded in set, and is ambiguous.","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/6913eb0c768d65260c2857a7d6c6c0d6095bacf5"},{"sha":"dc8cad10bf8f9f97d285b9a2cfdf07ed57d3973a","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(src/emacs/README.md): add header","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/dc8cad10bf8f9f97d285b9a2cfdf07ed57d3973a"},{"sha":"5b3fbf161827c1f886e93dd730fc358dff8e743d","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/algebra/module): make a start on modules and vector spaces (with material from Nathaniel Thomas)","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/5b3fbf161827c1f886e93dd730fc358dff8e743d"},{"sha":"08fbf127c61ce164cbcd523d6f79a067e250b9bd","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/analysis/metric_space,real_limit): define complete metric space, make real an instance","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/08fbf127c61ce164cbcd523d6f79a067e250b9bd"},{"sha":"84cdf3d36d401bc2855de3a0530601647b49c592","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/analysis/normed_space): start theory of normed spaces for analysis","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/84cdf3d36d401bc2855de3a0530601647b49c592"},{"sha":"d83e5d25fc9107fb87bf85fa8f1c1a9d9a093aa9","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/measure_theory/extended_real): start on extended reals","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/d83e5d25fc9107fb87bf85fa8f1c1a9d9a093aa9"},{"sha":"549feb5d7f95c0d28450b3778d471becafe58046","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/data/set/basic): add notation and theorems for large unions and intersections","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/549feb5d7f95c0d28450b3778d471becafe58046"},{"sha":"395eab7c2c805299d764971f6ba88f6d78b0273d","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/topology/basic): start on topology (with Jacob Gross)","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/395eab7c2c805299d764971f6ba88f6d78b0273d"},{"sha":"c52ffda0e0a149e6f07854ee18e9c49fa1dc0e87","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/algebra/intervals): add notation for intervals","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/c52ffda0e0a149e6f07854ee18e9c49fa1dc0e87"},{"sha":"fe66e2aa4a40d4a118a8ea930eaa599e65298421","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(tests/lean): subtype notation is not in the top-level anymore","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/fe66e2aa4a40d4a118a8ea930eaa599e65298421"}]}