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

10988 commits

Author SHA1 Message Date
Leonardo de Moura
01b4983fa2 fix(runtime/object): string_utf8_extract 2019-03-09 12:57:51 -08:00
Leonardo de Moura
ab73553bf2 chore(boot): update 2019-03-09 12:40:43 -08:00
Leonardo de Moura
c862ce4a75 feat(runtime, library/init/data/string/basic): add utf8_pos 
`utf8_pos` is a low level alternative for `string.iterator`.
TODO: implement `string.iterator` using it.
 2019-03-09 12:30:19 -08:00
Leonardo de Moura
402034df1f chore(library/init/data): move usize to uint 2019-03-09 10:32:23 -08:00
Leonardo de Moura
2032b10482 feat(library/init/data): bitwise operations 2019-03-09 10:19:35 -08:00
Leonardo de Moura
d2ef708763 feat(library/compiler/ll_infer_type): _unreachable 2019-03-09 07:49:51 -08:00
Leonardo de Moura
8799056607 chore(boot): update 2019-03-08 12:13:06 -08:00
Leonardo de Moura
b43ebab32c fix(library/compiler/specialize): we should not lambda abstract join points 2019-03-08 11:54:51 -08:00
Leonardo de Moura
7b1d15ec43 fix(library/compiler/specialize): avoid work duplication in the specializer 2019-03-08 11:21:49 -08:00
Sebastian Ullrich
6a96d94259 chore(boot): update 2019-03-08 17:26:02 +01:00
Sebastian Ullrich
ef7053dac9 chore(boot): update 2019-03-08 17:05:42 +01:00
Sebastian Ullrich
0580ce7cfa chore(boot): update 2019-03-08 15:34:37 +01:00
Leonardo de Moura
9962441b7b chore(boot): update 2019-03-07 15:44:43 -08:00
Leonardo de Moura
29770d73b3 chore(boot): update 2019-03-07 12:49:53 -08:00
Leonardo de Moura
67f4698593 feat(library/compiler): do not generate code for decls that have irrelevant types 
We were generating hundreds of definitions that just return
`lean::box(0)`.
 2019-03-07 12:48:16 -08:00
Leonardo de Moura
057d90b7ff chore(runtime/object): track number of external objects allocated 2019-03-07 12:31:05 -08:00
Leonardo de Moura
06be451110 chore(boot): update 2019-03-07 11:30:51 -08:00
Leonardo de Moura
9fc813e601 fix(library/compiler/llnf): polymorphic projection resulting type 2019-03-07 11:24:08 -08:00
Leonardo de Moura
4744d12e38 chore(boot): update 2019-03-07 10:26:05 -08:00
Leonardo de Moura
b5b2adea49 refactor(runtime): proper external objects without vtable 
A C++ vtable at `external_object` is bad because it prevents users
from implementing external object in different programming languages.

Another problem was memory leaks because of the vtable in the
beginning of the object.

cc @kha
 2019-03-07 10:26:05 -08:00
Leonardo de Moura
2984d6838c chore(library/compiler/ll_infer_type): dead variable 2019-03-07 10:21:14 -08:00
Sebastian Ullrich
1e248013f7 chore(runtime/alloc): don't init heap if LEAN_SMALL_ALLOCATOR is off 
makes tracking down leaks a bit nicer
 2019-03-07 15:52:06 +01:00
Sebastian Ullrich
35be90b3a1 chore(boot): update 2019-03-07 15:51:55 +01:00
Sebastian Ullrich
430fb81f69 fix(library/init/lean/parser/term,frontends/lean/builtin_exprs): @& should have higher rbp than -> 2019-03-07 14:35:25 +01:00
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