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

15573 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
efe64cb2d3 feat(library/init/data/list/basic): tail recursive length 2019-02-08 16:51:44 -08:00
Leonardo de Moura
2d55c3f73c chore(boot): update 2019-02-08 16:44:17 -08:00
Leonardo de Moura
a4f305a443 fix(library/compiler/export_name): allow constructors to be exported with a different name 2019-02-08 16:36:08 -08:00
Leonardo de Moura
4734e55f6d feat(library/init/data): tail recursive append 2019-02-08 16:35:20 -08:00
Leonardo de Moura
4ce415cbde chore(boot): update 2019-02-08 11:12:13 -08:00
Leonardo de Moura
b09be6d0a5 fix(library/compiler/emit_cpp): missing { } 2019-02-08 11:06:29 -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
afc2569f7c fix(library/init/data/nat/basic): tail recursive nat.repeat 2019-02-08 11:00:48 -08:00
Leonardo de Moura
4339afc802 chore(library/compiler): [extname] ==> [export] 2019-02-08 10:25:21 -08:00
Max Wagner
3164801a83 fix(library/vm): unary op dummies copy-paste error 2019-02-08 09:56:20 -08:00
Max Wagner
e663f75fb2 chore(library/compiler): move builtins into the environment 2019-02-08 09:56:03 -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
bd38fc530f refactor(kernel/level): low level API for level 2019-02-07 15:04:12 -08:00
Leonardo de Moura
ba449aa9f4 chore(library/compiler/llnf): fix compilation warning 2019-02-07 15:02:26 -08:00
Leonardo de Moura
7f11846068 feat(CMakeLists): invoke tests 2019-02-07 12:19:05 -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
Leonardo de Moura
bfbfe94ac9 chore(library/init/control/default): add init.control.combinators 2019-02-07 09:12:53 -08:00
Sebastian Ullrich
25ffbdda57 chore(src/*): fix style 2019-02-07 15:41:12 +01:00
Sebastian Ullrich
f964ec3bc8 chore(CMakeLists): style_check: ignore src/boot/ 2019-02-07 15:41:12 +01:00
Sebastian Ullrich
e08df252d3 chore(boot): update 2019-02-07 14:28:26 +01:00
Sebastian Ullrich
12480e665e chore(library/Makefile): make generated CMakeLists.txt deterministic 2019-02-07 14:25:14 +01:00
Sebastian Ullrich
789252ad2b chore(frontends/lean/elaborator): show traces from node! 2019-02-07 14:16:28 +01:00
Sebastian Ullrich
fce7aca812 feat(frontends/lean/vm_elaborator): recover from unknown identifiers 2019-02-07 14:16:28 +01:00
Sebastian Ullrich
f2a864c91e chore(boot): update 2019-02-07 14:16:07 +01:00
Sebastian Ullrich
f9b3244d97 fix(library/init/lean/expr): literal: use C++ constructor ordering 2019-02-07 13:03:09 +01:00
Sebastian Ullrich
80c6edc620 chore(bin/lean-gdb): add lean::object pretty printer 
Not quite sure yet if this helps or just confuses gdb/CLion on invalid pointers
 2019-02-07 13:02:48 +01:00
Leonardo de Moura
7ff42dd8e5 chore(doc/examples/compiler/test): simplify example 2019-02-06 17:23:16 -08:00
Leonardo de Moura
14dd0d4907 feat(library/compiler): treat a function named main as the main function 2019-02-06 17:20:23 -08:00
Leonardo de Moura
886fdf263e chore(doc/examples/compiler): we don't need main.cpp anymore 
cc @kha @ChristianoBraga
 2019-02-06 14:50:41 -08:00
Leonardo de Moura
434627ee8e chore(runtime/io): implement io.prim.put_str just to be able to test 2019-02-06 14:35:13 -08:00
Leonardo de Moura
16c0e62fa1 feat(library/compiler/emit_cpp): emit main 2019-02-06 14:34:52 -08:00
Leonardo de Moura
b85f4aac88 feat(library/compiler/extname): add validation 2019-02-06 13:24:42 -08:00
Leonardo de Moura
a8e2e535a2 feat(library/compiler): preserve the arity of entry points 2019-02-06 12:58:18 -08:00
Leonardo de Moura
b4a7bb4f4c refactor(library/compiler): [cppname] ==> [extname] 
We will use this atttribute for all backends.
 2019-02-06 12:53:12 -08:00
Leonardo de Moura
722b7663a4 chore(boot): update 
@kha note that the previous commit produced a small code bloat here.
The code bloat seems reasonable and affects definitions such as:
```
@[inline] protected def max : rbmap α β lt → option (α × β)
| ⟨t, _⟩ :=
  match t.max with
  | some ⟨k, v⟩ := some (k, v)
  | none        := none
```
Before previous commit, while compiling `max` we would not know it is
marked as `[inline]`. Thus, we would not inline `max._main` into
`max`. Now, we do.
I believe this is not a big deal since functions marked as `[inline]`
are supposed to be small.
 2019-02-06 12:37:47 -08:00
Leonardo de Moura
f38de694b0 feat(frontends/lean/definition_cmds): compile code after attributes have been applied 
@kha do you see any problem with this change?
 2019-02-06 12:14:53 -08:00
Leonardo de Moura
9dd1ba6671 chore(boot): update 2019-02-06 10:58:03 -08:00
Leonardo de Moura
d103ff70fe feat(library/compiler): avoid cnstr_set_scalar when possible 2019-02-06 10:49:58 -08:00
Leonardo de Moura
fbc6c47094 chore(boot): update 2019-02-06 09:59:22 -08:00
Sebastian Ullrich
83e0c35204 chore(runtime/object): closure double-free assert 2019-02-06 09:38:35 -08:00
Sebastian Ullrich
57b2607463 fix(library/compiler/specialize): declare specialized functions before caller 2019-02-06 09:36:36 -08:00
Sebastian Ullrich
58830be91f chore(library/compiler/emit_cpp): ignore warnings under GCC 2019-02-06 09:35:51 -08:00
Sebastian Ullrich
34110945f2 refactor(library/compiler/llnf): replace is_runtime_builtin_cnstr with just is_builtin_constant 2019-02-06 09:35:16 -08:00
Sebastian Ullrich
11860a65eb fix(library/compiler/emit_cpp): replace constructor tag on reuse 2019-02-06 09:34:14 -08:00
Sebastian Ullrich
eb85081a03 fix(library/compiler/emit_cpp): let y = f x; let z = ...; y is not a tail call 2019-02-06 09:33:38 -08:00
Leonardo de Moura
2b67c38718 chore(boot): update 2019-02-05 17:07:22 -08:00
Leonardo de Moura
a35a951374 chore(library/compiler/emit_cpp): add uint* aliases 2019-02-05 17:01:10 -08:00
Leonardo de Moura
ed1b101dd2 doc(doc/examples/compiler): new example 2019-02-05 16:50:12 -08:00