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

3388 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
9a6df02683 fix(util/name): avoid assertion violation when reading numeric names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 08:32:43 -07:00
Leonardo de Moura
6d6c62461f chore(library/kernel_serializer): add assertions for invalid uses of anonymous names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 08:32:32 -07:00
Leonardo de Moura
955d7d2659 fix(library/aliases): namespace and constant have the same name, and 'using' produces the 'empty' alias 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 08:32:21 -07:00
Leonardo de Moura
4ad7e709aa feat(frontends/lean): default for inductive types, closes #32 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 07:52:37 -07:00
Leonardo de Moura
72e4f113b3 doc(server): describe server mode format 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 23:16:37 -07:00
Leonardo de Moura
b56233cbe3 fix(frontends/lean): make sure typing information is sorted, make sure the error messages contains line file name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 23:15:05 -07:00
Leonardo de Moura
c6f3232f81 feat(frontends/lean): provide 'partial' type information even when there are type errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 21:56:57 -07:00
Leonardo de Moura
1cbf40a5d2 fix(frontends/lean): remove duplicate info entries, fix bug in save_overload 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 21:23:37 -07:00
Leonardo de Moura
8d9ca4c4ea fix(tests/lean): remove obsolete test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 19:40:02 -07:00
Leonardo de Moura
0af4a67881 feat(frontends/lean): save type information after elaboration, remove --flyinfo option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 19:35:26 -07:00
Leonardo de Moura
0276f4c1c0 feat(frontends/lean): store 'overload' information, remove #setline 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 19:13:09 -07:00
Leonardo de Moura
1ba9a92df2 feat(frontends/lean/parser): save snapshots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 18:31:53 -07:00
Leonardo de Moura
9b765a2a06 chore(frontends/lean): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 18:10:33 -07:00
Leonardo de Moura
1a725574b1 refactor(frontends/lean): add 'server' module as a replacement for 'interactive' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 18:07:04 -07:00
Leonardo de Moura
2c3737bcc6 feat(frontends/lean): add info_manager 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 15:25:28 -07:00
Leonardo de Moura
a173b7f6e6 test(tests/lean/interactive): add old 'interactive' tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 14:57:08 -07:00
Soonho Kong
b0a25cdbc9 fix(bin/lmake): missing case: no makefile & dir specified 
close #27
 2014-08-06 07:40:03 -07:00
Leonardo de Moura
da616f69ea perf(library/unifier): do not explore branches that will trigger type errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 20:16:16 -07:00
Leonardo de Moura
bbc4380a52 fix(library/unifier): bug exposed by recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 19:02:30 -07:00
Leonardo de Moura
069f217215 fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 17:21:21 -07:00
Leonardo de Moura
d14cbfd7e9 refactor(frontends/lean/elaborator): local context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 16:25:54 -07:00
Leonardo de Moura
9cc2015caa feat(library/unifier): better error message for invalid local context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 16:25:22 -07:00
Leonardo de Moura
d1924097d5 feat(library/match): add 'local' backtracking 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 10:09:00 -07:00
Leonardo de Moura
e6ffda0c51 feat(library/match): add basic match_plugin that just invokes whnf before failing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 08:37:03 -07:00
Soonho Kong
a4b023a175 feat(bin/lmake): support multiple targets; add '-C', '-f' options 2014-08-05 02:19:15 -07:00
Leonardo de Moura
56d151ef7f feat(frontends/lean): 'partial' aliases. closes #24 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 22:08:10 -07:00
Leonardo de Moura
f4031b620f feat(library/match): extend match_plugin interface, and allow them to recursively invoke the matcher 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 18:30:30 -07:00
Leonardo de Moura
c34c2f4f5c feat(library/match): match universe levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 18:30:30 -07:00
Leonardo de Moura
b0a5ff7f93 refactor(library): rename hop_match to match 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 18:30:30 -07:00
Soonho Kong
57410e7818 fix(bin/lmake): use '-j' option for make 
[skip ci]
 2014-08-04 17:28:57 -07:00
Leonardo de Moura
0d5e346143 fix(library/expr_lt): make sure the builtin order is AC-compatible 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 15:51:10 -07:00
Soonho Kong
b2cb49fa1f feat(bin/lmake): add lmake 
lmake tries to find a makefile in the current working-directory or its
ancestors and invoke the makefile if found. If a makefile is not found,
it calls lean directly. This is also used for flycheck-lean.

Usage:

    $ lmake
    $ lmake all
    $ lmake clean
    $ lmake basic
    $ lmake basic.lean
    $ lmake /home/user/projects/lean/library/.../basic.lean
    $ lmake --flyinfo --flycheck basic
 2014-08-04 15:17:23 -07:00
Leonardo de Moura
b9fadeb86e fix(util/realpath): realpath on cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 15:06:08 -07:00
Leonardo de Moura
5755ce4bfc fix(util/lean_path): use unix style paths when using cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 14:45:23 -07:00
Leonardo de Moura
53c7124c2b fix(util/realpath): rename realpath to lrealpath 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 14:42:44 -07:00
Leonardo de Moura
bc4cef9ecb feat(build): clean-olean target deletes .olean and .d files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 14:01:13 -07:00
Leonardo de Moura
59f6cb5962 fix(build): delete incorrect/old .d and .olean files, detect errors when generating .d files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:48 -07:00
Leonardo de Moura
d5bb7d45ec fix(library/unifier): constraint priority in the unifier, and remove hack from if.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:47 -07:00
Leonardo de Moura
47d49643b0 feat(library/standard/logic/connectives/if): add more general if_congr theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:47 -07:00
Soonho Kong
d8ae285f93 fix(library/Makefile.common): clean remove olean/d files recursively 
[skip ci]
 2014-08-04 11:47:24 -07:00
Leonardo de Moura
94efd51fc5 chore(library/standard/logic/connectives/if): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 23:11:52 -07:00
Leonardo de Moura
c3f57cdb1c feat(library/standard/logic/classes): add 'by_contradiction' theorem for decidable propositions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 22:58:12 -07:00
Leonardo de Moura
ae2e0fd3dc feat(library/standard/logic/connectives/if): add 'if-then-else' congruence theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 21:41:01 -07:00
Leonardo de Moura
63d478c63f fix(tests/lua/hop1): incorrect assertion 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 20:06:50 -07:00
Leonardo de Moura
f3cb5f2f84 feat(library/standard/logic/connectives/quantifiers): add some theorems for simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 20:03:49 -07:00
Leonardo de Moura
552be37d48 feat(library/hop_match): port higher-order (pattern) matcher to Lean 0.2, we still have to implement support for universe levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 16:03:58 -07:00
Leonardo de Moura
2dca68e645 chore(util/list): add inline functions for commonly used patterns in list processing code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 13:51:38 -07:00
Leonardo de Moura
5611c6a0a0 chore(util/lean_path): workaround 'spurious' warning produced by g++ in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 13:28:05 -07:00
Leonardo de Moura
50b0c17092 feat(library/unifier): add more information in error messages due to type errors when assigning metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 09:49:30 -07:00
Leonardo de Moura
938b4e8421 test(tests/lean/run): add unicode in identifiers test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 20:05:46 -07:00