Issues

• leanittest_complete_trailing_period.lean test fails (99% tests passed, 1 tests failed out of 1441)

  leanprover-community/lean#816 · Filter by author barracuda156 opened on Sep 3, 2024

• Segmentation fault when using get_env with run_tactic

  leanprover-community/lean#803 · Filter by author lenianiva opened on Mar 15, 2023
  1

• "Invalid return type" error when definining inductive propositions can be attached to more suitable text range

  leanprover-community/lean#802 · Filter by author ddrone opened on Feb 25, 2023
  1

• pp.links handles unit.star badly

  leanprover-community/lean#789 · Filter by author eric-wieser opened on Dec 2, 2022

• opening a namespace can affect elaboration

  leanprover-community/lean#776 · Filter by author alexjbest opened on Oct 26, 2022

• local notation can change explicitness of arguments

  bug
  leanprover-community/lean#772 · Filter by author fpvandoorn opened on Sep 26, 2022

• clang prints warnings: use reference type ... to prevent copying

  leanprover-community/lean#767 · Filter by author yurivict opened on Sep 5, 2022

• Simple programs run for many seconds

  leanprover-community/lean#765 · Filter by author yurivict opened on Sep 1, 2022
  8

• Failures in get_peak_rss() should fail the application instead of silently returning 0

  leanprover-community/lean#763 · Filter by author yurivict opened on Aug 31, 2022

• Kernel failed to type-check due to name collision involving include

  bug
  leanprover-community/lean#751 · Filter by author Vierkantor opened on Jul 29, 2022

• exceptions when saving oleans are not user-visible

  leanprover-community/lean#750 · Filter by author collares opened on Jul 29, 2022

• is_bi_equal use of BinderInfo-unaware hashes causes many collisions (a.k.a. timeout when saving oleans)

  leanprover-community/lean#749 · Filter by author collares opened on Jul 29, 2022

• Assertion failure in local_context_adapter.cpp

  leanprover-community/lean#748 · Filter by author eric-wieser opened on Jul 29, 2022
  1

• native.rb_map.insert not working as expected

  leanprover-community/lean#738 · Filter by author isadofschi opened on Jul 10, 2022
  2

• invalid synthesis of reflected instances

  leanprover-community/lean#731 · Filter by author eric-wieser opened on Jun 16, 2022

• Cannot build .olean file on NFS

  leanprover-community/lean#718 · Filter by author Longhao-Chen opened on May 21, 2022
  6

• Test failure on i686 (32 bit)

  leanprover-community/lean#685 · Filter by author tornaria opened on Feb 19, 2022

• "kernel failed to type check declaration" in presence of implicit coercion to Sort

  leanprover-community/lean#672 · Filter by author kmill opened on Jan 25, 2022

• universe error in definition generated by the equation compiler

  leanprover-community/lean#655 · Filter by author robertylewis opened on Dec 10, 2021

• apply tactic produces incorrect proof

  leanprover-community/lean#644 · Filter by author gebner opened on Nov 1, 2021
  1

• segfault in badly typed pattern match

  leanprover-community/lean#625 · Filter by author robertylewis opened on Sep 22, 2021

• CI: Flaky test on macos debug runs

  leanprover-community/lean#624 · Filter by author bryangingechen opened on Sep 22, 2021

• simp ignores direction of equation lemmas

  leanprover-community/lean#623 · Filter by author eric-wieser opened on Sep 21, 2021

• (No equational lemmas)/(Mistaken as field notation) when using a namespace inside a section with universe polymorphism

  leanprover-community/lean#613 · Filter by author winestone opened on Sep 6, 2021

• Repeat tactic does not terminate instead of giving an error or functioning as it should.

  leanprover-community/lean#584 · Filter by author Karthik-Dulam opened on Jun 20, 2021
  1