Leonardo de Moura
|
002ffc81bb
|
fix(tests/shared/univ): memory access violation
|
2017-02-12 16:29:13 -08:00 |
|
Leonardo de Moura
|
4fdd512636
|
fix(tests/shared/univ): bus error on OSX
|
2017-02-11 09:27:46 -08:00 |
|
Leonardo de Moura
|
32e6442d0a
|
feat(frontends/lean): no global universes in the frontend
|
2017-02-08 17:23:04 -08:00 |
|
Leonardo de Moura
|
01414cf21c
|
feat(frontends/lean): add token class, and procedure for consuming the tokens
|
2017-02-03 18:11:06 -08:00 |
|
Gabriel Ebner
|
61804eb8e9
|
chore(util/sexpr): remove mpz and mpq cases
|
2017-01-31 09:39:31 +01:00 |
|
Leonardo de Moura
|
52164d56b9
|
chore(tests/shell/shell): style
|
2017-01-13 07:39:06 -08:00 |
|
Sebastian Ullrich
|
b180c54c0e
|
feat(shell): move lean.js to server mode
|
2017-01-13 07:34:54 -08:00 |
|
Gabriel Ebner
|
2867163db0
|
fix(tests): initialize util module
|
2016-12-08 13:11:53 -08:00 |
|
Gabriel Ebner
|
60f0f30c5c
|
fix(tests/shared/thread): fix single-threaded build
|
2016-12-08 07:13:48 -08:00 |
|
Leonardo de Moura
|
f9a0029a47
|
chore(tests/util/thread): enable test on OSX
|
2016-12-05 09:24:17 -08:00 |
|
Leonardo de Moura
|
79d87138f0
|
feat(util/memory): simplify memory tracking code
|
2016-12-01 16:07:46 -08:00 |
|
Gabriel Ebner
|
d8ee8d6ea7
|
fix(tests/util/exception): adapt to changed superclass of interrupted
|
2016-11-29 11:12:44 -08:00 |
|
Gabriel Ebner
|
a8df381d20
|
feat(*): parallel compilation
|
2016-11-29 11:12:40 -08:00 |
|
Leonardo de Moura
|
7da0acc3fd
|
chore(src/tests/util): fix gcc 6.2 warnings
|
2016-11-07 14:38:33 -08:00 |
|
Gabriel Ebner
|
888609013f
|
feat(tests): run tests in emscripten build
|
2016-10-16 14:41:35 -07:00 |
|
Gabriel Ebner
|
6d7cf7bace
|
fix(tests/shell): fix build
|
2016-10-16 14:41:35 -07:00 |
|
Gabriel Ebner
|
ec0aa6d248
|
refactor(*): integrate emscripten build
|
2016-10-16 14:41:35 -07:00 |
|
Leonardo de Moura
|
e9ef7d1342
|
chore(util/parray): remove dead code
|
2016-10-03 19:09:57 -07:00 |
|
Leonardo de Moura
|
e5ba0d7733
|
chore(*): cleanup
|
2016-09-27 17:30:57 -07:00 |
|
Leonardo de Moura
|
9ef3ebbd5b
|
refactor(*): delete HoTT support
|
2016-09-27 16:33:39 -07:00 |
|
Leonardo de Moura
|
da27454c8c
|
chore(util): remove dead code
|
2016-09-23 14:29:13 -07:00 |
|
Leonardo de Moura
|
dde5f7ac70
|
feat(frontends/lean): add aliases such as: .1 for ~>1
|
2016-09-21 11:32:02 -07:00 |
|
Leonardo de Moura
|
465f898882
|
chore(library): remove lean2 old type checker
|
2016-09-19 22:21:19 -07:00 |
|
Leonardo de Moura
|
f7df7dc9a7
|
refactor(kernel): add reducibility_hints
|
2016-09-04 16:30:02 -07:00 |
|
Leonardo de Moura
|
a93eada058
|
feat(library/type_context): improved (and simplified) cache management for type_context
|
2016-08-23 17:56:58 -07:00 |
|
Leonardo de Moura
|
803c956d18
|
feat(util/sexpr/option_declarations): allow options to be registered after initialization
|
2016-08-19 16:58:30 -07:00 |
|
Leonardo de Moura
|
f3dbd0c69a
|
chore(library): disable stdlib but init and systems folder
|
2016-08-11 18:42:10 -07:00 |
|
Leonardo de Moura
|
5b0100ef0b
|
refactor(library/lazy_abstraction): lazy ==> delayed
|
2016-07-27 13:53:17 -07:00 |
|
Leonardo de Moura
|
4f3ce09b57
|
fix(library/type_context,library/lazy_abstraction): bug in lazy_abstraction, and handle lazy_abstraction in type inference
|
2016-06-25 14:47:30 -07:00 |
|
Leonardo de Moura
|
989dbcb265
|
chore(tests): fix some C++ unit tests
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
d302514933
|
chore(frontends/lean): remove tactic notation
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
83f64ef8b3
|
chore(util): remove dead code
|
2016-06-02 18:38:07 -07:00 |
|
Lev Nachmanson
|
c2d795e46a
|
dev(lp): integrate with z3
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
|
2016-06-02 11:51:07 -07:00 |
|
Leonardo de Moura
|
53811822d4
|
chore(*): style
|
2016-05-25 18:10:15 -07:00 |
|
Leonardo de Moura
|
7641b602ca
|
chore(util): fun_array ==> parray
|
2016-05-10 16:05:41 -07:00 |
|
Leonardo de Moura
|
6cb8e82fef
|
feat(util/fun_array): add functional array
|
2016-05-09 17:40:26 -07:00 |
|
Leonardo de Moura
|
4728b03f20
|
refactor(kernel/type_checker): do not use definitional depth in the kernel type checker
|
2016-04-11 14:53:02 -07:00 |
|
Leonardo de Moura
|
a6b112d3b2
|
fix(tests/library/occurs): compilation error
|
2016-03-25 14:10:07 -07:00 |
|
Leonardo de Moura
|
487a1e7f89
|
refactor(kernel): remove extension_context
We replaced it with abstract_type_context
|
2016-03-19 15:15:39 -07:00 |
|
Leonardo de Moura
|
63d8a0ed45
|
refactor(kernel): move justification/constraint/metavar to library
These files will be eventually deleted
|
2016-03-19 14:39:15 -07:00 |
|
Leonardo de Moura
|
e7f1f409c4
|
refactor(kernel): simplify kernel type_checker
TODO: cleanup, move justification/metavar/constraints to library
|
2016-03-18 16:28:42 -07:00 |
|
Leonardo de Moura
|
c8e5907b70
|
feat(util/rb_tree,util/rb_map): add back_find_if
|
2016-03-05 13:29:34 -08:00 |
|
Leonardo de Moura
|
4a43e33d45
|
chore(*): disable big chunk of the standard library and tests
|
2016-03-03 13:43:08 -08:00 |
|
Leonardo de Moura
|
82fb38b440
|
feat(util/rb_tree): add for_each_greater
|
2016-03-01 15:42:27 -08:00 |
|
Leonardo de Moura
|
3c878ecd01
|
feat(kernel): add let-expressions to the kernel
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
|
2016-02-29 16:40:17 -08:00 |
|
Lev Nachmanson
|
23079a75a7
|
dev(lp): fix build for clang, avoid clang-3.3 bug, cleanup permutation_matrix
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
|
2016-02-26 16:07:16 -08:00 |
|
Leonardo de Moura
|
7d61f640f6
|
refactor(*): add abstract_type_context class
|
2016-02-26 14:17:34 -08:00 |
|
Leonardo de Moura
|
c9e9fee76a
|
refactor(*): remove name_generator and use simpler mk_fresh_name
|
2016-02-11 18:05:57 -08:00 |
|
Leonardo de Moura
|
9cbda49297
|
chore(frontends/lean): remove script blocks
|
2016-02-11 17:26:44 -08:00 |
|
Leonardo de Moura
|
f67181baf3
|
chore(*): remove support for Lua
|
2016-02-11 17:17:55 -08:00 |
|