Leonardo de Moura
9d741a8b3a
chore: update stage0
2020-10-22 16:30:07 -07:00
Leonardo de Moura
bc8b78f481
chore: cleanup
2020-10-22 16:30:06 -07:00
Leonardo de Moura
620647f2f1
refactor: simplify MonadCache and generalize instantiateExprMVars
2020-10-22 16:30:06 -07:00
Leonardo de Moura
c865abb340
refactor: remove MonadRun
2020-10-22 16:30:06 -07:00
Leonardo de Moura
02968a44a8
chore: update stage0
2020-10-22 16:30:06 -07:00
Leonardo de Moura
a5a153d1fb
refactor: remove foldlFrom from PersistentArray and LocalContext
2020-10-22 16:30:05 -07:00
Leonardo de Moura
34cdc3a1f1
chore: avoid Array.foldlFrom
2020-10-22 16:30:05 -07:00
Leonardo de Moura
9c4a08d846
chore: update stage0
2020-10-22 16:30:05 -07:00
Leonardo de Moura
43fbfec1fd
chore: avoid Array.iterate and Array.iterateM
2020-10-22 16:30:04 -07:00
Leonardo de Moura
7750d56d82
chore: update stage0
2020-10-22 16:30:04 -07:00
Leonardo de Moura
073bbeb676
chore: move to new frontend
2020-10-22 16:30:03 -07:00
Leonardo de Moura
98bfa780b3
chore: update stage0
2020-10-22 16:30:03 -07:00
Leonardo de Moura
19d7050847
chore: remove Lean.Name.Name.beq
2020-10-22 16:30:02 -07:00
Leonardo de Moura
fafad59577
chore: update stage0
2020-10-22 16:30:02 -07:00
Leonardo de Moura
311265d833
fix: Name.beq primitive name
...
@Kha I cannot change the name is one step. The problem is that stage0
contains only the function `l_Lean_Name_Name_beq___boxed`.
So, I have to add a function with the new name, update stage0, and
then delete the old one. Otherwise, the build breaks because
the interpreter will fail when we try to test whether two names are
equal or not. The summary is: we cannot change the Lean name for a
primitive in one step because it changes the name of the auxiliary
"boxed" definition used by the interpreter.
2020-10-22 16:30:02 -07:00
Leonardo de Moura
4f6538fa9f
fix: extern detection
2020-10-22 16:30:02 -07:00
Sebastian Ullrich
7964b727e5
chore: improve error message
2020-10-22 21:40:58 +02:00
Leonardo de Moura
4d95c36885
chore: update stage0
2020-10-22 10:38:35 -07:00
Leonardo de Moura
85c955d77f
feat: improve ▸ notation
2020-10-22 10:35:45 -07:00
Leonardo de Moura
025e7eb64a
chore: update stage0
2020-10-22 10:25:32 -07:00
Leonardo de Moura
34945dfc1c
feat: elaborate ▸ notation
2020-10-22 10:20:23 -07:00
Leonardo de Moura
417336ad2f
feat: allow .. in non-pattern applications
2020-10-22 08:56:10 -07:00
Leonardo de Moura
a2de86f0e2
chore: cleanup
2020-10-22 08:35:51 -07:00
Leonardo de Moura
af968c60e6
chore: cleanup
2020-10-22 07:32:23 -07:00
Leonardo de Moura
4efad86fa5
chore: cleanup
2020-10-22 07:26:13 -07:00
Leonardo de Moura
2a393cd4ab
chore: remove workaround
2020-10-22 07:06:09 -07:00
Leonardo de Moura
a919349c80
chore: update stage0
2020-10-22 07:02:40 -07:00
Leonardo de Moura
2041277cae
fix: field default value with implicit type
2020-10-22 07:02:40 -07:00
Leonardo de Moura
427936fa63
chore: move to new frontend
2020-10-22 07:02:40 -07:00
Sebastian Ullrich
c32f843efc
fix: profiling from the new frontend; use trace out for the time being
2020-10-22 16:00:03 +02:00
Sebastian Ullrich
997365b622
chore: remove lone #check
2020-10-22 15:58:53 +02:00
Sebastian Ullrich
7f8d6b803f
feat: interpolatedStr pretty printer
2020-10-22 15:01:53 +02:00
Sebastian Ullrich
ecece59cc3
fix: tracing the compiler from the new frontend
2020-10-22 14:50:26 +02:00
Sebastian Ullrich
b562cb8a2a
fix: exception while tracing in the old frontend
2020-10-22 14:50:26 +02:00
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
