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

80 commits

Author SHA1 Message Date
Sebastian Ullrich
354439dd43 chore: bench C++ lines 2020-02-07 17:14:27 +01:00
Sebastian Ullrich
6cbb6c89ca chore: bench .olean byte size 2020-02-07 17:09:25 +01:00
Leonardo de Moura
bb1a90b24d chore: fix tests 2020-01-28 10:34:27 -08:00
Simon Hudon
92c8773137 feat: file IO using handles 2020-01-12 08:02:48 -08:00
Sebastian Ullrich
df3112d54d chore: fix one more benchmark 2019-11-25 12:47:42 +01:00
Sebastian Ullrich
fe3e8022a5 chore: update benchmarks 2019-11-25 10:42:14 +01:00
Leonardo de Moura
167549de59 chore: fix tests 2019-11-22 07:56:06 -08:00
Sebastian Ullrich
3dcd4febd9 feat: make LEAN_PATH a mapping from package names to root dirs, remove C++ impl 2019-11-20 16:39:53 +01:00
Sebastian Ullrich
ab42cffad2 refactor: rename all Default.lean files except for Init/Default.lean 2019-11-19 13:52:21 +01:00
Sebastian Ullrich
5c286ca6fd chore: bench cross suite: move default.nix and update README 2019-11-15 16:39:14 +01:00
Sebastian Ullrich
425230abc4 chore: fix cross bench suite 2019-11-15 16:39:14 +01:00
Sebastian Ullrich
a961e1314a chore: cross bench suite: fix fatal laziness in rbmap_checkpoint.hs 2019-11-15 16:39:14 +01:00
Sebastian Ullrich
ef9150cacd chore: cross bench suite: add Strict Haskell category (disabled by default) 
No change to slightly faster in general, except for a significant speedup in rbmap_10 that should be fixed in the lazy version
 2019-11-15 16:39:00 +01:00
Sebastian Ullrich
f2bc0b1c84 chore: add parser benchmark to speedcenter suite 2019-11-11 10:31:46 +01:00
Sebastian Ullrich
5a29922b6f chore: replace broken frontend benchmark with repeated parser benchmark on pinned Core.lean 2019-11-11 10:31:46 +01:00
Sebastian Ullrich
389f32e1c8 chore: bench/default.nix: fix and improve Lean building 2019-11-11 10:31:39 +01:00
Sebastian Ullrich
68a126be3f chore: update benchmark packages 2019-11-07 17:47:58 +01:00
Sebastian Ullrich
5ce9ca81da chore: revert "test: capture stderr as well" 
This reverts commit 2866824b51.
 2019-10-29 19:55:48 +01:00
Leonardo de Moura
ed3c95f892 chore: fix tests 2019-10-27 18:29:51 -07:00
Sebastian Ullrich
2866824b51 test: capture stderr as well 
This might or might not give more information on randomly failing tests on CI
/cc @leodemoura
 2019-10-15 17:36:28 +02:00
Leonardo de Moura
0714716477 fix: file and import names, tests and stage0 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2019-10-04 17:04:02 -07:00
Leonardo de Moura
e596089a2d chore: one module per import command 2019-10-04 12:27:47 -07:00
Leonardo de Moura
a8b39346d3 chore(tests/bench): fix tests 2019-10-02 10:07:26 -07:00
Sebastian Ullrich
941aeb113a chore(tests/bench/speedcenter.yaml): update temci config 2019-10-02 14:14:49 +02:00
Sebastian Ullrich
cae1009175 fix(library/init/data/list/aux): rename to basic_aux.lean 
`aux` is a reserved filename on Windows

/cc @leodemoura
 2019-10-02 12:30:29 +02:00
Leonardo de Moura
fdab3b90b9 refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
Leonardo de Moura
411f397654 refactor(library/init/data/list): new name convention for List functions 
cc @dselsam @kha
 2019-10-01 15:15:02 -07:00
Sebastian Ullrich
522cf13449 chore(tests/bench): update GHC and ocaml 2019-09-25 14:09:22 +02:00
Sebastian Ullrich
4b4f5c9832 test(tests/bench): further updates 2019-09-25 11:03:14 +02:00
Sebastian Ullrich
d3aa6488da chore(tests/bench): update cross suite 2019-09-24 22:42:25 +02:00
Leonardo de Moura
e5846934e6 chore(tests/bench/rbmap500k): add new test 2019-09-11 18:01:56 -07:00
Sebastian Ullrich
2110da4784 chore(tests/bench/speedcenter.exec.yaml): fix deriv speedcenter benchmark 2019-09-03 21:43:50 +02:00
Sebastian Ullrich
7b7f1d2cac test(tests/bench): add benchmarks as regular ctests with lowered inputs 2019-09-02 10:52:24 +02:00
Sebastian Ullrich
94b3de0130 chore(tests/bench): parameterize all benchmarks 2019-08-29 18:38:39 +02:00
Sebastian Ullrich
572926f5ce perf(shell/CMakeLists.txt, tests/): define NDEBUG in leanc release builds 
`assert` is now being used by the C runtime
 2019-08-27 16:54:29 +02:00
Sebastian Ullrich
8cc2f731cd chore(tests/bench/speedcenter.exec.yaml): fix again 2019-08-16 22:24:22 +02:00
Sebastian Ullrich
f1db7e8041 chore(tests/bench/speedcenter.exec.yaml): add "rbmap_10" benchmark 2019-08-16 19:11:01 +02:00
Sebastian Ullrich
7c84f522be chore(tests/bench/speedcenter.exec.yaml): fix hilariously broken "stdlib size: lines" benchmark 2019-08-16 19:11:01 +02:00
Sebastian Ullrich
a1a9daedce chore(tests/bench/report.py): go back to normalized tables 2019-08-15 14:24:23 +02:00
Sebastian Ullrich
5379636a94 chore(tests/bench): fix benchmarks 2019-08-10 12:52:42 +02:00
Sebastian Ullrich
3ed67138d5 chore(*): update equation syntax in files and old parser 
for f in ../../**/*.lean; do echo $f; ./patch.lean.out $f > tmp && cat tmp > $f; done
 2019-08-09 11:11:34 +02:00
Sebastian Ullrich
aef4a7159b chore(*): remove obsolete leanpkg.path files 2019-07-25 17:46:53 -07:00
Leonardo de Moura
b0d0cf973d chore(tests): fix tests 2019-07-25 17:44:25 -07:00
Sebastian Ullrich
11ba44ed8a chore(tests/bench): fix syntax 2019-07-19 10:46:02 +02:00
Leonardo de Moura
40943f84f3 chore(tests): fix tests 2019-07-17 10:46:35 -07:00
Leonardo de Moura
8944767f6c chore(frontends/lean): Π ==> ∀ 2019-07-07 08:13:40 -07:00
Sebastian Ullrich
3ee9371374 doc(tests/bench/README): update speedcenter URL 2019-07-05 16:23:07 +02:00
Sebastian Ullrich
a87591af40 chore(tests/bench/speedcenter.exec.yaml): stdlib: time imports 2019-07-05 15:54:35 +02:00
Sebastian Ullrich
2d60a4eb50 chore(tests/bench/speedcenter.exec.yaml): simplify 'stdlib' benchmark 
@leodemoura This removes the need for `--output-sync` and cmake hackery. It
doesn't quite measure actual `make stdlib` times (no parallelization, no
.olean/.cpp/.o output), but all of these actually seem to be negligible.
 2019-07-05 10:51:44 +02:00
Leonardo de Moura
ea6eee516b chore(frontends/lean): use => instead of := in match-expressions 
Motivation: use same separator used in lambda expressions as in
other programming languages.
 2019-07-04 11:38:38 -07:00