leanprover/lean3 issues and pull requests

#100 - add `CLEAR_CACHE` command to lean server

Issue - State: closed - Opened by leodemoura over 10 years ago

#99 - add command `lean-clear-cache` to lean emacs mode

Issue - State: closed - Opened by leodemoura over 10 years ago

#98 - in server mode (--server), send output produced by worker thread to a separate stream

Issue - State: closed - Opened by leodemoura over 10 years ago
Labels: bug

#97 - lean-mode: add imenu support

Issue - State: closed - Opened by soonhokong over 10 years ago

#96 - server: internal info is leaked when showing private definitions

Issue - State: closed - Opened by soonhokong over 10 years ago - 3 comments

#95 - reserve notation

Issue - State: closed - Opened by avigad over 10 years ago

#94 - server: missing synth information

Issue - State: closed - Opened by soonhokong over 10 years ago - 2 comments
Labels: bug

#93 - unnecessary coercion being inserted by the check cmd

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#92 - lean-mode: use cask

Issue - State: closed - Opened by soonhokong over 10 years ago

#91 - lean-mode: check the installation of required packages

Issue - State: closed - Opened by soonhokong over 10 years ago

#90 - server: maintain previous info and send to emacs when the current one is not available.

Issue - State: closed - Opened by soonhokong over 10 years ago

#89 - need type and kind for index (.ilean file)

Issue - State: closed - Opened by soonhokong over 10 years ago

#88 - make sections persistent, contexts transient

Issue - State: closed - Opened by avigad over 10 years ago - 1 comment

#87 - pretty print "let"-expressions correctly

Issue - State: closed - Opened by leodemoura over 10 years ago

#86 - generated class instances should have precedence over terms inferred by type inference

Issue - State: closed - Opened by leodemoura over 10 years ago

#85 - user provided subterm t, being reduced in the fully elaborated term

Issue - State: closed - Opened by leodemoura over 10 years ago

#84 - elaborate statement/type of a theorem independently of the proof.

Issue - State: closed - Opened by leodemoura over 10 years ago

#83 - lean-server: missing identifier info

Issue - State: closed - Opened by soonhokong over 10 years ago

#82 - use 'proof - qed' for creating independent elaboration problems.

Issue - State: closed - Opened by leodemoura over 10 years ago - 2 comments

#81 - Replace 'proof - qed' with 'begin - end' for blocks of tactics

Issue - State: closed - Opened by leodemoura over 10 years ago

#80 - switch '{ }' and '{{ }}' semantics for binders

Issue - State: closed - Opened by leodemoura over 10 years ago - 2 comments

#79 - 'let [inline]' should be the default behavior for let-expressions

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#78 - add/finish "structure" command

Issue - State: closed - Opened by leodemoura over 10 years ago

#77 - Pi / forall intro in class inference

Issue - State: closed - Opened by avigad over 10 years ago

#76 - lean-mode: flycheck is not triggered after change

Issue - State: closed - Opened by soonhokong over 10 years ago - 2 comments
Labels: bug

#75 - lean-mode: use two lean processes for flycheck (with and without cache)

Issue - State: closed - Opened by soonhokong over 10 years ago - 3 comments

#74 - lean-mode: syntax highlight for embedded lua code in lean file

Issue - State: closed - Opened by leodemoura over 10 years ago - 5 comments

#73 - binder info is not being printed correctly in the pretty printer.

Issue - State: closed - Opened by leodemoura over 10 years ago - 2 comments
Labels: bug

#72 - add supporting for tracing/debugging the execution of a "prolog" program associated with a class

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#71 - add command for displaying the "prolog" program associated with a "class"

Issue - State: closed - Opened by leodemoura over 10 years ago

#70 - store unsolved flex flex constraints in the proof state

Issue - State: closed - Opened by leodemoura over 10 years ago
Labels: bug

#69 - avoid delays produced by lean server

Issue - State: closed - Opened by leodemoura over 10 years ago

#68 - separate class instance resolution from unifier

Issue - State: closed - Opened by leodemoura over 10 years ago

#67 - improve order constraints are generated

Issue - State: closed - Opened by leodemoura over 10 years ago

#66 - add delta reduction case split when solving flex rigid constraints

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#65 - calc_subst command should support multiple relations

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment
Labels: bug

#64 - support notation in the pretty printer

Issue - State: closed - Opened by leodemoura over 10 years ago

#63 - multi-line comments in emacs mode

Issue - State: closed - Opened by leodemoura over 10 years ago - 3 comments
Labels: bug

#62 - lean-mode: auto indentation

Issue - State: closed - Opened by soonhokong over 10 years ago - 2 comments

#61 - lean-mode: implement lean-server.py

Issue - State: closed - Opened by soonhokong over 10 years ago - 2 comments

#60 - flycheck does not seem to work if there is no makefile

Issue - State: closed - Opened by leodemoura over 10 years ago - 2 comments
Labels: bug

#59 - can't import sorry from more than one file

Issue - State: closed - Opened by avigad over 10 years ago

#58 - lean server: caching and implicit arguments

Issue - State: closed - Opened by avigad over 10 years ago - 3 comments
Labels: duplicate

#57 - emacs: check buffer-saved when lean-server starts

Issue - State: closed - Opened by soonhokong over 10 years ago
Labels: bug

#56 - lean-mode: flycheck display issue

Issue - State: closed - Opened by soonhokong over 10 years ago - 1 comment

#55 - emacs: add supports for SET and EVAL

Issue - State: closed - Opened by soonhokong over 10 years ago

#54 - lean-mode: auto-complete doesn't work at the end of buffer

Issue - State: closed - Opened by soonhokong over 10 years ago - 5 comments
Labels: bug

#53 - lean server crashes on OSX

Issue - State: closed - Opened by soonhokong over 10 years ago - 9 comments

#52 - emacs: redefine lean-mode

Issue - State: closed - Opened by soonhokong over 10 years ago

#51 - emacs: support -- NAY

Issue - State: closed - Opened by soonhokong over 10 years ago - 1 comment

#50 - ltags

Issue - State: closed - Opened by soonhokong over 10 years ago - 1 comment

#49 - problem: $(LEAN_VERSION_FILE) on Makefile.common

Issue - State: closed - Opened by leodemoura over 10 years ago - 2 comments

#48 - add options to setting delay for requesting type information

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#47 - lmake error message

Issue - State: closed - Opened by avigad over 10 years ago

#46 - Create thread for producing type information in --server mode

Issue - State: closed - Opened by leodemoura over 10 years ago

#45 - use cache in server mode

Issue - State: closed - Opened by leodemoura over 10 years ago

#44 - update tactic framework

Issue - State: closed - Opened by leodemoura over 10 years ago

#43 - add fake dependency to LEAN_VERSION fake file

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#42 - generate corrupted .olean file even if compilation fails

Issue - State: closed - Opened by leodemoura over 10 years ago - 4 comments

#41 - add support for indexing: .ilean files should be generated automatically

Issue - State: closed - Opened by leodemoura over 10 years ago

#40 - add EVAL and SET commands

Issue - State: closed - Opened by leodemoura over 10 years ago - 2 comments

#39 - add -- SYNTH

Issue - State: closed - Opened by leodemoura over 10 years ago

#38 - type information for placeholders

Issue - State: closed - Opened by leodemoura over 10 years ago

#37 - type info left-over

Issue - State: closed - Opened by leodemoura over 10 years ago

#36 - namespace management

Issue - State: closed - Opened by avigad over 10 years ago - 4 comments

#35 - problem with 'INSERT' command (lean-server)

Issue - State: closed - Opened by soonhokong over 10 years ago - 1 comment

#34 - generalize and intro tactics

Issue - State: closed - Opened by avigad over 10 years ago

#33 - error message for application

Issue - State: closed - Opened by avigad over 10 years ago

#32 - default for inductive types

Issue - State: closed - Opened by avigad over 10 years ago

#31 - unambiguous coercions

Issue - State: closed - Opened by avigad over 10 years ago

#30 - section - end matching

Issue - State: closed - Opened by avigad over 10 years ago

#29 - emacs configuration

Issue - State: closed - Opened by avigad over 10 years ago - 1 comment

#28 - lean-mode: line wrapping in error messages

Issue - State: closed - Opened by avigad over 10 years ago - 8 comments

#27 - lmake crash

Issue - State: closed - Opened by leodemoura over 10 years ago

#26 - add pygments lexer for lean

Issue - State: closed - Opened by soonhokong over 10 years ago - 3 comments

#25 - output convention for type info

Issue - State: closed - Opened by soonhokong over 10 years ago - 2 comments

#24 - feature request: using nested namespaces

Issue - State: closed - Opened by avigad over 10 years ago

#23 - don't create .d file when there is an error

Issue - State: closed - Opened by avigad over 10 years ago - 2 comments

#22 - spurious "replacing coercion"

Issue - State: closed - Opened by avigad over 10 years ago

#21 - --flyinfo shows numeric representation of meta variables

Issue - State: closed - Opened by soonhokong over 10 years ago - 2 comments

#20 - add "find" command

Issue - State: closed - Opened by leodemoura over 10 years ago

#19 - Relaxed identifiers: we should be able to use unicode "letter-like" characters (e.g., beta, delta) in identifiers

Issue - State: closed - Opened by leodemoura over 10 years ago

#18 - Column numbers are incorrect when we use unicode characters

Issue - State: closed - Opened by leodemoura over 10 years ago

#17 - shorter commands, like "lean foo" and "lean foo -o"

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#16 - make for directory structure

Issue - State: closed - Opened by leodemoura over 10 years ago

#15 - import file - relative indexing

Issue - State: closed - Opened by leodemoura over 10 years ago - 1 comment

#14 - better way to do "sorry"

Issue - State: closed - Opened by leodemoura over 10 years ago

#13 - chore(.travis.yml): add 'travis_wait' to doxygen build

Pull Request - State: closed - Opened by soonhokong over 10 years ago - 1 comment

#12 - (bitbucket) email diff is disabled.

Issue - State: closed - Opened by soonhokong almost 11 years ago - 1 comment

#11 - Thread-local storage unsupported for the current target: problem in compilation

Issue - State: closed - Opened by ceilican almost 11 years ago - 2 comments

#10 - apply tactic

Issue - State: closed - Opened by leodemoura about 11 years ago

#9 - SMT frontend

Issue - State: closed - Opened by leodemoura about 11 years ago

#8 - Two fixes for the problems that I had on OSX (with Lua-5.1)

Pull Request - State: closed - Opened by soonhokong about 11 years ago - 1 comment

#7 - update cross-compiler for windows (MXE) to use latest gcc-4.8 snapshot and test thread_local support Edit

Issue - State: closed - Opened by soonhokong about 11 years ago - 1 comment
Labels: bug

#6 - Lua 5.2 and cmake

Pull Request - State: closed - Opened by soonhokong about 11 years ago - 1 comment

#5 - Suggestion for lean_assert

Pull Request - State: closed - Opened by soonhokong over 11 years ago - 1 comment

#4 - suggestion to improve lean_assert

Pull Request - State: closed - Opened by soonhokong over 11 years ago

#3 - Rewrite module

Pull Request - State: closed - Opened by soonhokong over 11 years ago

#2 - have separate cmake files for GMP and Tcmalloc

Pull Request - State: closed - Opened by soonhokong over 11 years ago

#1 - add instructions for clang, use markdown format

Pull Request - State: closed - Opened by soonhokong over 11 years ago

GitHub / leanprover/lean3 issues and pull requests