Sebastian Ullrich
|
3851009ea3
|
fix(frontends/lean/elaborator): elaborate auto_param fields last
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
d8eef9e68e
|
feat(frontends/lean/util): allow lazily resolved auto params
|
2017-03-27 13:42:08 -07:00 |
|
Leonardo de Moura
|
900c56be05
|
feat(frontends/lean,library/equations_compiler): abstract proofs in equations and regular definitions
|
2017-03-25 14:22:52 -07:00 |
|
Leonardo de Moura
|
0890ae5c01
|
fix(library/type_context): When synthesizing subsingleton instances, we should not assign universe metavariables
fixes #1487
|
2017-03-25 10:54:12 -07:00 |
|
Gabriel Ebner
|
122355aa32
|
fix(emacs/lean-server): emacs 24 compatibility
|
2017-03-24 08:28:32 -07:00 |
|
Gabriel Ebner
|
69f0d30452
|
fix(emacs/lean-server): update roi when user changes checking mode
|
2017-03-24 09:29:06 +01:00 |
|
Gabriel Ebner
|
2c7b6fc48f
|
fix(frontends/lean/parser): only show sorry warning once per import
|
2017-03-24 09:19:17 +01:00 |
|
Gabriel Ebner
|
e784fad8c6
|
feat(shell/server,emacs): add visible lines and above checking mode
|
2017-03-24 09:08:17 +01:00 |
|
Gabriel Ebner
|
33b55250a8
|
fix(emacs/lean-server): fix highlight pending tasks toggle
|
2017-03-24 07:35:14 +01:00 |
|
Gabriel Ebner
|
9db6d1d845
|
perf(emacs/lean-server): only render visible task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
f16c2c68db
|
perf(emacs/lean-server): speed up task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
83c4b410be
|
feat(emacs/lean-server): more awesome fringe highlighting
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
7442aa0752
|
fix(frontends/lean/parser): better task description
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
24e19bdd00
|
feat(emacs): add tooltip to task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
af588add56
|
fix(emacs/lean-server): correctly react to scrolling
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
34586a2e82
|
feat(util/log_tree): deindent _next nodes
|
2017-03-24 07:04:35 +01:00 |
|
Gabriel Ebner
|
fdd80c12dd
|
feat(util/log_tree): inherit description
|
2017-03-24 07:04:35 +01:00 |
|
Gabriel Ebner
|
c55579dd69
|
fix(frontends/lean/scanner): initialize m_pos
|
2017-03-24 07:04:35 +01:00 |
|
Leonardo de Moura
|
7543d9e050
|
chore(tests/lean/io_fs_error): fix test
|
2017-03-23 18:52:37 -07:00 |
|
Leonardo de Moura
|
8cf43e1b30
|
feat(library/tactic/tactic_state): add tactic.run_io
|
2017-03-23 18:17:53 -07:00 |
|
Leonardo de Moura
|
7db44ce403
|
chore(library/vm/vm_io): style
|
2017-03-23 16:58:28 -07:00 |
|
Leonardo de Moura
|
fe3875a103
|
feat(library/system/io): add stdin, stdout and stderr
|
2017-03-23 16:49:39 -07:00 |
|
Leonardo de Moura
|
82748a61b7
|
feat(library/system/io): basic file system API
|
2017-03-23 16:30:16 -07:00 |
|
Leonardo de Moura
|
527c8851a8
|
refactor(library/system/io): use type classes
|
2017-03-23 14:29:07 -07:00 |
|
Leonardo de Moura
|
ccd9a8212a
|
chore(shell/lean_js): compilation warning
|
2017-03-23 12:56:35 -07:00 |
|
Gabriel Ebner
|
0d4f829ada
|
fix(library/mt_task_queue): fix abort
|
2017-03-23 15:37:52 +01:00 |
|
Gabriel Ebner
|
8814fe8276
|
chore(tests/lean): add test for error position clamping
|
2017-03-23 09:23:57 +01:00 |
|
Gabriel Ebner
|
69322cd523
|
fix(util/task): evaluate dependencies iteratively
|
2017-03-23 09:16:49 +01:00 |
|
Gabriel Ebner
|
2da9d72491
|
chore(tests/lean/interactive): fix test
|
2017-03-23 09:14:32 +01:00 |
|
Gabriel Ebner
|
73826eee54
|
chore(util/rb_tree): fix clang warning
|
2017-03-23 09:07:50 +01:00 |
|
Gabriel Ebner
|
14c24a66a1
|
feat(emacs): provide commands to change check mode
|
2017-03-23 09:07:09 +01:00 |
|
Gabriel Ebner
|
a6f7f31e85
|
refactor(shell,emacs): handle different checking modes in server
|
2017-03-23 09:07:09 +01:00 |
|
Sebastian Ullrich
|
1f07319bc7
|
fix(emacs/lean-server): Emacs 24 compatibility
|
2017-03-23 09:07:09 +01:00 |
|
Gabriel Ebner
|
a8ba78e20a
|
refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic
|
2017-03-23 09:07:08 +01:00 |
|
Gabriel Ebner
|
d90dda01b0
|
chore(*): fix tests
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
9dfd8e1018
|
fix(shell/server): fix field completion
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
5e29fe227e
|
fix(shell/server): set global ios in info and complete tasks
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
dfb5dad1a3
|
chore(util/log_tree): style
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
c7ca21625c
|
feat(util/log_tree): annotate nodes with detail levels
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
ef0e113b4b
|
chore(tests): fix tests
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
0853d9fd2a
|
fix(util/thread): fix single-threaded build
|
2017-03-23 09:03:42 +01:00 |
|
Gabriel Ebner
|
05c151c60e
|
fix(CMakeLists): make leanchecker link to jemalloc
|
2017-03-23 09:03:42 +01:00 |
|
Gabriel Ebner
|
098d6f8f2a
|
refactor(init/meta/tactic): remove report_errors argument from to_expr
|
2017-03-23 09:03:42 +01:00 |
|
Gabriel Ebner
|
c8fff9f4ff
|
refactor(init/meta/interaction_monad): replace rstep by istep
|
2017-03-23 09:03:41 +01:00 |
|
Gabriel Ebner
|
7f1569535b
|
feat(library/messages): clamp message position to current location
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
98f86ccabd
|
chore(frontends/lean/parser): remove obsolete option
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
e64c10dd20
|
feat(emacs): create all info buffers by default
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
e35968cda1
|
feat(util/memory): implement get_current_rss using the jemalloc API
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
c5c0a74d77
|
fix(frontends/lean/definition_cmds): reinstate fallback to sorry
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
a591e35544
|
chore(*): fix tests
|
2017-03-23 09:00:59 +01:00 |
|