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

10964 commits

Author SHA1 Message Date
Sebastian Ullrich
a37dd02a41 perf(library/init/lean/frontend): do not hold on to outputs (syntax trees etc.) by default 2019-03-07 12:56:48 +01:00
Sebastian Ullrich
473e998ef6 chore(boot): update 2019-03-07 11:29:19 +01:00
Leonardo de Moura
ae95a3b6ef chore(boot): update 2019-03-06 17:27:40 -08:00
Leonardo de Moura
8e9b0d2799 fix(library/compiler): inferred types for stage2 declarations 2019-03-06 17:24:43 -08:00
Leonardo de Moura
89f692f548 chore(boot): update 2019-03-06 17:06:54 -08:00
Leonardo de Moura
35459664ad fix(library/compiler/emit_cpp): handle new unreachable terminal 2019-03-06 17:03:56 -08:00
Leonardo de Moura
515556a718 feat(library/init/lean/compiler/ir): add new terminal: unreachable 2019-03-06 17:00:50 -08:00
Leonardo de Moura
3e0c90d17d fix(frontends/lean/vm_elaborator): incorrect arity 2019-03-06 16:52:03 -08:00
Leonardo de Moura
110c727237 feat(library/compiler/llfn): rename to_llnf_fn => to_lambda_pure_fn, and make sure it produce valid terminal expressions 
A terminal must be a variable, jump or cases.
This commit also makes sure `explicit_boxing_fn` preserve valid terminals.
 2019-03-06 16:42:51 -08:00
Leonardo de Moura
b32ba9cb9d feat(library/compiler/compiler): add compiler trace option ll_infer_type 2019-03-06 14:53:27 -08:00
Leonardo de Moura
801f55faf0 chore(boot): update 2019-03-06 11:07:02 -08:00
Sebastian Ullrich
1ad5450853 perf(library/init/control/coroutine): mark as [inline_as_reduce] 2019-03-06 17:30:20 +01:00
Sebastian Ullrich
c17cabf58b chore(boot): update 2019-03-06 16:28:55 +01:00
Leonardo de Moura
5f46ca210d chore(boot): update 2019-03-06 07:09:57 -08:00
Leonardo de Moura
5e39a711fc chore(init/lean/ir): remove old IR 2019-03-06 07:04:47 -08:00
Leonardo de Moura
6defbf82bd feat(library/init/lean/compiler/ir): add meta data, fix names and declarations 
cc @kha
 2019-03-06 06:56:16 -08:00
Leonardo de Moura
53cbbd89b1 chore(util): remove dead code 2019-03-06 06:56:16 -08:00
Leonardo de Moura
818f2f2d4a chore(kernel): remove old #include 2019-03-06 06:56:16 -08:00
Leonardo de Moura
af039f420a chore(util): remove dead code 2019-03-06 06:56:16 -08:00
Sebastian Ullrich
00d9a1e76e chore(boot): update 2019-03-06 13:59:34 +01:00
Sebastian Ullrich
85bc52b9f2 feat(library/init/lean/frontend): profile frontend 2019-03-06 11:08:38 +01:00
Sebastian Ullrich
f2a161e5a9 feat(library/init/lean/util): Lean API for profiler 2019-03-06 10:37:38 +01:00
Leonardo de Moura
333ba43266 feat(runtime): statistics 
We can enabled runtime statistics by using cmake option `-D RUNTIME_STATS`.

cc @kha
 2019-03-05 16:01:06 -08:00
Leonardo de Moura
e067d82ab3 fix(library/compiler/llnf): nasty bug at explicit_rc_fn 
@kha I found this nasty bug today after I tried a small modification
at lean.parser.token. It is crazy that it didn't manifest itself before.
 2019-03-04 15:39:21 -08:00
Leonardo de Moura
3f50df70bc perf(library/init/lean/name): use hash code to speedup name.quick_lt 
We use the same trick in the C++ version of this function.

I measured the impact using `lean --new-frontend core.lean` and checking
the number of instructions executed reported by Valgrind.
Before:  4,891,642,264
After:   4,847,313,330
 2019-03-04 12:48:06 -08:00
Leonardo de Moura
7051099997 fix(runtime/object): performance bug 
The "quick" filter `&s1 != &s2` was incorrect.
It was actually always false, since it just comparing the stack address
of `s1` and `s2`.
I incorporated the quick filter into `string_eq`.

I measured the impact using `lean --new-frontend core.lean` and checking
the number of instructions executed reported by Valgrind.
Before: 5,210,225,530
After:  4,891,642,264

@kha
 2019-03-04 12:23:12 -08:00
Leonardo de Moura
9cc41c4f3d chore(frontends/lean/inductive_cmds): disable broken check 
@kha I have disabled this check. It was implemented 2 years ago by
Daniel, and I don't want to fix it. It seems you have already fixed a
bug there. AFAICT, this check is just for improving error messages.
I believe we may not even need it since the kernel now supports nested
inductive types. AFAIR, Daniel implemented this check here because the
inductive compiler was introducing a lot of auxiliary declarations
that were making the kernel error messages unreadable.
 2019-03-04 11:05:21 -08:00
Leonardo de Moura
2a0f5186e8 fix(runtime/object): bug at array_push 
Small object allocator was masking this bug.
 2019-02-26 14:19:37 -08:00
Leonardo de Moura
5635057549 feat(runtime/object): improve m_queue 2019-02-26 09:15:00 -08:00
Leonardo de Moura
f2ef0eb597 fix(runtime/alloc): bug at import_objs 2019-02-26 07:34:26 -08:00
Leonardo de Moura
a9458fdcb3 chore(runtime/alloc): remove incorrect assertion 2019-02-26 07:33:53 -08:00
Leonardo de Moura
f556423ae2 chore(library/compiler/llnf): add TODO 2019-02-25 17:43:21 -08:00
Leonardo de Moura
1f3de14f9c fix(runtime/object): embarrassing bug at del_core 2019-02-25 17:42:56 -08:00
Leonardo de Moura
3a252f5b55 chore(runtime/object): avoid overhead when SMALL_ALLOCATOR is disabled 2019-02-25 15:32:59 -08:00
Leonardo de Moura
0f9c52367d feat(library/equations_compiler/elim_match): prune equations occurring after equation that contains only pattern variables 2019-02-24 18:21:22 -08:00
Leonardo de Moura
e82632cbe4 chore(boot): update 2019-02-24 15:44:11 -08:00
Leonardo de Moura
2ff3899d62 fix(library/compiler/llnf): missing case at push_proj_fn 
We were not pushing projections over scalar projections.
 2019-02-24 15:39:53 -08:00
Leonardo de Moura
66b55d9d12 chore(CMakeLists.txt): add options for enabling/disabling LAZY_RC and SMALL_ALLOCATOR 2019-02-24 15:11:48 -08:00
Leonardo de Moura
67d197a2e0 fix(runtime/object): correct support for objects without RC 
Lean was not crashing because we do not have region objects yet, and
the persistent objects still have a RC.
 2019-02-24 09:29:20 -08:00
Leonardo de Moura
935d90e77c chore(runtime/object): disable lazy RC to collect data at speedcenter 2019-02-23 17:37:11 -08:00
Leonardo de Moura
abd0f89820 feat(runtime): avoid extra switch 2019-02-23 17:35:21 -08:00
Leonardo de Moura
4b44c5ce36 feat(runtime/object): small object allocator 2019-02-23 17:17:56 -08:00
Leonardo de Moura
a9276c8834 fix(runtime/object): incorrect { 2019-02-23 17:16:49 -08:00
Leonardo de Moura
61f06fbf8e chore(boot): update 2019-02-23 09:16:29 -08:00
Leonardo de Moura
313fd69e8c feat(library/compiler/borrowed_annotation): mark objects as owned when stored in constructors 
@kha
 2019-02-23 09:12:53 -08:00
Leonardo de Moura
b971db6c11 chore(boot): update 2019-02-22 16:09:48 -08:00
Leonardo de Moura
d23216e3ee fix(library/compiler/llnf): bug at explicit_rc_fn 2019-02-22 16:01:52 -08:00
Leonardo de Moura
07aa990f22 fix(library/compiler/borrowed_annotation): ensure that exported functions do not take borrowed arguments 
In the future, we should automatically generate wrappers that make all
adjustments for us.
 2019-02-22 15:32:30 -08:00
Leonardo de Moura
b1b75c7c2e feat(library/compiler): borrow inference procedure 2019-02-22 15:23:42 -08:00
Leonardo de Moura
ba43d355b7 feat(library/compiler): add borrowed annotation inference skeleton 2019-02-22 11:14:38 -08:00