{"push_id":1562944426,"size":13,"distinct_size":13,"ref":"refs/heads/master","head":"7886a78967488a04be2b244383f27e46adfe28e9","before":"e0d57aa8a36ebc9bc1619bae2c4176dd10592ffc","commits":[{"sha":"3b28cef858e9cc3ac364c1da451c3fc6ab5826d2","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(shell/lean): default heartbeat should be unbounded in batch mode","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/3b28cef858e9cc3ac364c1da451c3fc6ab5826d2"},{"sha":"604cbf827aef1c9b503cd4a23e4a33b1b044834f","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"chore(kernel/type_checker): remove dead code","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/604cbf827aef1c9b503cd4a23e4a33b1b044834f"},{"sha":"707cf45a26e11d716192f436fef67e729a008b2e","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(library/type_context): rename whnf_pred => whnf_head_pred","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/707cf45a26e11d716192f436fef67e729a008b2e"},{"sha":"245b4be3150715e1a83de144d570488ef7a0d999","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(library/vm/vm): compilation warning","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/245b4be3150715e1a83de144d570488ef7a0d999"},{"sha":"d4d5ac115c7b7084c0d02941533e09ac3549c0d9","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/type_context): add whnf_transparency_pred","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/d4d5ac115c7b7084c0d02941533e09ac3549c0d9"},{"sha":"7ebf16ca26da82b3d0e458dbcf32cda374ec785d","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(library/equations_compiler): performance issues at structural_rec module and equational lemma generator\n\nThere were two performance bottlenecks in the recursive equation\ncompiler. Both bottlenecks were due to conversion checking.\n\n1- We allow patterns such as (x+1) in the left-hand-side of a\n   recursive equation. This is kind of pattern has to be reduced\n   since it is not a constructor. Moreover, when we are trying to\n   compile using structural recursion, we need to find an element\n   that is structurally smaller in recursive applications.\n   Again, we need to use reduction since the pattern may be (x+2),\n   and in the recursive application we have (x+1). Now, consider\n   the following equation\n\n         f (x+1) (y+1) := f complex_term y\n\n   It will first check whether complex_term is structurally smaller\n   than (x+1), and the compiler will timeout trying to reduce\n   complex_term.\n\n   This commit adds the following workaround. The structural\n   recursion module from now on will only unfold reducible constants\n   and constants marked as patterns. This is not a complete\n   solution. It will timeout in the following equation:\n\n         f (x+1) (y+1) := f (x+1000000000000) y\n\n   For this one, we need to add a whnf \"fuel\" option to type_context\n\n2- Equational lemma generation was producing lemmas that are too\n   expensive to check. Suppose we the following two definitions\n\n       | f x 0     := 1\n       | f x (y+1) := f complex_term y\n\n    and\n\n       | g 0     y    := 1\n       | g (x+1) y    := g x complex_term\n\n    Before this commit, we would generate the following proofs for\n    the second equation of each definition:\n\n         eq.refl (f complex_term y)\n         eq.refl (g x complex_term)\n\n    This proof triggers the following definitionally equality test:\n\n             f x     (y+1)  =?= f complex_term y\n             g (x+1) y      =?= g x complex_term\n\n    Since, we have f/g on both sides, the type checker will try\n    first to unify the arguments, and may timeout trying to solve\n\n               x  =?= complex_term\n               y  =?= complex_term\n\n    since it may take a long time to reduce `complex_term`.\n\n    We workaround this problem by creating a slightly different\n    proof.\n\n          eq.refl (unfold_of(f x (y+1)))\n          eq.refl (unfold_of(g (x+1) y))\n\n    where unfold_of(t) is the result of applying one delta reduction\n    step.","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/7ebf16ca26da82b3d0e458dbcf32cda374ec785d"},{"sha":"8f2a8a3cd38157a072135f91f5ee7ec2e1ec1bb7","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"chore(tests/shell): leftover","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/8f2a8a3cd38157a072135f91f5ee7ec2e1ec1bb7"},{"sha":"368e2bce803e3d83534629d99a6a482845869baf","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/compiler/preprocessor): ignore propositions in the preprocessor\n\nSuppose we have\n\n    def foo : some_proposition :=\n    by non_trivial_automation\n\nMoreover, assume non_trivial_automation generates a huge proof.\nSince this definition is marked with `def`, it is sent to the VM\ncompiler. In this kind of scenario, the compiler preprocessor was\nspending a long time applying \"useless\" preprocessing steps.\nWe say they are useless because in the end everything is erased.\n\nI think we should make sure every definition has some bytecode\nassociated with it in the VM even if the type of the definition\nis a proposition. In this way, we have a simple invariant:\n\n      every definition has a vm_decl associated with it.\n\nSo, we workaround the performance problem above by short-circuiting\nthe preprocessor for propositions.","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/368e2bce803e3d83534629d99a6a482845869baf"},{"sha":"c1c1cd417ab3fdeb3b1538281ce351d839e202d1","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(frontends/lean/builtin_exprs): make sure we use internal names (i.e., names starting with `_`) when compiling do-blocks\n\n@johoelzl This commit fixes the problem you reported at slack.","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/c1c1cd417ab3fdeb3b1538281ce351d839e202d1"},{"sha":"bff3e446569082c73af5357398ca8987ff6f77ed","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(library/vm/vm): compilation error when multi threading is disabled","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/bff3e446569082c73af5357398ca8987ff6f77ed"},{"sha":"ad713c81b4e80b919351b79d29b1288456c871c9","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"perf(library/vm/vm_nat): use __builtin_expect to optimize nat operations\n\n@gebner I used the __builtin_expect trick to optimize the vm_nat module.\nMost of the time, we are processing small numbers.\nIn the following example, the runtime went from 7.27 secs to 6.6 secs\non my machine.\n\ndef mk (a : nat) : nat → list nat\n| 0     := []\n| (nat.succ n) := a :: mk n\n\ndef Sum : list nat → nat → nat\n| []      r := r\n| (n::ns) r := Sum ns (r + n)\n\ndef loop : nat → nat → nat\n| s 0            := s\n| s (nat.succ n) := loop (s + (Sum (mk (n % 2) 1000000) 0)) n\n\nvm_eval timeit \"time\" $ loop 0 30","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/ad713c81b4e80b919351b79d29b1288456c871c9"},{"sha":"1437ee959930291ede5e07b11cd003704ebb4e2e","author":{"name":"Gabriel Ebner","email":"1b660fb788ccf92c8293f42098059e11385ec300@gebner.org"},"message":"fix(kernel/type_checker): disable expression caching in asynchronous proof checking","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/1437ee959930291ede5e07b11cd003704ebb4e2e"},{"sha":"7886a78967488a04be2b244383f27e46adfe28e9","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(library/vm/vm): incorrect lean_vm_check","distinct":true,"url":"https://api.github.com/repos/diakopter/lean/commits/7886a78967488a04be2b244383f27e46adfe28e9"}]}
{"actor":{"display_login":"diakopter"}}