max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
11199 commits 1 branch 0 tags 5.3 GiB
Commit graph

11199 commits

This branch
This branch
All branches
Author SHA1 Message Date
Gabriel Ebner
7daefedf05 chore(shell/server): remove hard limit on number of reported tasks 2017-01-17 17:10:37 -08:00
Gabriel Ebner
7d9c89b519 feat(emacs/lean-server): show skullbones as soon as server dies 2017-01-17 17:10:37 -08:00
Gabriel Ebner
a230c47178 feat(util/task_queue,emacs,*): highlight running tasks with different background color 2017-01-17 17:10:37 -08:00
Sebastian Ullrich
484bb67d44 fix(frontends/lean/tactic_notation): report state after tactic execution on , 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
6acc2cf8b7 fix(frontends/lean/notation_cmd): some position fixes 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
7b049e7d55 fix(shell/server): prevent empty prefix completion for declarations 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
59055fd5d0 feat(emacs): new and improved goal and next error buffers 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
568862ea91 chore(emacs): remove unimplemented binding C-c C-p 2017-01-17 16:38:00 -08:00
Scott Morrison
8c723cea72 workaround instruction for gperftools on macOS Sierra 2017-01-17 16:37:06 -08:00
Leonardo de Moura
3178f41cce fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied 
see #1316
 2017-01-17 16:33:19 -08:00
Gabriel Ebner
b4774e9ed1 fix(library/vm/vm): fix segfault in call_stack_fn 2017-01-17 16:00:01 -08:00
Leonardo de Moura
8e76d079d3 chore(tests/lean/run): fix tests 2017-01-17 15:50:54 -08:00
Gabriel Ebner
1a6629ce3b feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08:00
Leonardo de Moura
7a210a9b62 chore(library/util): style 2017-01-16 22:59:17 -08:00
Leonardo de Moura
e19e5ae212 test(tests/lean/run): test inductive datatypes with non-recursive arguments after recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
fc00275636 fix(library/compiler/elim_recursors): it was assuming that recursive arguments occur after non recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
70b7a35cfe fix(library/constructions/has_sizeof): it was assuming that recursive arguments occur after non recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
1db1f8b229 feat(kernel/inductive/inductive): do not force recursive arguments to occur after non-recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
29b7001bff fix(library/equations_compiler/elim_match): avoid nasty inferred types in auxiliary declarations produced by the equation compiler 2017-01-16 22:55:12 -08:00
Leonardo de Moura
cce6e4d58c fix(library/equations_compiler/compiler): fix #1315 2017-01-16 20:01:25 -08:00
Leonardo de Moura
0ad6dec5fd fix(tests/lean/run/converter): fix test 2017-01-16 19:04:52 -08:00
Leonardo de Moura
bfa48ff0c7 fix(frontends/lean/parser): position info when error is inside notation 2017-01-16 10:29:00 -08:00
Leonardo de Moura
eabbc5bb68 chore(library/module_mgr): comment unreachable_code assertion 
@gebner, could you please take a look a check whether there is a better fix.
 2017-01-15 23:18:44 +01:00
Leonardo de Moura
67226269b4 feat(library/tactic/simp_lemmas): convenient way of adding equational lemmas of a definition to a simp set 2017-01-14 22:16:16 -08:00
Leonardo de Moura
c3b7c54d7c chore(.travis.yml): fix STATIC config 2017-01-14 08:55:02 -08:00
Leonardo de Moura
612c02d11e chore(.travis.yml): use static build for binary distribution for Linux 2017-01-14 08:25:27 -08:00
Leonardo de Moura
6246e6d72f fix(src/CMakeLists): -DSTATIC=ON option 
We are still getting a bunch of warnings because of dynamic_library.cpp.
I will fix this later.
 2017-01-14 08:23:51 -08:00
Leonardo de Moura
0a63133abe chore(.appveyor.yml): missing DLLs 2017-01-14 07:47:38 -08:00
Leonardo de Moura
1f7ad171c4 chore(README.md): test 2017-01-14 00:10:30 -08:00
Leonardo de Moura
8be43e524b chore(.appveyor.yml): update artifact decl 2017-01-13 22:57:27 -08:00
Leonardo de Moura
c1a3c562c8 chore(.travis.yml): deployment file path, cpack invocation 2017-01-13 22:51:53 -08:00
Leonardo de Moura
75fb8f109d chore(.appveyor.yml): trying again 2017-01-13 22:36:10 -08:00
Leonardo de Moura
450d20d0db chore(.appveyor.yml): remove "branch: master" 2017-01-13 22:05:53 -08:00
Leonardo de Moura
5502c21578 chore(.travis.yml): update secure 2017-01-13 22:02:59 -08:00
Leonardo de Moura
647efd7d63 fix(.appveyor.yml): artifact path 2017-01-13 21:47:13 -08:00
Leonardo de Moura
9561cb8385 chore(.travis.yml): update secure 2017-01-13 20:55:52 -08:00
Leonardo de Moura
6e9a6d15db fix(.appveyor): fix typo 2017-01-13 20:41:20 -08:00
Leonardo de Moura
f8b91e35af chore(.appveyor.yml): add deploy config 2017-01-13 20:33:55 -08:00
Leonardo de Moura
8dfe6ce385 chore(.travis.yml): try to fix upload 2017-01-13 20:00:21 -08:00
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
6ebc23eca4 feat(library/init/meta/smt/smt_tactic): add smt_tactic.induction 
Non-interactive version.
 2017-01-13 16:49:54 -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
a6ef7f52a9 chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -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
François G. Dorais
b305130ec3 fix(library/init/wf): typo 
Same typo as #1091, different location.
 2017-01-13 11:35:52 -08:00
Gabriel Ebner
5f790d82cd fix(test/lean/run/super_tests): fix try_sup API change 2017-01-13 11:33:35 -08:00
Scott Morrison
6f8fc0fe06 fix(library/scoped_ext): typo in error message 2017-01-13 11:33:17 -08:00
Leonardo de Moura
69fd35f068 feat(library/init/meta/smt): add helper tactics and doc-strings 2017-01-13 11:21:20 -08:00
Leonardo de Moura
04fb7b88e7 feat(library/init/algebra): mark basic facts as [ematch] until we have support for arithmetic 2017-01-13 10:36:08 -08:00
Leonardo de Moura
6f4bcbab20 feat(library/init/meta/smt/ematch): convenient way of marking all equational lemmas of a giving definition as ematch lemmas 2017-01-13 10:35:09 -08:00