Sebastian Ullrich
85bc52b9f2
feat(library/init/lean/frontend): profile frontend
2019-03-06 11:08:38 +01:00
Leonardo de Moura
e82632cbe4
chore(boot): update
2019-02-24 15:44:11 -08:00
Leonardo de Moura
61f06fbf8e
chore(boot): update
2019-02-23 09:16:29 -08:00
Leonardo de Moura
b971db6c11
chore(boot): update
2019-02-22 16:09:48 -08:00
Leonardo de Moura
f91a37e686
chore(boot): update
2019-02-20 17:06:02 -08:00
Leonardo de Moura
a068c91e50
chore(boot): update
2019-02-20 16:20:22 -08:00
Leonardo de Moura
0cbf587a00
chore(boot): update
2019-02-19 22:17:57 -08:00
Leonardo de Moura
6276d1a7f1
feat(library/compiler/emit_cpp): avoid reset field instructions when reuse instruction is guaranteed to be executed
...
expr_const_folding.lean takes 3 secs now.
2019-02-19 13:44:46 -08:00
Leonardo de Moura
e2eeccdb2a
chore(boot): update
2019-02-19 13:06:33 -08:00
Leonardo de Moura
fe4b1509ba
chore(boot): update
2019-02-18 20:22:18 -08:00
Leonardo de Moura
59e9751c2b
chore(boot): update
2019-02-17 11:46:17 -08:00
Leonardo de Moura
0a19f46c6a
chore(boot): update
2019-02-17 10:53:04 -08:00
Leonardo de Moura
b7e7ca9527
chore(boot): update
2019-02-17 07:32:05 -08:00
Leonardo de Moura
f4143c030f
chore(boot): update
2019-02-17 06:53:05 -08:00
Leonardo de Moura
0c1c1dd607
chore(boot): update
2019-02-17 06:26:15 -08:00
Leonardo de Moura
7ed04d3ff1
chore(boot): update
2019-02-16 12:28:41 -08:00
Leonardo de Moura
54985b5a0e
fix(library/compiler/csimp): accidentally removed nat.succ x ==> x + 1 transformation from csimp
2019-02-16 12:05:17 -08:00
Leonardo de Moura
370561fbdd
chore(boot): update
2019-02-16 11:42:48 -08:00
Leonardo de Moura
90a1616cff
chore(boot): update
2019-02-15 15:26:41 -08:00
Leonardo de Moura
11c4e2dd94
chore(boot): update
2019-02-15 14:42:20 -08:00
Leonardo de Moura
b02ec6370c
chore(boot): update
2019-02-14 14:25:50 -08:00
Leonardo de Moura
4627929a83
refactor(boot,runtime,util): move name runtime implementation to util/name, and use "extern C" ABI
2019-02-13 08:27:23 -08:00
Leonardo de Moura
008ac698d7
chore(boot): update
2019-02-12 18:18:18 -08:00
Leonardo de Moura
64a2742859
chore(boot): update
2019-02-12 16:11:49 -08:00
Leonardo de Moura
0e98f6bd66
chore(boot): update
2019-02-12 15:48:44 -08:00
Leonardo de Moura
4df56faf6a
chore(boot): update
2019-02-12 14:11:36 -08:00
Leonardo de Moura
c8e8fbf840
chore(boot): update after rebase
2019-02-12 11:49:49 -08:00
Sebastian Ullrich
8e7faeeb5d
chore(boot): update
2019-02-12 13:35:50 +01:00
Leonardo de Moura
c105da0d86
chore(boot): update
2019-02-11 15:57:05 -08:00
Leonardo de Moura
7e8f9e6f66
feat(library/compiler): add [extern] attribute
2019-02-09 18:53:44 -08:00
Sebastian Ullrich
b579358b25
chore(boot): update
2019-02-09 19:57:24 +01:00
Leonardo de Moura
2d55c3f73c
chore(boot): update
2019-02-08 16:44:17 -08:00
Leonardo de Moura
4ce415cbde
chore(boot): update
2019-02-08 11:12:13 -08:00
Sebastian Ullrich
f2a864c91e
chore(boot): update
2019-02-07 14:16:07 +01: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
9dd1ba6671
chore(boot): update
2019-02-06 10:58:03 -08:00
Leonardo de Moura
fbc6c47094
chore(boot): update
2019-02-06 09:59:22 -08:00
Leonardo de Moura
2b67c38718
chore(boot): update
2019-02-05 17:07:22 -08:00
Leonardo de Moura
c4e8770342
feat(runtime,boot): second part of the previous commit
2019-02-05 16:28:18 -08:00
Leonardo de Moura
cfa21d6875
chore(boot): update
2019-02-05 14:41:42 -08:00
Leonardo de Moura
60c8b1870e
chore(boot): update
2019-02-05 13:08:59 -08:00
Leonardo de Moura
fe3be7a80d
chore(boot): update
2019-02-04 16:23:38 -08:00
Leonardo de Moura
a6645645e3
chore(boot): update
2019-02-04 16:07:31 -08:00
Leonardo de Moura
fc4505884b
chore(boot): update
2019-02-04 12:56:11 -08:00
Leonardo de Moura
4696f603e2
chore(boot): update
2019-02-04 10:36:02 -08:00
Leonardo de Moura
b4a78a0280
chore(src/boot): update
2019-02-03 19:22:01 -08:00
Leonardo de Moura
628c377673
chore(src/boot): update
2019-02-03 10:45:48 -08:00
Leonardo de Moura
b5f20f0b73
chore(src/boot): update
2019-02-03 10:38:57 -08:00
Leonardo de Moura
fb0562e107
chore(src/boot): update
2019-02-03 10:06:47 -08:00
Leonardo de Moura
065c3b991c
chore(src/boot): update
2019-02-01 17:59:29 -08:00
