michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
3711 commits 3 branches 0 tags 28 MiB
Commit graph

3083 commits

Author SHA1 Message Date
Soonho Kong
246d4224bc feat(emacs/lean-tags): call "linja TAGS" to make TAGS 
fix #117
 2014-08-30 14:58:48 -07:00
Soonho Kong
26d548a069 feat(emacs/lean-mode): add lean-tab-indent-or-complete 
Close #105
 2014-08-30 14:57:34 -07:00
Soonho Kong
d393771d8a feat(emacs/eri.el): add eri.el (from agda mode) 2014-08-30 14:57:34 -07:00
Leonardo de Moura
b7d7f12b8e fix(frontends/lean/info_manager): several bugs: invalid flag was not being reset for empty lines, merge with overwrite=false was adding 'poluting' state, --NAY generation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-30 10:35:36 -07:00
Leonardo de Moura
658e0780a6 feat(util/rb_tree): add max (element) method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-30 10:25:12 -07:00
Soonho Kong
a47dada27f feat(emacs/lean-server): add 'SLEEP ms' for trace 2014-08-30 07:51:53 -07:00
Soonho Kong
ad1111cb21 feat(emacs/lean-server): add *lean-server-trace* buffer 
Fix #115.
 2014-08-30 07:38:12 -07:00
Leonardo de Moura
231039ad26 chore(frontends/lean/inductive_cmd): add auxiliary assertion for debugging 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 22:28:22 -07:00
Soonho Kong
543fdf840e fix(emacs/lean-mode): add comment-start "--" 
fix #113
 2014-08-29 20:12:22 -07:00
Leonardo de Moura
373bda0c74 fix(frontends/lean/server): in valid line tracking, add 'VALID' command similar to show, but marks invalid lines with a '*' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 18:17:07 -07:00
Leonardo de Moura
cb27407fcb feat(frontends/lean): add SHOW and SLEEP debugging support commands, fixes worker interrupted bug, and LEAN_SERVER_DIAGNOSTIC compilation mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 18:17:07 -07:00
Soonho Kong
36c632f48d doc(emacs/README.md): clean up 
[skip ci]
 2014-08-29 15:22:06 -07:00
Leonardo de Moura
9a4472cff5 fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 14:32:53 -07:00
Leonardo de Moura
5ebebb30a8 feat(shell): remove --permissive option, closes #107 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 13:26:07 -07:00
Leonardo de Moura
eeffb498b8 feat(frontends/lean/dependencies): send all missing files to standard error, closes #111 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 13:20:25 -07:00
Leonardo de Moura
d7da307f85 feat(frontends/lean/server): add 'OPTIONS' command to 'lean --server' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 12:59:22 -07:00
Leonardo de Moura
bd3fb3489b feat(frontends/lean/dependencies): do not stop computing dependencies at error, compute as many as possible, and sign error in the end 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 12:34:37 -07:00
Leonardo de Moura
3f50fd3ddd feat(build): invoke linja from lean build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 12:15:07 -07:00
Leonardo de Moura
b9489ce585 fix(frontends/let): let-expression pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 10:58:27 -07:00
Soonho Kong
e966aa3145 feat(emacs/lean-settings): use linja for flycheck 2014-08-29 10:31:16 -07:00
Leonardo de Moura
d8548369e7 feat(frontends/lean/pp): improve let-expr pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 07:46:58 -07:00
Leonardo de Moura
2ce92feae1 fix(frontends/lean/pp): remove unreachable code: elaborator eliminates typed_expr macros 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 18:30:33 -07:00
Leonardo de Moura
be56fcf0bd fix(frontends/lean/pp): pretty print 'let-expressions', closes #87 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 18:20:58 -07:00
Leonardo de Moura
662345e2af fix(frontends/lean/elaborator): missing '\n' in error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 18:17:00 -07:00
Leonardo de Moura
b9628842cf feat(library/unifier): remove mk_macro_imitation, we instead expand the macro before solving flex-rigid constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 17:34:03 -07:00
Leonardo de Moura
1e80a9dfe9 feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 16:27:52 -07:00
Leonardo de Moura
79acd3e1b7 fix(kernel/converter): missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 15:21:57 -07:00
Leonardo de Moura
641624a277 fix(library/unifier): bug in expand_rhs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 14:35:11 -07:00
Leonardo de Moura
e303651dee refactor(library/unifier): cleanup mk_macro_imitation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 13:19:19 -07:00
Leonardo de Moura
d9fa9f1039 feat(src/emacs/lean-syntax.el): add commonly used operators 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 13:03:22 -07:00
Leonardo de Moura
f98ab2a8ff fix(src/emacs/lean-syntax.el): remove obsolete command set_opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 11:16:29 -07:00
Leonardo de Moura
b3615d5c8b fix(src/emacs): add 'begin' reserved keyword 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 09:33:09 -07:00
Leonardo de Moura
823a3a7c56 feat(frontends/lean/server): add ECHO command for debugging purposes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 07:40:02 -07:00
Leonardo de Moura
1a8eb9799e feat(frontends/lean/server): preserve info that occurs in columns before first changed column 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 21:09:52 -07:00
Leonardo de Moura
8df5fc0623 fix(frontends/lean/server): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 17:53:00 -07:00
Leonardo de Moura
8719dff361 fix(frontends/lean): distribute '@' over choice 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 16:31:18 -07:00
Leonardo de Moura
19c14fcca7 refactor(frontends/lean/server): refactor lean info server, closes #90, closes #69 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 14:53:16 -07:00
Leonardo de Moura
c7e9e238ec fix(frontends/lean/server): ignore output produced by worker thread, fixes #98 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 10:46:49 -07:00
Leonardo de Moura
fab4eb0d69 feat(frontends/lean/server): add CLEAR_CACHE command, closes #100 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 10:31:01 -07:00
Leonardo de Moura
f4c7154825 feat(util/lean_path): throws an exception if there is an ambiguity when importing a module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 10:18:35 -07:00
Leonardo de Moura
9484ab6a04 fix(util/lean_path): if directory 'foo' does not contain 'default.lean', then we should also check whether the file 'foo.lean' exists or not, fixes #102 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 09:04:03 -07:00
Soonho Kong
f8d2ed7936 feat(emacs/lean-type): maintain nay-retry timer 2014-08-27 00:48:55 -07:00
Soonho Kong
224a4feba2 fix(emacs/lean-type): problem with lean-eldoc-nay-retry-time 
If (current-idle-time) is non-zero, we need to set a timer to run
eldoc-documentation-function again when idle-time = (current-idle-time)
+ retry-delay.
 2014-08-26 23:58:02 -07:00
Soonho Kong
a1a14cf425 fix(emacs/lean-info): handle when both identifier and symbol info exist 
Example: library/data/int/basic.lean file (398, 22)

The '+' symbol is attached with both of identifier info and symbol info

-- SYMBOL|398|22
+
-- ACK
-- IDENTIFIER|398|22
int.add
-- ACK
 2014-08-26 22:32:57 -07:00
Soonho Kong
b9c1b1e186 fix(emacs/lean-info): type of a symbol at the end of buffer 2014-08-26 22:32:57 -07:00
Leonardo de Moura
dd99e60a00 refactor(frontends/lean/info_manager): store environment+options in the info_manager, fixes #96 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 18:07:09 -07:00
Soonho Kong
1de515f693 feat(emacs/lean-mode): clean up old generic-mode 2014-08-26 17:16:16 -07:00
Soonho Kong
665a8f3ecb feat(emacs/lean-server): handle signal 2014-08-26 17:16:16 -07:00
Soonho Kong
0426d04cb9 feat(emacs/README.md): add elisp which installs required packages 2014-08-26 17:16:16 -07:00
Soonho Kong
83f05e104a fix(emacs/lean-server): fix ERROR regex pattern 2014-08-26 16:22:32 -07:00