Leonardo de Moura
00a3c2ac56
chore: update stage0
2020-10-22 05:32:12 -07:00
Sebastian Ullrich
b77a2de10d
perf: must inline basic coercions
2020-10-22 14:26:51 +02:00
Leonardo de Moura
e899dc5e16
chore: remove workaround
2020-10-22 05:16:48 -07:00
Leonardo de Moura
f3c8cf3811
chore: update stage0
2020-10-22 05:15:03 -07:00
Leonardo de Moura
8b146ffe14
feat: expand uminus notation
2020-10-22 05:07:05 -07:00
Leonardo de Moura
fc323b5aaa
chore: remove workaround
2020-10-22 04:42:59 -07:00
Leonardo de Moura
7c37453745
chore: update stage0
2020-10-22 04:42:10 -07:00
Leonardo de Moura
6ca1768957
fix: optional := in the structure command
2020-10-22 04:39:20 -07:00
Sebastian Ullrich
ce96fab8de
chore: fix passing additional LEAN(C)_OPTS to make
2020-10-22 12:00:39 +02:00
Sebastian Ullrich
4e74e36331
feat: run initializers on import
...
Also, refuse to evaluate an `[init]` decl in the same module (since we don't know whether the initialization is
backtrackable) and always use native symbol of a `[builtinInit]` decl
2020-10-22 11:59:55 +02:00
Sebastian Ullrich
6ed395a131
feat: ParametricAttributeImpl.afterImport
2020-10-22 11:59:55 +02:00
Sebastian Ullrich
4e8f4fcaef
refactor: extract AttributeImplCore, introduce ParametricAttributeImpl
2020-10-22 11:59:55 +02:00
Sebastian Ullrich
86fe95898d
fix: don't try to interpret [builtinInit] constants
2020-10-22 11:59:55 +02:00
Leonardo de Moura
64fc4897c3
chore: update stage0
2020-10-21 18:46:49 -07:00
Leonardo de Moura
82ee2e361b
chore: cleanup
2020-10-21 18:43:47 -07:00
Leonardo de Moura
ea829b75c0
chore: remove coercions for old frontend
2020-10-21 17:37:35 -07:00
Leonardo de Moura
943687ad09
chore: move to new frontend
...
@Kha all files at `src/Lean` and `src/Std` have been moved to the new
frontend :)
Next target `src/Init`
2020-10-21 17:31:25 -07:00
Leonardo de Moura
d5612320d7
chore: move to new frontend
2020-10-21 17:12:56 -07:00
Leonardo de Moura
0c89dca20e
chore: move to new frontend
2020-10-21 17:09:24 -07:00
Leonardo de Moura
b555307f06
chore: move to new frontend
2020-10-21 16:35:50 -07:00
Leonardo de Moura
805b3e0ef9
chore: update stage0
2020-10-21 15:22:30 -07:00
Leonardo de Moura
21e6ae645a
chore: move to new frontend
2020-10-21 15:14:13 -07:00
Leonardo de Moura
8abbf7634d
chore: move to new frontend
2020-10-21 14:16:41 -07:00
Leonardo de Moura
6814d89ac8
chore: update stage0
2020-10-21 13:31:30 -07:00
Leonardo de Moura
7111eb4d79
chore: move to new frontend
2020-10-21 13:30:43 -07:00
Leonardo de Moura
21132d6c63
chore: update stage0
2020-10-21 12:18:04 -07:00
Leonardo de Moura
24d41b9518
chore: move to new frontend
2020-10-21 12:16:30 -07:00
Leonardo de Moura
cb66295149
chore: cleanup
2020-10-21 11:34:44 -07:00
Leonardo de Moura
2c94222a69
chore: update stage0
2020-10-21 11:32:22 -07:00
Leonardo de Moura
d25ec3417b
chore: remove some [inline] and [specialize] annotations from Parser/Basic
2020-10-21 11:27:18 -07:00
Leonardo de Moura
93a8bb737f
chore: cleanup
2020-10-21 11:07:18 -07:00
Leonardo de Moura
d640105dcc
chore: cleanup
2020-10-21 11:02:01 -07:00
Leonardo de Moura
e5c17463c5
chore: move to new frontend
2020-10-21 10:06:53 -07:00
Leonardo de Moura
1af6f14fa8
chore: move to new frontend
2020-10-21 09:17:02 -07:00
Leonardo de Moura
7966856b32
chore: move to new frontend
2020-10-21 09:13:55 -07:00
Leonardo de Moura
4d64edfff3
chore: move to new frontend
2020-10-21 08:51:11 -07:00
Leonardo de Moura
3e9c5e1653
chore: move to new frontend
2020-10-21 08:43:47 -07:00
Leonardo de Moura
4f109e23c2
feat: return syntax object representing the whole file
2020-10-21 07:55:59 -07:00
Sebastian Ullrich
5351bffb99
chore: revert obsolete workaround
2020-10-21 11:21:56 +02:00
Sebastian Ullrich
b06f8311e8
fix: avoid using native code during bootstrap
2020-10-21 11:21:56 +02:00
Sebastian Ullrich
438b3351dd
feat: add interpreter.prefer_native option
2020-10-21 11:21:56 +02:00
Leonardo de Moura
f6ece7ee04
chore: update stage0
2020-10-20 17:41:57 -07:00
Leonardo de Moura
28664d9dc2
chore: move to new frontend
2020-10-20 17:41:04 -07:00
Leonardo de Moura
b3678954f4
chore: move to new frontend
2020-10-20 17:19:05 -07:00
Leonardo de Moura
e57d5800c2
chore: update stage0
2020-10-20 17:03:03 -07:00
Leonardo de Moura
f8971200af
chore: move to new frontend
2020-10-20 17:01:29 -07:00
Leonardo de Moura
e1469d07d2
chore: move to new frontend
2020-10-20 16:36:02 -07:00
Leonardo de Moura
805481ac50
chore: move to new frontend
2020-10-20 16:24:10 -07:00
Leonardo de Moura
192d45d867
chore: fix tests
2020-10-20 16:15:30 -07:00
Leonardo de Moura
93f7b1d7bc
chore: move to new frontend
2020-10-20 16:13:07 -07:00
