leanprover/lean3 issues and pull requests

#2006 - build error: vm check failed: is_composite(o)

Issue - State: open - Opened by jwaldmann over 5 years ago - 1 comment

#2005 - rewrite cannot handle even the simplest of lemmas involving nat.rec

Issue - State: open - Opened by JasonGross over 5 years ago - 1 comment

#2004 - simp fails to handle recursors

Issue - State: open - Opened by JasonGross over 5 years ago - 2 comments

#2003 - Are there linux install instructions?

Issue - State: closed - Opened by enricozb over 5 years ago - 1 comment

#2002 - Nested names confuse the typechecker

Issue - State: closed - Opened by mrakgr over 5 years ago - 1 comment

#2001 - Autocomplete is incomplete

Issue - State: closed - Opened by mrakgr over 5 years ago - 1 comment

#2000 - Feature/vm dynload

Pull Request - State: closed - Opened by cipher1024 over 5 years ago

#1999 - Add structs support to FFI

Pull Request - State: closed - Opened by agentultra over 5 years ago

#1998 - Fix a failing test (one more still fails, but you have a [TODO] in it)

Pull Request - State: closed - Opened by khoek almost 6 years ago - 1 comment

#1997 - fix(vm/get_cwd): add test for get_cwd

Pull Request - State: closed - Opened by cipher1024 almost 6 years ago - 1 comment

#1996 - Documentation for lean --server

Issue - State: open - Opened by whitequark almost 6 years ago - 4 comments

#1995 - Universe metavariables and typeclass resolution failure

Issue - State: open - Opened by joehendrix almost 6 years ago

#1994 - Add inductive no confusion

Pull Request - State: closed - Opened by digama0 almost 6 years ago - 1 comment

#1993 - [Question]: Proving false vs proving double negation

Issue - State: closed - Opened by domfarolino almost 6 years ago - 2 comments

#1992 - Angle brackets precidence

Issue - State: open - Opened by rspencer01 about 6 years ago

#1991 - Please have a cmake variable that controls if tests should be built

Issue - State: open - Opened by yurivict about 6 years ago

#1990 - Export contains tag #EZ that is not documented

Issue - State: closed - Opened by huma23 about 6 years ago - 1 comment

#1989 - Remove relators and the transfer tactic

Pull Request - State: closed - Opened by gebner about 6 years ago

#1988 - Deep recursion was detected at 'replace'

Issue - State: closed - Opened by stop-cran about 6 years ago - 3 comments

#1987 - chore(.travis.yml): gpg key for new rvm maintainer

Pull Request - State: closed - Opened by bryangingechen about 6 years ago - 1 comment

#1986 - fix(library/module_mgr): ignore '\r' changes

Pull Request - State: closed - Opened by gebner about 6 years ago - 2 comments

#1985 - I cannot find native_compiler.h and some other header files in src folder while building

Issue - State: closed - Opened by NeverLandFly about 6 years ago - 2 comments

#1984 - fix(library/coinductive_predicates): fix existential types

Pull Request - State: closed - Opened by cipher1024 about 6 years ago - 4 comments

#1983 - fix(library/init):removed unused import

Pull Request - State: closed - Opened by huma23 about 6 years ago - 1 comment

#1982 - repeated instance in init/algebra/field.lean

Pull Request - State: closed - Opened by kckennylau about 6 years ago - 1 comment

#1981 - feat(leanpkg): add git branch tracking for dependencies

Pull Request - State: closed - Opened by khoek about 6 years ago - 1 comment

#1980 - leanpkg fails if there's a space in the pathname to the binary

Issue - State: open - Opened by kevinsullivan about 6 years ago - 1 comment

#1979 - Import Isabelle theorems

Issue - State: closed - Opened by mrmartin over 6 years ago - 1 comment

#1978 - fix(frontends/dependencies): ignore `.olean` files when listing depen…

Pull Request - State: closed - Opened by cipher1024 over 6 years ago

#1977 - Add Coq-like "abort" tactic

Issue - State: open - Opened by kevinsullivan over 6 years ago - 4 comments

#1976 - fix(lean/bin/leanpkg*): handle spaces in paths

Pull Request - State: closed - Opened by solson over 6 years ago - 2 comments

#1975 - leanpkg new returns failed to start child process

Issue - State: open - Opened by fstiffo over 6 years ago - 2 comments

#1974 - out of date files on bitbucket

Issue - State: open - Opened by holtzermann17 over 6 years ago

#1973 - leanpkg doesn't work on Windows when lean is copied to C:\Program Files\lean\

Issue - State: closed - Opened by varosi over 6 years ago - 3 comments

#1972 - Seg fault on lean.exe

Issue - State: open - Opened by alisever over 6 years ago - 1 comment

#1971 - OSX binary depends on libgmp, missing by default

Issue - State: open - Opened by kevinsullivan over 6 years ago - 3 comments

#1970 - leanfmt: Lean code formatter

Issue - State: open - Opened by alok over 6 years ago - 2 comments

#1969 - Workaround for unsupported equality between type and constructor indices

Issue - State: closed - Opened by evhub over 6 years ago - 5 comments

#1968 - algebraic data type vm check failed is_closure

Issue - State: closed - Opened by joehendrix over 6 years ago - 2 comments

#1967 - doxygen: problems opening map file doc/html/inherit_graph_180.map for inclusion

Issue - State: open - Opened by andres-erbsen over 6 years ago

#1966 - gcc 8.1.1: trie.h:69:76: error: ‘this’ was not captured for this lambda function

Issue - State: open - Opened by andres-erbsen over 6 years ago - 4 comments

#1965 - GCC: ‘this’ was not captured for this lambda function

Issue - State: closed - Opened by EdAyers over 6 years ago - 5 comments

#1964 - Can't find the output of exporting the Lean library in low level format.

Issue - State: open - Opened by ITervaNkYu over 6 years ago

#1963 - Meta program that traverses product expressions fails

Issue - State: closed - Opened by kendroe over 6 years ago - 3 comments

#1962 - error with leanpkg

Issue - State: closed - Opened by blairshi111 over 6 years ago - 1 comment

#1961 - subtype.eq has wrong signature

Issue - State: open - Opened by fgdorais over 6 years ago - 3 comments

#1960 - fix(doc/export_format): correct #DEF example and typos

Pull Request - State: closed - Opened by andrejtokarcik over 6 years ago - 1 comment

#1959 - Typo in Tutorial

Issue - State: closed - Opened by kevinsullivan almost 7 years ago - 2 comments

#1958 - Segfault with monad inference

Issue - State: open - Opened by digama0 almost 7 years ago

#1957 - Error with meta mutual defs

Issue - State: open - Opened by digama0 almost 7 years ago

#1956 - silent overflow with large integers

Issue - State: closed - Opened by kbuzzard almost 7 years ago

#1955 - fix(init/core): typed_expr should accept Props

Pull Request - State: closed - Opened by Kha almost 7 years ago

#1954 - Problem with `typed_expr`

Issue - State: closed - Opened by johoelzl almost 7 years ago

#1953 - [feature] io.proc.fork

Issue - State: closed - Opened by forked-from-1kasper almost 7 years ago

#1952 - assertion violation when using rfl to define instance

Issue - State: closed - Opened by kbuzzard almost 7 years ago - 1 comment

#1951 - nat.pow is not right-associative

Issue - State: closed - Opened by kbuzzard almost 7 years ago - 1 comment

#1950 - refactor(library/init/core,library/init/unit): make `unit` an abbreviation of `punit.{0}`

Pull Request - State: closed - Opened by Kha almost 7 years ago - 1 comment

#1949 - [WIP] Turn on jemalloc, turn off custom allocators by default

Pull Request - State: closed - Opened by Kha almost 7 years ago - 9 comments

#1948 - Proper nightly builds

Pull Request - State: closed - Opened by Kha almost 7 years ago - 1 comment

#1947 - fix(tactic_state): bugfix

Pull Request - State: closed - Opened by semorrison almost 7 years ago

#1946 - Build broken by last commit

Issue - State: closed - Opened by semorrison almost 7 years ago

#1945 - Fix server memory leak

Pull Request - State: closed - Opened by Kha almost 7 years ago

#1944 - chore(README,doc/faq): The Gitter chat room has been migrated to Zulip

Pull Request - State: closed - Opened by Kha almost 7 years ago

#1943 - unknown declaration 'B.mk.inj_eq._aux_1'

Issue - State: closed - Opened by semorrison almost 7 years ago - 2 comments

#1942 - Lean assertion violation

Issue - State: closed - Opened by semorrison almost 7 years ago

#1941 - make sure no one calls math.h's log2()

Pull Request - State: closed - Opened by nunoplopes almost 7 years ago - 4 comments

#1940 - ematch fails when there are two instance arguments which are different types of a type family

Issue - State: closed - Opened by semorrison almost 7 years ago - 2 comments

#1939 - fix(frontends/lean/pp): fix #1922

Pull Request - State: closed - Opened by Kha almost 7 years ago - 3 comments

#1938 - fix(frontends/lean/pp): is_field_notation_candidate

Pull Request - State: closed - Opened by semorrison almost 7 years ago - 1 comment

#1937 - AppVeyor: Support MSVC

Pull Request - State: closed - Opened by Kha almost 7 years ago - 14 comments

#1936 - Encapsulate tactic's Lean implementation better

Pull Request - State: closed - Opened by Kha almost 7 years ago

#1935 - fix MSVC build

Pull Request - State: closed - Opened by nunoplopes almost 7 years ago - 1 comment

#1934 - More misc changes from the monad PR

Pull Request - State: closed - Opened by Kha almost 7 years ago - 1 comment

#1933 - fix(library/tactic/simp_lemmas): avoid rewrite failure with more robust code

Pull Request - State: closed - Opened by Kha almost 7 years ago - 2 comments

#1932 - fix memory leak in type_context.cpp

Pull Request - State: closed - Opened by nunoplopes almost 7 years ago - 1 comment

#1931 - Fix crash on Windows/VS when invoking external processes

Pull Request - State: closed - Opened by nunoplopes almost 7 years ago - 4 comments

#1930 - assertion violation

Issue - State: closed - Opened by semorrison almost 7 years ago

#1929 - Profiling improvements

Pull Request - State: closed - Opened by Kha almost 7 years ago

#1928 - Name collision between fields and parameters in struct declaration

Issue - State: open - Opened by Rotsor almost 7 years ago - 1 comment

#1927 - fix MSVC build

Pull Request - State: closed - Opened by nunoplopes almost 7 years ago - 3 comments

#1926 - chore(README.md) fixing link to download page

Pull Request - State: closed - Opened by semorrison almost 7 years ago

#1925 - cleanup(init/meta/tactic) removing obsolete meta constants

Pull Request - State: closed - Opened by semorrison almost 7 years ago - 1 comment

#1923 - fix warnings with VS

Pull Request - State: closed - Opened by nunoplopes almost 7 years ago - 3 comments

#1922 - bug with pp.implicit and structure fields

Issue - State: closed - Opened by semorrison almost 7 years ago

#1920 - Adding type class instances in tactic mode doesn't work anymore

Issue - State: closed - Opened by johoelzl almost 7 years ago - 12 comments

#1918 - Build shouldn't copy files into the source directory

Issue - State: closed - Opened by nunoplopes about 7 years ago - 4 comments

#1915 - Can `simp at *` also work on non-dependent hypotheses which are not propositions?

Issue - State: closed - Opened by semorrison about 7 years ago - 1 comment

#1910 - Pretty substitution of backslashed keywords doesn't occur unless a space terminates the keyword

Issue - State: closed - Opened by quaeler about 7 years ago - 1 comment

#1889 - `dsimp at *` interacts poorly with `let` expressions

Issue - State: closed - Opened by semorrison about 7 years ago

#1884 - Revert "fin.succ injective theorem"

Pull Request - State: closed - Opened by digama0 about 7 years ago

#1881 - Monad refactorings

Pull Request - State: closed - Opened by Kha about 7 years ago - 8 comments

#1878 - refactor(algebra/ordered_field): move theorems from discrete

Pull Request - State: closed - Opened by digama0 about 7 years ago - 1 comment

#1858 - refactor(init/meta/interactive): factor out replace_at from simp_core_aux

Pull Request - State: closed - Opened by digama0 about 7 years ago - 2 comments

#1857 - chore(init/algebra/group): use a user attr for transport to additive

Pull Request - State: closed - Opened by digama0 about 7 years ago - 1 comment

#1836 - unreachable code with cases tactic

Issue - State: closed - Opened by fpvandoorn over 7 years ago

#1827 - eq.subst produces a type mismatch when eta-expanded

Issue - State: closed - Opened by mrhaandi over 7 years ago - 7 comments

#1821 - chore(.travis.yml): undo Travis update

Pull Request - State: closed - Opened by Kha over 7 years ago

#1796 - feat(init/meta/injection_tactic): injection also does subst

Pull Request - State: closed - Opened by digama0 over 7 years ago - 3 comments

#1552 - cabb435 causes `eblast` to often fail

Issue - State: closed - Opened by semorrison almost 8 years ago - 3 comments
Labels: P-low, A-smt

#1392 - Problem building master on Windows: CMake can't find GMP (mingw64, cmake, make)

Issue - State: closed - Opened by kevinsullivan almost 8 years ago - 6 comments

GitHub / leanprover/lean3 issues and pull requests