Sebastian Ullrich
b83875301a
chore: move test without output
...
/cc @leodemoura
2021-02-02 13:37:56 +01:00
Sebastian Ullrich
dd6c291788
fix: relax eager mvar instantiation during constructor elaboration
...
@leodemoura: Could you double-check?
2021-02-02 13:19:15 +01:00
Leonardo de Moura
b6ba346f2a
test: add cases alternative @ test
2021-02-01 18:24:50 -08:00
Leonardo de Moura
fba719ff02
chore: adjust WF.lean
2021-02-01 18:08:48 -08:00
Leonardo de Moura
a7d2edd333
chore: update stage0
2021-02-01 18:04:28 -08:00
Leonardo de Moura
2888e49785
feat: @ modifier at induction and cases tactic alternatives
2021-02-01 18:03:19 -08:00
Leonardo de Moura
c1dce595a5
feat: add option useNamesForExplicitOnly to introN
2021-02-01 17:35:48 -08:00
Leonardo de Moura
e583b3bdc0
feat: allow @ modifier at inductionAlt
2021-02-01 17:13:51 -08:00
Leonardo de Moura
1d39c2aabc
chore: update stage0
2021-02-01 17:07:10 -08:00
Leonardo de Moura
4a932b9d06
chore: prepare to @ to inductionAlt
2021-02-01 17:05:50 -08:00
Leonardo de Moura
bc173375ba
fix: missing resolveGlobalConstNoOverload
2021-02-01 16:12:25 -08:00
Leonardo de Moura
b4dfa08543
chore: store eliminator name at ElimInfo
2021-02-01 13:16:52 -08:00
Leonardo de Moura
ac104213e3
test: cases-using name resolution issue
2021-02-01 13:16:19 -08:00
Sebastian Ullrich
d4dc54a724
fix: make sure to instantiate mvars in constructors
2021-02-01 12:10:26 +01:00
Sebastian Ullrich
eedce252ff
chore: Nix: do not set extra cmake flags like fsanitize for stage 0
2021-02-01 11:58:37 +01:00
Leonardo de Moura
752af03899
chore: update stage0
2021-01-31 12:10:08 -08:00
Leonardo de Moura
22a7a9e313
fix: missing lean_inc
2021-01-31 12:07:24 -08:00
Leonardo de Moura
f9ebfb466f
fix: missing lean_inc
2021-01-31 11:18:57 -08:00
Leonardo de Moura
d8ced44ce2
test: fix test
...
Error is now caught by the elaborator too
2021-01-31 09:01:08 -08:00
Leonardo de Moura
60805b5c0c
test: test for Int.mod bug
2021-01-31 08:57:41 -08:00
Leonardo de Moura
c4cfbceb71
test: div0 crash
2021-01-31 08:52:39 -08:00
Leonardo de Moura
9419b178bc
chore: update stage0
2021-01-31 08:52:24 -08:00
Leonardo de Moura
36e70e9a08
fix: Int.mod implementation in the runtime
2021-01-31 08:50:06 -08:00
Leonardo de Moura
e47485a9d1
chore: update stage0
2021-01-31 08:25:16 -08:00
Leonardo de Moura
3fa1f355eb
fix: mod implementation
2021-01-31 08:19:32 -08:00
Leonardo de Moura
52c4b7219f
chore: document fix
2021-01-30 17:15:16 -08:00
Leonardo de Moura
29a56db732
fix: check if reused segment is full
2021-01-30 17:02:29 -08:00
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
