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

4213 commits

Author SHA1 Message Date
Leonardo de Moura
6083bde3bc chore(tests/playground/deriv): add example for testing in the playground 2019-02-14 10:49:46 -08:00
Leonardo de Moura
b6d1506434 fix(tests/compiler/t2): pause at the end 
@kha I figured out why we had a long pause in the end of this benchmark
when using `11` instead of `9`. The function `deriv` was computing
`d := d "x" f` (the expensive computation), printing the size of `f` and
returning `d`. So, in the last step we were quickly printing the size
of the input 40230090 (when using `nest deriv 11 f`), and then computing
`d := d "x" f` which returns an object of size 374429936 which is never
used for anything.
That is, the pause had nothing to do with memory deallocation. I found
this issue after I implemented the deferred free feature which did not
fix the pause :)
 2019-02-14 10:44:59 -08:00
Leonardo de Moura
1716f1f6c9 test(tests/playground/perf): performance test 
On my macbook,
- with default kind STHeap: 3.15 secs
- with default kind MTHeap: 3.75 secs

@cc kha
 2019-02-14 08:43:04 -08:00
Leonardo de Moura
6f852cf7af feat(tests/playground): add run.sh script for running tests 
@kha I have added `timeit` for running experiments for the paper.
We have to be careful because `timeit` may produce incorrect results
due to compiler optimizations (e.g., ground term extraction).
Here are examples that do not produce the result we expect:

```
def main : io uint32 :=
timeit "tst" (io.println' ("result " ++ to_string (tst 1000000))) *>
pure 0
```

```
def main (xs : list string) : io uint32 :=
timeit "tst" (io.println' ("result " ++ to_string (tst xs.head.to_nat))) *>
pure 0
```
 2019-02-13 17:17:14 -08:00
Leonardo de Moura
19e111c2ff feat(library/compiler): allow main function to also have type io uint32 2019-02-13 16:29:10 -08:00
Leonardo de Moura
06bb9b7ea8 test(tests/compiler): add simple test for expr 2019-02-13 16:22:01 -08:00
Sebastian Ullrich
534b507aff feat(library/init/lean/frontend): rework error reporting 2019-02-12 13:34:32 +01:00
Leonardo de Moura
7e8f9e6f66 feat(library/compiler): add [extern] attribute 2019-02-09 18:53:44 -08:00
Sebastian Ullrich
67f8f7a2da chore(tests/compiler/append): add expected output 2019-02-09 20:02:26 +01:00
Leonardo de Moura
6cb96331b1 chore(tests/compiler): add .gitignore 2019-02-08 16:59:17 -08:00
Leonardo de Moura
5dcbb9c50d test(tests/compiler/append): append test 2019-02-08 16:52:41 -08:00
Leonardo de Moura
01119b529f test(tests/compiler): add thunk test 
This test will take a long time if `thunk` result is not cached.
 2019-02-08 11:01:33 -08:00
Leonardo de Moura
e2ee2d4bd9 chore(tests/compiler): add deriv test 2019-02-07 16:56:40 -08:00
Leonardo de Moura
259941c184 chore(tests/compiler/test_flags): include release flags 
@kha The `-O3` option is not at CMAKE_CXX_FLAGS, but in build mode
specific configuration. I added this hack because I want to include
performance tests too. Perhaps, I should move performance tests to a
different directory.
 2019-02-07 16:30:30 -08:00
Leonardo de Moura
109d569310 feat(tests/compiler): add first test 2019-02-07 12:14:25 -08:00
Leonardo de Moura
dc8edd3894 feat(tests/compiler): script skeleton 
cc @kha
 2019-02-07 11:54:46 -08:00
Sebastian Ullrich
4c0f836305 chore(shell/lean): reduce lean interface to taking a single file, assuming all dependencies have already been built 2019-01-25 18:27:38 +01:00
Sebastian Ullrich
9f90dbfd3d feat(library/init/lean/parser/syntax): improve syntax.get_pos for more error positions 2019-01-22 11:16:00 +01:00
Sebastian Ullrich
69e363446d fix(library/init/lean/{parser/term,elaborator}): local notations override previous notations 2019-01-20 16:25:15 +01:00
Leonardo de Moura
c3dfb613d5 test(tests/lean/run/rc_tests): basic explicit_rc_fn tests 2019-01-17 15:25:27 -08:00
Sebastian Ullrich
3611eda136 fix(frontends/lean/vm_elaborator): message order 2019-01-17 19:57:00 +01:00
Sebastian Ullrich
3d66e7dbe1 fix(library/pos_info_provider): row and column were swapped 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
5660a8e690 feat(library/init/lean/elaborator): transmit position information 2019-01-15 18:28:35 +01:00
Sebastian Ullrich
9ac41835ba test(tests/lean/parser1): add some name resolution tests 2019-01-06 18:22:18 +01:00
Sebastian Ullrich
32a3c0e62e feat(library/init/lean/frontend,bin/lean-bootstrapped): expose new frontend as executable 2018-12-20 14:28:18 +01:00
Sebastian Ullrich
0911d16bc3 feat(library/init/lean): compute and show error positions 2018-12-20 14:28:18 +01:00
Sebastian Ullrich
e5aaf391ff fix(library/init/lean/parser/syntax): macro_scopes.flip 2018-12-19 15:04:48 +01:00
Sebastian Ullrich
1d524476b7 chore(tests/lean/parser1): restore #exit... 2018-12-12 11:06:52 +01:00
Sebastian Ullrich
94dec2cb9f feat(library/init/lean/elaborator): elaborate universe 2018-12-11 19:01:41 +01:00
Sebastian Ullrich
11e5d1a8a2 chore(tests/lean/parser1): reintroduce #exit in front of core.lean test 2018-12-06 13:23:25 +01:00
Sebastian Ullrich
143ac0e58a feat(library/init/lean/expander): also normalize bracketed binders in e.g. declarations 2018-12-06 13:23:12 +01:00
Sebastian Ullrich
58def30036 chore(tests/lean/parser1): clearly delimit components in profiler output 2018-12-04 12:31:13 +01:00
Leonardo de Moura
607d22ae58 fix(library/compiler/csimp): bug at float_cases_on_core 
The bug occurs when floating `cases_on` application in code of the form
```
let x := C.cases_on ...
in t
```
and when the type of `t` depends on `x`.
The issue here is that the `x` declaration disappears after the float, but the resulting type still depends on it.
We fix the bug by replacing `x` with its value in the type.

cc @kha
 2018-11-30 11:40:41 -08:00
Sebastian Ullrich
fd121f03bd feat(library/init/lean/expander): make set of transformers configurable 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
222fff8862 refactor(library/init/lean/elaborator): introduce simple lambda binder 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
6d0b3afa7e fix(library/compiler/compiler): do not silently abort on user-given sorrys 2018-11-17 18:00:55 +01:00
Leonardo de Moura
04227701d6 chore(tests/lean/run): fix the tests 
@kha I found the real issue with these two tests.
You have modified the compiler to ignore definitions containing `sorry` :)
 2018-11-15 11:21:12 -08:00
Leonardo de Moura
d0ccaa1083 chore(tests/lean): fix tests 
TODO: `io` modifications performed yesterday may have affected `eval`.
 2018-11-15 10:56:03 -08:00
Leonardo de Moura
c0ac39f7f0 chore(tests/lean/parser1): fix test output 2018-11-12 08:53:57 -08:00
Sebastian Ullrich
bd70dc1fc9 perf(library/init/lean/parser): move backtrackable state from parser_core_t to module_parser_m 2018-11-08 15:58:41 +01:00
Sebastian Ullrich
41f4a34d4b feat(library/init/lean/parser/token): cache hit statistics 2018-11-08 14:52:54 +01:00
Sebastian Ullrich
0026b59a88 fix(tests/lean/macro_scopes): expected output 2018-11-07 09:11:49 +01:00
Leonardo de Moura
f404c5c446 refactor(library/init/data): make sure uint* and usize are irreducible 
Remark: this commit breaks the support for `uint*` and `usize` in the old VM.
 2018-11-06 16:55:02 -08:00
Sebastian Ullrich
5a286f5e46 test(tests/lean/macro_scopes): macro scopes propagation test 2018-11-06 17:33:16 +01:00
Sebastian Ullrich
090c4c0ce7 feat(library/init/lean/syntax): add lazily propagated macro scopes to syntax_node 2018-11-06 16:46:50 +01:00
Sebastian Ullrich
dcb7566e53 fix(tests/lean/parser1): fix test 2018-11-05 17:40:11 +01:00
Leonardo de Moura
189b037358 chore(tests/lean/run/new_compiler): fix test 2018-10-31 13:25:01 -07:00
Sebastian Ullrich
93fc1fd1de fix(library/init/lean/parser/combinators): node: do not wrap error in first argument 2018-10-30 17:43:05 +01:00
Leonardo de Moura
28a34e798a feat(library/compiler/csimp): projection to field 
The new test demonstrations this transformation.
 2018-10-28 09:38:45 -07:00
Leonardo de Moura
392f019184 chore(tests/lean/parsec1): fix test 2018-10-23 12:54:29 -07:00