Sebastian Ullrich
|
febeaad5bb
|
feat(lean4-mode/lean4-flycheck): store .olean of dependencies
|
2018-09-11 16:35:25 -07:00 |
|
Sebastian Ullrich
|
52d4cc10ad
|
feat(shell/lean,lean4-mode/lean4-flycheck): use stdin for communication
no more `flycheck_` files
|
2018-09-11 16:35:25 -07:00 |
|
Leonardo de Moura
|
81545c12f2
|
chore(runtime/object): fix comment
|
2018-09-11 14:31:14 -07:00 |
|
Leonardo de Moura
|
46d6f7bfb5
|
chore(runtime/object): store function pointer as void * inside closure
|
2018-09-11 14:27:45 -07:00 |
|
Leonardo de Moura
|
e8fa692611
|
chore(runtime/object): change default object_memory_kind to STHeap
|
2018-09-11 13:57:55 -07:00 |
|
Leonardo de Moura
|
3feae112bc
|
chore(frontends/lean/parser): unused var warning
|
2018-09-11 13:55:44 -07:00 |
|
Leonardo de Moura
|
efb33ac0a7
|
chore(library/init/env_ext): update
|
2018-09-11 13:55:25 -07:00 |
|
Leonardo de Moura
|
6914d35062
|
chore(library/compiler/preprocess): dead trace option
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
78ced9ffcf
|
refactor(library/module_mgr): minimize parser interface
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
43e57358af
|
refactor(library/module_mgr): minor refactorings
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
af99f153f8
|
refactor(library/module{,_mgr},frontends/lean/parser): use absolute module names everywhere for identifying modules, move actual importing from parser to module_mgr
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
716de48078
|
chore(library/module): remove loaded_module.m_env
It was used by `--run` only, which I guess will change quite a bit anyway
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
904d7c4a88
|
chore(*): remove old task API and task queues
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
af55cb13e7
|
fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
38208802c6
|
refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
99ab0e9d67
|
refactor(library/messages): make an object_ref
|
2018-09-11 13:55:25 -07:00 |
|
Leonardo de Moura
|
7c7eccf6ad
|
test(tests/util/object): add perf test
|
2018-09-11 08:27:25 -07:00 |
|
Leonardo de Moura
|
0691d43153
|
feat(library/init/lean/parser/basic): define trie using rbnode (char × trie) nested inductice type
|
2018-09-09 18:19:28 -07:00 |
|
Leonardo de Moura
|
4e6748b55b
|
feat(library/init/data/rbmap/basic): add rbmap_core low level functions
|
2018-09-09 18:18:40 -07:00 |
|
Leonardo de Moura
|
5bc9b07ab9
|
feat(runtime/object): split Heap into MTHeap and STHeap
|
2018-09-09 14:46:28 -07:00 |
|
Leonardo de Moura
|
0573d7e1d5
|
fix(runtime/object): parray RC bugs
|
2018-09-09 12:04:27 -07:00 |
|
Leonardo de Moura
|
b45ac3fcc0
|
chore(runtime/object): minor
|
2018-09-09 10:59:36 -07:00 |
|
Leonardo de Moura
|
36423e4389
|
fix(runtime): parray memory leaks
|
2018-09-09 10:33:15 -07:00 |
|
Leonardo de Moura
|
2a24f4a09b
|
test(tests/util/object): add parray test
|
2018-09-09 10:21:55 -07:00 |
|
Leonardo de Moura
|
4863ca071a
|
chore(runtime): make sure we use the same naming convention for getters and setters
|
2018-09-09 10:07:00 -07:00 |
|
Leonardo de Moura
|
8f195515a6
|
feat(runtime): add persistent arrays to runtime
|
2018-09-09 09:44:38 -07:00 |
|
Sebastian Ullrich
|
a7b1de8bf7
|
chore(tests/shell/test): remove
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
0d865b37dd
|
feat(library/init/lean/{message,parser}): enhance lean.message
Small regression: order of messages flipped, should eventually be sorted by
position
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
845c496a07
|
fix(lean4-mode/lean4-util): (lean4-setup-rootdir) returns the wrong path
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
1a4a69679d
|
chore(lean4-mode): rename files
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
11f8e24136
|
chore(lean4-mode): change lean- prefixes to lean4-
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
f2cb01bbf0
|
chore(lean-mode): rename to lean4-mode
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
f2f4022420
|
feat(lean-mode): use --json batch mode instead of --server
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
7d5a52299e
|
feat(lean-mode): embed for the time being
|
2018-09-08 18:37:58 -07:00 |
|
Sebastian Ullrich
|
b3c44ec56e
|
chore(shell/{server,lean_js}): remove
|
2018-09-08 18:37:58 -07:00 |
|
Leonardo de Moura
|
03a99986bb
|
feat(kernel): implement local_decl using runtime
|
2018-09-08 16:25:43 -07:00 |
|
Leonardo de Moura
|
f5ac6875a6
|
chore(frontends/lean/json): style
|
2018-09-08 16:23:48 -07:00 |
|
Leonardo de Moura
|
3b07eeec47
|
fix(kernel/inductive): name generator was not being consistenly used
|
2018-09-08 16:21:33 -07:00 |
|
Leonardo de Moura
|
81a694e73c
|
chore(frontends/lean): remove dead code
|
2018-09-08 15:44:49 -07:00 |
|
Leonardo de Moura
|
fabfe32ca5
|
chore(*): remove unnecessary scoped_ext dependencies
|
2018-09-08 15:42:48 -07:00 |
|
Leonardo de Moura
|
1d5529389a
|
chore(util/name_generator): add explicit
|
2018-09-08 15:42:48 -07:00 |
|
Leonardo de Moura
|
bb96f184ee
|
chore(library): remove dead code
|
2018-09-08 15:34:30 -07:00 |
|
Leonardo de Moura
|
5503bd113b
|
chore(kernel/type_checker): assume m_cache != nullptr will continue to hold in future versions
|
2018-09-08 09:13:08 -07:00 |
|
Leonardo de Moura
|
7479d6e55b
|
refactor(kernel/type_checker): allow type_checker::cache to be reused
|
2018-09-08 08:43:19 -07:00 |
|
Leonardo de Moura
|
dacc4c9cd6
|
chore(kernel): move abstract_type_context to library
|
2018-09-08 08:29:51 -07:00 |
|
Leonardo de Moura
|
3e5f59d6df
|
chore(kernel): remove expr.quote constructor
In Lean4, we will reify expressions.
|
2018-09-07 22:08:08 -07:00 |
|
Leonardo de Moura
|
4ddd915886
|
chore(kernel): remove dummy file
|
2018-09-07 21:43:15 -07:00 |
|
Leonardo de Moura
|
aa3292eb36
|
feat(kernel/type_checker): remove m_memoize
It is always `true`
|
2018-09-07 20:50:53 -07:00 |
|
Leonardo de Moura
|
13fbd8304e
|
chore(library,frontends/lean): use is_constructor, is_recursor, is_inductive helper functions
They do not throw exception if the constant is not declared in the environment.
|
2018-09-07 20:36:42 -07:00 |
|
Leonardo de Moura
|
88d4a1b0cd
|
feat(kernel/inductive): inductive_reduce_rec should not throw exception when it finds an unknown constant
It should just fail to reduce. This is important when using it in the elaborator.
|
2018-09-07 17:34:54 -07:00 |
|