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
Leonardo de Moura
9017fd3658
chore(src/boot): update
2019-02-01 15:13:06 -08:00
Leonardo de Moura
0c36b8c4d8
chore(src/boot): update
2019-02-01 15:02:24 -08:00
Leonardo de Moura
8c1d6c49c5
chore(src/boot): update
2019-02-01 14:40:22 -08:00
Leonardo de Moura
4fa06e38b2
chore(*): add skeleton for new builtin primitives, update src/boot
2019-02-01 14:03:03 -08:00
Leonardo de Moura
5b37913a51
chore(src/boot): add generated C++ files
2019-02-01 11:24:08 -08:00
