Leonardo de Moura
14052ff785
chore(boot): update
2019-03-14 10:46:12 -07:00
Leonardo de Moura
2a2f3c1429
chore(boot): update
2019-03-12 06:56:05 -07:00
Leonardo de Moura
cf3bbd7e25
feat(runtime): add utf8_prev and utf8_set
...
Next goal: implement string.iterator in Lean
2019-03-11 18:05:40 -07:00
Sebastian Ullrich
0580ce7cfa
chore(boot): update
2019-03-08 15:34:37 +01:00
Leonardo de Moura
29770d73b3
chore(boot): update
2019-03-07 12:49:53 -08:00
Leonardo de Moura
06be451110
chore(boot): update
2019-03-07 11:30:51 -08:00
Leonardo de Moura
ae95a3b6ef
chore(boot): update
2019-03-06 17:27:40 -08:00
Leonardo de Moura
801f55faf0
chore(boot): update
2019-03-06 11:07:02 -08:00
Sebastian Ullrich
1ad5450853
perf(library/init/control/coroutine): mark as [inline_as_reduce]
2019-03-06 17:30:20 +01:00
Sebastian Ullrich
00d9a1e76e
chore(boot): update
2019-03-06 13:59:34 +01:00
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
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
b739d7f343
chore(boot): update
2019-02-18 20:53:04 -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
fbedc1d098
chore(boot): update
2019-02-17 07:18:28 -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
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
60c8b1870e
chore(boot): update
2019-02-05 13:08:59 -08:00
