Sebastian Ullrich
|
e5fb11a219
|
chore(emacs/lean-debug): toggle via lean-debug-mode and automatically open debug buffer
|
2016-11-10 15:17:06 -08:00 |
|
Leonardo de Moura
|
922d48524b
|
fix(frontends/lean): fixes #1188
This commit also adds support for recording the type of local variables
in the info_manager
|
2016-11-10 15:08:25 -08:00 |
|
Leonardo de Moura
|
29e5464e42
|
fix(frontends/lean/tactic_notation): fix minor problem for info at position
See comment for details.
|
2016-11-10 13:48:35 -08:00 |
|
Leonardo de Moura
|
0e20d9493b
|
feat(library/quote): make sure to syntactically identical quoted expressions are not equated
Motivation: preserve position information
|
2016-11-10 13:35:54 -08:00 |
|
Leonardo de Moura
|
40fca8efd4
|
feat(frontends/lean): add tactic.save_type_info, preserve pos info at translate
|
2016-11-10 11:51:05 -08:00 |
|
Leonardo de Moura
|
a7af70da2e
|
feat(library/vm): add expr.copy_pos_info
|
2016-11-10 11:50:38 -08:00 |
|
Leonardo de Moura
|
83e0e7104c
|
feat(frontends/lean): save tactic_state in the info_manager
|
2016-11-10 09:56:36 -08:00 |
|
Leonardo de Moura
|
7d3c0c24f8
|
fix(library/compiler): missing file
|
2016-11-10 09:34:32 -08:00 |
|
Leonardo de Moura
|
d6000416f8
|
feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information
We will use this information in the debugger.
|
2016-11-09 16:51:48 -08:00 |
|
Leonardo de Moura
|
b79b76db83
|
feat(library/compiler/vm_compiler): improve local_info collection
|
2016-11-09 12:18:44 -08:00 |
|
Gabriel Ebner
|
a3aced1b30
|
feat(frontends/lean/structure_cmd): record position of structure declaration
|
2016-11-08 19:22:42 -08:00 |
|
Leonardo de Moura
|
6ce00a9b45
|
fix(library/compiler): move inliner to the beginning
Reason: the inliner may introduce recursors, non eta-expanded terms,
etc. Before this commit, it was "undoing" previous compilation steps.
|
2016-11-08 16:14:01 -08:00 |
|
Leonardo de Moura
|
c6558f8af5
|
feat(library/num): handle nat.zero and (nat.succ nat.zero) at to_num
|
2016-11-08 16:13:21 -08:00 |
|
Leonardo de Moura
|
6b3da2daf4
|
feat(library/compiler/vm_compiler): save local_info for let-expressions
|
2016-11-08 15:50:38 -08:00 |
|
Leonardo de Moura
|
d66584f390
|
feat(library/vm,library/compiler): save argument names
|
2016-11-08 15:10:04 -08:00 |
|
Gabriel Ebner
|
cd32335c51
|
feat(emacs/lean-info): push marker to go back after find-definition
|
2016-11-08 11:23:31 -08:00 |
|
Sebastian Ullrich
|
25803e745c
|
fix(emacs/lean-info): support jumping to definition in current file
|
2016-11-08 09:10:09 -08:00 |
|
Sebastian Ullrich
|
131f972499
|
fix(emacs): fix support for emacs < 25 again
|
2016-11-08 09:10:09 -08:00 |
|
Sebastian Ullrich
|
b0037684d8
|
fix(frontends/lean/elaborator): pass info_manager to nested elaborators via thread-local variable
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
9bb167d619
|
chore(frontends/lean): bring back beautiful #ifdefs around json.hpp usage
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
ef633abec7
|
chore(*): fix test and style
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
bb75e6398a
|
feat(emacs, frontends/lean/info_manager): implement 'go to definition'
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
96c9276f52
|
feat(emacs): first working version of info-at-pos
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
bbb06dec70
|
fix(frontends/lean): pass around info_manager at more locations
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
1f9554a014
|
refactor(frontends/lean/info_manager): always pass column in requests
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
ba1b6165e3
|
feat(frontends, shell): implement basic server 'info' command
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
388b337f50
|
chore(frontends/lean/info_manager): make copyable and integrate into snapshots
|
2016-11-08 08:37:41 -08:00 |
|
Sebastian Ullrich
|
67017cecef
|
chore(shell): add back info_manager from master and make it compile
|
2016-11-08 08:37:41 -08:00 |
|
Leonardo de Moura
|
ab12259ba7
|
chore(util/timeit): style
|
2016-11-08 08:36:27 -08:00 |
|
Leonardo de Moura
|
abd96e748f
|
fix(frontends/lean/parser): crash on Win 10
|
2016-11-07 21:30:19 -08:00 |
|
Leonardo de Moura
|
bb5033dc57
|
feat(util/timeit, frontends/lean/definition_cmds): add xtimeit
|
2016-11-07 17:01:19 -08:00 |
|
Gabriel Ebner
|
e88b97d46d
|
fix(library/vm/vm): initialize m_total_time field
|
2016-11-07 15:03:25 -08:00 |
|
Leonardo de Moura
|
db3ad3156b
|
chore(src/kernel/declaration): move cell inside declaration
|
2016-11-07 14:59:37 -08:00 |
|
Gabriel Ebner
|
15e2950834
|
core(frontends/lean/pp): bring back removed pp and pp_detail functions
|
2016-11-07 14:55:32 -08:00 |
|
Gabriel Ebner
|
8eb4bbd0cb
|
fix(kernel/declaration): allow introspection of declarations in GDB
If the declaration::cell struct is not defined in the same header file
as declaration, GDB will show the cells as <incomplete type>.
|
2016-11-07 14:55:32 -08:00 |
|
Gabriel Ebner
|
f52b178a29
|
feat(src/CMakeLists): allow evaluation of inline functions in GDB
|
2016-11-07 14:55:32 -08:00 |
|
Leonardo de Moura
|
7da0acc3fd
|
chore(src/tests/util): fix gcc 6.2 warnings
|
2016-11-07 14:38:33 -08:00 |
|
Leonardo de Moura
|
1cee5fbfea
|
chore(library/compiler/vm_compiler): hide API
|
2016-11-05 14:11:21 -07:00 |
|
Leonardo de Moura
|
2d86d88c92
|
feat(library/tactic/user_attribute): allow user to specify whether attribute is persistent or not
|
2016-11-05 11:46:04 -07:00 |
|
Leonardo de Moura
|
43aa6eb87f
|
fix(library/class): bug in whnf_pred predicate
|
2016-11-05 11:44:05 -07:00 |
|
Leonardo de Moura
|
93ccea11fc
|
chore(frontends/lean): remove dead code
`abstract` can be implemented as a tactic on top of add_decl.
|
2016-11-04 12:36:12 -07:00 |
|
Leonardo de Moura
|
ecb563baa3
|
chore(library/fun_info): patch assertion
The fixed assertion makes sure we don't get an array-index-out-of-bounds
in the for-loop in the end of the procedure.
|
2016-11-04 10:14:00 -07:00 |
|
Daniel Selsam
|
f3dc41b631
|
fix(library/tactic/simplify): only use auto_eq_congr if number of args match
|
2016-11-04 10:13:02 -07:00 |
|
Leonardo de Moura
|
1dcc21525a
|
chore(library/vm/vm): style
|
2016-11-04 09:55:20 -07:00 |
|
Gabriel Ebner
|
1aacf1f20b
|
chore(*): fix style errors
|
2016-11-04 09:47:17 -07:00 |
|
Gabriel Ebner
|
3f85253dac
|
fix(CMakeLists): uncomment style check
|
2016-11-04 09:47:17 -07:00 |
|
Gabriel Ebner
|
41643d6400
|
fix(library/compiler/vm_compiler): prevent segfault
|
2016-11-04 09:47:17 -07:00 |
|
Leonardo de Moura
|
5075891f66
|
chore(library/vm/vm): fix gcc 4.8 warning
|
2016-11-04 09:46:16 -07:00 |
|
Gabriel Ebner
|
ef1fc9871b
|
feat(library/vm/vm): profiler: show cumulative runtimes
|
2016-11-04 09:39:12 -07:00 |
|
Sebastian Ullrich
|
395ddd9d38
|
fix(frontends/lean/builtin_cmds): fix positioning of vm_eval output
|
2016-11-04 09:36:55 -07:00 |
|