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

15800 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
3b06c52d4f test(tests/playground/Makefile): re-add original ocamlopt parameters 
This reverts commit 8e212ef9d9.
 2019-03-05 15:44:42 +01:00
Sebastian Ullrich
069c07fa39 test(tests/playground/Makefile): update 2019-03-05 15:44:39 +01:00
Sebastian Ullrich
90a058a655 test(tests/playground/Makefile): bench fallback, all Lean tests 2019-03-05 15:44:03 +01:00
Sebastian Ullrich
467799c6c3 test(tests/playground/run.sh): fix 2019-03-05 15:37:11 +01:00
Leonardo de Moura
ed4cd39d59 feat(library/init/lean/compiler/ir): new IR for Lean 
It is currently implemented in C++. The plan is to move the procedures
for inserting inc/dec, reset/reuse, and inferring borrow inferences to
Lean. Another goal is to make sure new IR optimizations can be
implemented in Lean, and to avoid backend optimizations that would
have to be duplicated in each backend (e.g., `emit_proj_inc_reset_seq`
at `emit_cpp.cpp`).

cc @kha
 2019-03-04 16:46:10 -08:00
Leonardo de Moura
e5950cf710 test(tests/playground/gen): simple lean file generator 
@kha
I am using this little program to generate big lean files to test the
new front end. For the output produced for `gen 5000`, the new frontend
is almost 10x slower than the old one.
I used `valgrind --tool=callgrind` to collect profiling data.
The number of closures is too big. For example, `free_closure_obj` was
invoked 38.5 million times. The total number of deallocated objects is around
49.5 million.
 2019-03-04 16:19:50 -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
Sebastian Ullrich
5e7970dca3 test(tests/playground/deriv): Haskell version 2019-02-28 14:57:57 +01:00
Leonardo de Moura
b25c0db35d tests(tests/playground/deriv): deriv in OCaml 2019-02-27 11:15:52 -08:00
Leonardo de Moura
f4302a5f48 test(tests/playground): new versions of unionfind1 
@kha I'm just trying to understand the performance numbers.
 2019-02-26 16:47:53 -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
d128af10f9 test(tests/playground): add union find examples 
@kha I tried to make the examples self contained.

- unionfind1.lean uses the modified StateT and ExceptT
- unionfind2.lean uses the standard StateT and ExceptT
 2019-02-26 13:44:16 -08:00
Sebastian Ullrich
f366af76ac test(tests/playground/rbmap): consistent naming 2019-02-26 20:27:23 +01:00
Sebastian Ullrich
850001b996 test(tests/playground): rbmap.hs, Makefile 2019-02-26 20:26:55 +01:00
Sebastian Ullrich
c4bc783ef4 test(tests/playground/run.sh): split out compile.sh 2019-02-26 20:25:30 +01:00
Leonardo de Moura
6f73f19d19 chore(tests/playground/rbmap_standalone): make sure lean version mirrors the OCaml one 2019-02-26 10:37:12 -08:00
Leonardo de Moura
b883388d66 chore(tests/playground/rbmap_standalone): add missing [specialize] and remove alias 2019-02-26 10:06:18 -08:00
Leonardo de Moura
397be6d1c0 test(tests/playground/rbmap_standalone): add standalone rbmap benchmark 2019-02-26 09:56:59 -08:00
Leonardo de Moura
5635057549 feat(runtime/object): improve m_queue 2019-02-26 09:15:00 -08:00
Sebastian Ullrich
d258f325f1 test(tests/playground/binarytrees.lean): further opt 2019-02-26 18:08:09 +01:00
Sebastian Ullrich
24ad2e2b89 test(tests/playground/binarytrees.lean): optimize 2019-02-26 17:47:14 +01:00
Sebastian Ullrich
8e212ef9d9 test(tests/playground/Makefile): these ocamlopt parameters do nothing 2019-02-26 17:26:37 +01:00
Sebastian Ullrich
70a5c6d585 test(tests/playground/binarytrees.lean): more coarse parallelization 2019-02-26 17:21:45 +01: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
Sebastian Ullrich
9724491dc2 test(tests/playground/binarytrees.lean): parallelize 2019-02-26 16:16:34 +01: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
Sebastian Ullrich
cf0bf911c8 test(tests/playground): binarytrees benchmarks game benchmark in Lean, OCaml & Haskell 2019-02-25 23:46:10 +01:00
Sebastian Ullrich
c4740b7295 test(tests/playground/rbmap.ml): take the same input as Lean version 2019-02-25 14:51:16 +01: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
ccea4c2043 chore(tests/playground/rbmap): use +1 instead of +k to avoid big number arithmetic when we increase number of elements inserted 2019-02-24 08:49:38 -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
483125f828 test(tests/playground/rbmap): rbmap in OCaml 2019-02-22 17:43:27 -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