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
36e70e9a08
fix: Int.mod implementation in the runtime
2021-01-31 08:50:06 -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
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
7cb566af15
chore: remove lean_alloc_ctor_big
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
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
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
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
f3f31052e5
fix: From/ToJson derive handlers with inheritance
2021-01-28 15:07:26 +01: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
7d4f80fbc6
chore: fix name
2021-01-27 16:26:34 -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
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
Sebastian Ullrich
d76378f12e
chore: fix pp.coercions description
...
@leodemoura still unsure about the ideal polarity of some pp options...
2021-01-27 14:46:37 +01:00
Sebastian Ullrich
a3a8d76e96
chore: move pp_options.cpp to Lean
2021-01-27 14:16:12 +01:00
Sebastian Ullrich
c7347bbe0f
fix: that's not how Makefiles work
2021-01-27 12:34:48 +01:00
Leonardo de Moura
5f704b6b6f
chore: fix option name
2021-01-26 18:30:46 -08:00
Leonardo de Moura
6c119a1921
chore: use register_builtin_option
2021-01-26 18:24:56 -08:00
Leonardo de Moura
365a71ad9c
chore: remove dead options
2021-01-26 18:09:59 -08:00
Leonardo de Moura
4c3c049198
chore: use builtin_initialize
2021-01-26 18:09:45 -08:00
Sebastian Ullrich
cfecdbce8b
refactor: typed Lean.Option & register_builtin_option macro
2021-01-26 17:43:26 -08:00
