Leonardo de Moura
|
6a5d3ed0e5
|
feat(library/vm/vm_string): use check_system to avoid stack overflow
|
2017-01-13 17:06:24 -08:00 |
|
Leonardo de Moura
|
05d86e49ca
|
feat(library/init/meta/smt): add intros variants for smt_tactic
|
2017-01-13 16:13:37 -08:00 |
|
Leonardo de Moura
|
db646dda89
|
fix(library/tactic/smt/smt_state): forgot to set zeta option
|
2017-01-13 13:33:47 -08:00 |
|
Scott Morrison
|
6f8fc0fe06
|
fix(library/scoped_ext): typo in error message
|
2017-01-13 11:33:17 -08:00 |
|
Leonardo de Moura
|
52164d56b9
|
chore(tests/shell/shell): style
|
2017-01-13 07:39:06 -08:00 |
|
Leonardo de Moura
|
fbc5f7a5fa
|
chore(util/lean_path): compilation warning
|
2017-01-13 07:36:24 -08:00 |
|
Sebastian Ullrich
|
e4ec1808f3
|
fix(util/lean_path): find_imports: .olean files and default modules
|
2017-01-13 07:34:54 -08:00 |
|
Sebastian Ullrich
|
b180c54c0e
|
feat(shell): move lean.js to server mode
|
2017-01-13 07:34:54 -08:00 |
|
Sebastian Ullrich
|
222952d5b8
|
chore(frontends/lean/scanner): another CLion fix
|
2017-01-13 07:34:54 -08:00 |
|
Leonardo de Moura
|
c1ecaf4edd
|
feat(library/tactic/smt/smt_state): do not apply intros automatically in begin[smt]...end blocks
|
2017-01-12 21:49:17 -08:00 |
|
Leonardo de Moura
|
30cea2dceb
|
fix(frontends/lean): auxiliary bind-application in do-notation was not allowing us to obtain type information for the monadic actions.
The new test exposes the problem.
|
2017-01-12 18:38:31 -08:00 |
|
Gabriel Ebner
|
ab539971a6
|
fix(emacs/lean-flycheck): only update next-error-mode for current buffer
|
2017-01-12 13:51:43 -08:00 |
|
Gabriel Ebner
|
fcc559a7f0
|
feat(library/init/util): add trace_call_stack function
|
2017-01-12 21:47:46 +01:00 |
|
Gabriel Ebner
|
b5ac381a5e
|
chore(frontends/lean/print_cmd): update print command to keyword changes
|
2017-01-12 12:04:37 -08:00 |
|
Leonardo de Moura
|
3967cd28fa
|
fix(library/vm/vm): curr_fn() may not be available
|
2017-01-12 11:47:45 -08:00 |
|
Leonardo de Moura
|
ad8c241129
|
perf(library/compiler/eta_expansion): conservative eta_expansion
We only eta_expand where needed (e.g., partial constructor/projection/recursor applications).
|
2017-01-12 11:18:16 -08:00 |
|
Leonardo de Moura
|
1977b4ff3f
|
fix(library/compiler/vm_compiler): bytecode generation error
This bug was introduced by commit 2bd400964c
when we decided to store arguments in reverse order.
|
2017-01-12 11:18:16 -08:00 |
|
Leonardo de Moura
|
1f2b8745dc
|
fix(library/compiler): prevent let-expressions from being expanded
|
2017-01-12 11:18:16 -08:00 |
|
Leonardo de Moura
|
1bfc2f0009
|
fix(library/type_context): remove hack from use_zeta
|
2017-01-12 11:18:16 -08:00 |
|
Leonardo de Moura
|
7e1db95c79
|
fix(frontends/lean): doc strings after constants and axioms
|
2017-01-12 00:22:37 -08:00 |
|
Gabriel Ebner
|
db81e4b5b8
|
feat(frontends/lean/parser): gracefully handle scanner exceptions in imports
|
2017-01-11 23:49:44 -08:00 |
|
Gabriel Ebner
|
7319000c98
|
fix(library/module_mgr): set up message handling outside of exception handler
|
2017-01-11 23:49:44 -08:00 |
|
Gabriel Ebner
|
130f80efff
|
fix(library/module_mgr): gracefully handle exceptions during dependency discovery
|
2017-01-11 23:49:44 -08:00 |
|
Leonardo de Moura
|
df91ae3738
|
fix(library/string,library/init/data/to_string): handle ASCII control characters
|
2017-01-11 23:44:33 -08:00 |
|
Leonardo de Moura
|
acef1efb86
|
fix(frontends/lean/pp,library/equations_compiler,library/tactic/smt/congruence_closure): bug at to_char function
|
2017-01-11 23:44:25 -08:00 |
|
Leonardo de Moura
|
1bb5b2ec01
|
feat(library/tactic/simp_lemmas): do not pretty print bizarre "perm" flag
|
2017-01-11 13:48:11 -08:00 |
|
Leonardo de Moura
|
ae56c6d322
|
feat(frontends/lean/builtin_cmds): improve error message when import is used in the middle of the file
|
2017-01-11 11:15:29 -08:00 |
|
Leonardo de Moura
|
2df280431a
|
fix(library/compiler/comp_irrelevant): fix #1302
|
2017-01-11 11:10:17 -08:00 |
|
Leonardo de Moura
|
a3c7ca1501
|
feat(shell/completion): do not include internal attribute names in auto completion
|
2017-01-11 08:40:36 -08:00 |
|
Sebastian Ullrich
|
83bddce900
|
feat(frontends/lean/info_manager,shell/server,emacs/lean-type): info: provide more metadata
* docs: attributes, options, identifiers
* location: attributes, imports
|
2017-01-11 15:29:14 +01:00 |
|
Sebastian Ullrich
|
7e67b48b2d
|
chore(util/name): avoid parameter name confusing CLion
The overloading of `name` makes it error out on the _entire_ remaining file.
|
2017-01-11 15:27:37 +01:00 |
|
Leonardo de Moura
|
19e20f7e1a
|
fix(frontends/lean/elaborator): universe elaboration issue
|
2017-01-10 22:35:12 -08:00 |
|
Sebastian Ullrich
|
e0ebe9f4a8
|
fix(frontends/lean/tactic_evaluator): show VM errors on tactic
|
2017-01-10 14:42:48 -08:00 |
|
Sebastian Ullrich
|
ed4275ae17
|
fix(frontends/lean/builtin_cmds): do not complete after namespace
Most identifiers used with the command are not namespaces yet
|
2017-01-10 14:42:48 -08:00 |
|
Sebastian Ullrich
|
8eb39bb982
|
fix(frontends/lean/parser): catch exceptions thrown by sync_command
|
2017-01-10 14:42:48 -08:00 |
|
Sebastian Ullrich
|
82bcdebf7c
|
fix(shell/completion): remove duplicate completion candidates
VS Code does not automatically remove them
|
2017-01-10 14:42:48 -08:00 |
|
Leonardo de Moura
|
00c89f209c
|
fix(frontends/lean/definition_cmds): fix #1299
|
2017-01-10 14:38:46 -08:00 |
|
Leonardo de Moura
|
e96bbaee3f
|
fix(library/type_context): fix #1295
|
2017-01-10 11:54:38 -08:00 |
|
Leonardo de Moura
|
cd947e263a
|
fix(library/tactic/smt/congruence_closure): nat numerals do not have a canonical representation
|
2017-01-10 11:26:50 -08:00 |
|
Leonardo de Moura
|
d987df3db9
|
feat(library/tactic/smt): allow propositions without universal quantifiers to be tagged as hinst_lemmas
|
2017-01-10 11:24:27 -08:00 |
|
Leonardo de Moura
|
80d0b8d5f5
|
chore(library,shell): fix style
|
2017-01-10 09:00:17 -08:00 |
|
Sebastian Ullrich
|
3ae4d0fbee
|
feat(shell/completion,emacs/lean-company): provide doc string and location with completion candidate
|
2017-01-10 16:19:32 +01:00 |
|
Sebastian Ullrich
|
2b374cd517
|
fix(emacs/lean-company): do not highlight prefix of non-prefix match
|
2017-01-10 12:25:33 +01:00 |
|
Sebastian Ullrich
|
481a217722
|
feat(shell/completion): prefer exact prefix matches for all completion modes
|
2017-01-10 12:25:33 +01:00 |
|
Sebastian Ullrich
|
cc3126e944
|
feat(frontends/lean,library/scoped_ext,shell): complete namespaces
|
2017-01-10 12:25:33 +01:00 |
|
Sebastian Ullrich
|
fb294f4415
|
chore(shell/server): info: skip "record" output field if null
|
2017-01-10 12:25:33 +01:00 |
|
Sebastian Ullrich
|
3c89a79144
|
feat(shell/completion): sort completions alphabetically (secondary)
|
2017-01-10 12:25:33 +01:00 |
|
Sebastian Ullrich
|
b04df04120
|
feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes
|
2017-01-10 12:25:33 +01:00 |
|
Sebastian Ullrich
|
7ef1bd1a15
|
chore(tests/lean/interactive): simplify input format and test full completion output
|
2017-01-10 12:25:33 +01:00 |
|
Leonardo de Moura
|
c726f19d32
|
fix(library/tactic/smt/ematch): warning
|
2017-01-09 19:28:36 -08:00 |
|