Leonardo de Moura
95ebd58ae9
chore: add assertions
2021-01-30 15:49:13 -08:00
Leonardo de Moura
1ca916d9b4
fix: assertion violation
2021-01-30 14:04:47 -08:00
Leonardo de Moura
b7a0bdb9c9
fix: Injection.lean
2021-01-30 11:58:56 -08:00
Leonardo de Moura
a58ff18a5b
refactor: pos at time_task::time_task was a dead field
2021-01-30 11:10:18 -08:00
Leonardo de Moura
b28c427cb6
chore: update stage0
2021-01-30 10:58:34 -08:00
Leonardo de Moura
cde7fd97fa
chore: set page size back to 8192
...
@Kha @Vtec234 The server crashes whenever I try to use a page size
different from 8192. Any ideas?
Note that, we can compile lean, and all tests succeed but `leanserver`
ones. I am wondering whether this is a problem with the process API,
or another API that is currently being used only by the server.
2021-01-30 10:58:34 -08:00
Leonardo de Moura
3bb0c18544
chore: update stage0
2021-01-30 10:58:34 -08:00
Leonardo de Moura
7cb566af15
chore: remove lean_alloc_ctor_big
2021-01-30 10:58:34 -08:00
Leonardo de Moura
854933169e
chore: update stage0
2021-01-30 10:58:34 -08:00
Leonardo de Moura
cf5adbd4fe
chore: increase LEAN_MAX_SMALL_OBJECT_SIZE and simplify code
2021-01-30 10:58:34 -08:00
Sebastian Ullrich
a852b64bcd
chore: leanc: do not pass linking flags when not linking
...
Which suppresses a warning that may or may not have defeated ccache...?
2021-01-30 18:49:09 +01:00
Leonardo de Moura
1941081059
chore: update stage0
2021-01-29 18:25:17 -08:00
Leonardo de Moura
d71aab5dc4
fix: allow bigger ctor objects
...
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
2021-01-29 18:23:38 -08:00
Leonardo de Moura
bd65035cbb
chore: update stage0
2021-01-29 17:19:12 -08:00
Leonardo de Moura
3c02f877a8
chore: fix test
2021-01-29 17:13:04 -08:00
Leonardo de Moura
761b64c929
fix: missing occursCheck at SyntheticMVars
...
fixes #301
2021-01-29 17:13:04 -08:00
Leonardo de Moura
bf77f0707e
refactor: remove no-mutual workaround
...
This is still leftover from the old frontend.
2021-01-29 17:13:04 -08:00
Leonardo de Moura
920ae5f1b9
chore: cleanup
2021-01-29 17:13:04 -08:00
Leonardo de Moura
3b2605018b
fix: propagate nested LCtx at elimMVar
2021-01-29 17:13:04 -08:00
Leonardo de Moura
32f219772c
chore: minor
2021-01-29 17:13:04 -08:00
Leonardo de Moura
e102cd4f42
fix: checkAssignment must be at assignConst
...
Example of issue fixed by this commit: the variables `xs` may have references to `mvar`.
2021-01-29 17:13:03 -08:00
Leonardo de Moura
c86803392e
refactor: withNestedTraces
2021-01-29 17:13:03 -08:00
Leonardo de Moura
8699f439da
chore: avoid big match-expr
2021-01-29 17:13:03 -08:00
Leonardo de Moura
07beb6bc46
chore: cleanup
2021-01-29 17:13:03 -08:00
Leonardo de Moura
af7db05000
chore: remove nested outParam
2021-01-29 17:13:03 -08:00
Sebastian Ullrich
811b90dd0e
feat: option for disabling hygiene
...
/cc @leodemoura
2021-01-29 15:26:06 +01:00
Leonardo de Moura
5a02c4facc
chore: cleanup
2021-01-28 15:23:46 -08:00
Leonardo de Moura
27a27d33d2
feat: special cases for mkCongrArg, mkCongrFun, mkCongr
2021-01-28 12:19:56 -08:00
Leonardo de Moura
1d76f3e1c1
chore: cleanup
2021-01-28 12:03:06 -08:00
Wojciech Nawrocki
28d6a1ebe1
fix: go-to-def paths on Windows
2021-01-28 11:45:33 -08:00
Leonardo de Moura
8115dd11c8
chore: update stage0
2021-01-28 11:38:26 -08:00
Leonardo de Moura
d7ca646071
fix: make sure mkUnit return Syntax that is a valid term and pattern
2021-01-28 11:27:28 -08:00
Leonardo de Moura
51699f3a5b
feat: ensure binder names are atomic
2021-01-28 11:27:28 -08:00
Sebastian Ullrich
434564b125
chore: clean up manual From/ToJson instances
2021-01-28 15:51:47 +01:00
Sebastian Ullrich
d8b13c0fa2
chore: update stage0
2021-01-28 15:09:24 +01:00
Sebastian Ullrich
f3f31052e5
fix: From/ToJson derive handlers with inheritance
2021-01-28 15:07:26 +01:00
Leonardo de Moura
870896ba45
chore: fix test
2021-01-27 18:40:53 -08:00
Leonardo de Moura
7f047a95f4
chore: update stage0
2021-01-27 18:35:34 -08:00
Leonardo de Moura
4a19a5d2a4
refactor: move Eq.trans to Prelude.lean
...
We need it at `SizeOf.lean`
2021-01-27 18:27:04 -08:00
Leonardo de Moura
70d6ea57a2
fix: mkSizeOfSpecLemmaInstance
...
It was not handling correctly constructors with implicit fields.
2021-01-27 18:24:32 -08:00
Leonardo de Moura
f1a0044241
fix: use previously generated sizeOf_spec lemmas to expand rhs
2021-01-27 18:14:25 -08:00
Leonardo de Moura
c47c25cf33
feat: finish sizeOf_spec lemma generation
2021-01-27 17:20:23 -08:00
Leonardo de Moura
46d861847e
chore: update stage0
2021-01-27 16:28:01 -08:00
Leonardo de Moura
7d4f80fbc6
chore: fix name
2021-01-27 16:26:34 -08:00
Leonardo de Moura
17edc1d615
test: inductive types for testing SizeOf.lean
2021-01-27 16:26:03 -08:00
Leonardo de Moura
992e0c5ded
feat: auxiliary sizeOf lemma recursor skeleton
...
TODO: minor premises
2021-01-27 16:18:53 -08:00
Leonardo de Moura
a0ed2d1738
chore: update tests
2021-01-27 15:17:51 -08:00
Leonardo de Moura
afdc19c2f1
feat: generalize indices at mkSizeOfAuxLemma
2021-01-27 15:16:43 -08:00
Leonardo de Moura
dff6bd300e
chore: add Expr.const?
2021-01-27 15:16:15 -08:00
Leonardo de Moura
8b3a28dd2b
test: reflection
2021-01-27 12:11:43 -08:00
