Leonardo de Moura
|
2ad33a23db
|
chore(runtime,library/init/lean): remove evalConst
|
2019-07-19 11:04:57 -07:00 |
|
Leonardo de Moura
|
b2d678f4ca
|
chore(stage0): update
|
2019-07-19 10:57:33 -07:00 |
|
Leonardo de Moura
|
b634fc30ee
|
chore(library/init/lean/elaborator/command): add command.lean
|
2019-07-19 10:54:39 -07:00 |
|
Leonardo de Moura
|
79545f55c0
|
feat(library/init/io): add IO.readTextFile
|
2019-07-18 17:31:31 -07:00 |
|
Leonardo de Moura
|
119a890d79
|
chore(stage0): update
|
2019-07-18 13:23:22 -07:00 |
|
Leonardo de Moura
|
09c51622a7
|
chore(stage0): update
|
2019-07-17 19:09:16 -07:00 |
|
Leonardo de Moura
|
2f7220402d
|
chore(stage0): update
|
2019-07-17 19:09:16 -07:00 |
|
Leonardo de Moura
|
eebb8e2e27
|
feat(library/init/lean/elaborator): add Elab monad
|
2019-07-17 19:09:16 -07:00 |
|
Leonardo de Moura
|
12ba2d353e
|
fix(stage0): missing file
|
2019-07-17 19:09:16 -07:00 |
|
Leonardo de Moura
|
f0899b381d
|
feat(library/init/lean/parser/module): add displayStx param
|
2019-07-17 19:09:15 -07:00 |
|
Leonardo de Moura
|
18d47a2b74
|
chore(frontends/lean): remove allow_field_notation = false setting
This setting was used for the explicit notation `@`.
We should not need it.
|
2019-07-17 19:09:15 -07:00 |
|
Leonardo de Moura
|
d03e00de99
|
chore(frontends/lean/builtin_exprs): remove obsolete notation from old parser
|
2019-07-17 19:09:15 -07:00 |
|
Leonardo de Moura
|
a3c0e2bb36
|
chore(frontends/lean/builtin_exprs): ensure old let notation is not accepted
|
2019-07-17 08:26:42 -07:00 |
|
Leonardo de Moura
|
0c4708ad28
|
chore(stage0): update
|
2019-07-16 09:07:39 -07:00 |
|
Leonardo de Moura
|
b2e1ff8b3e
|
feat(library/init): use new "empty match" syntax
|
2019-07-15 16:25:14 -07:00 |
|
Leonardo de Moura
|
7d062dd961
|
feat(frontends/lean): add new "empty/no match" syntax to old parser
|
2019-07-15 16:18:44 -07:00 |
|
Leonardo de Moura
|
12346d344a
|
feat(shell/lean): invoke new parser when --new-frontend is used
|
2019-07-15 13:57:05 -07:00 |
|
Leonardo de Moura
|
367f28e90b
|
chore(library/init/lean/parser/module): export test function
|
2019-07-15 13:39:56 -07:00 |
|
Leonardo de Moura
|
4c3ea024bc
|
chore(stage0): update
|
2019-07-15 09:46:39 -07:00 |
|
Leonardo de Moura
|
1b8c2200d5
|
chore(stage0): update
|
2019-07-11 16:45:09 -07:00 |
|
Leonardo de Moura
|
57e2f1be2a
|
feat(library/init/lean/parser/term): builtin operators
|
2019-07-11 10:13:00 -07:00 |
|
Leonardo de Moura
|
c9cd693b8e
|
feat(runtime/object): avoid recursion at mark_mt and mark_persistent
Reason: potential stack overflows
|
2019-07-10 11:27:49 -07:00 |
|
Leonardo de Moura
|
a85a98f1ec
|
chore(stage0): update
|
2019-07-10 11:19:40 -07:00 |
|
Leonardo de Moura
|
022d22cac4
|
feat(library/compiler/extract_closed): fine grain extraction
Motivation: increase reuse
|
2019-07-10 11:14:20 -07:00 |
|
Leonardo de Moura
|
efa48d6762
|
chore(stage0): update
|
2019-07-10 11:11:53 -07:00 |
|
Leonardo de Moura
|
17cc34def5
|
feat(library/compiler/compiler): add option compiler.extract_closed
It is useful when using `unsafeIO`
|
2019-07-10 11:08:34 -07:00 |
|
Leonardo de Moura
|
228ddd5fdc
|
chore(stage0): update
|
2019-07-09 16:39:32 -07:00 |
|
Leonardo de Moura
|
85d151a335
|
feat(library/compiler): use eta expansion at eager_lambda_lifting
|
2019-07-09 16:34:20 -07:00 |
|
Leonardo de Moura
|
bda0277468
|
chore(stage0): update
|
2019-07-09 14:22:10 -07:00 |
|
Leonardo de Moura
|
f1a2c83e8c
|
feat(library/compiler/eager_lambda_lifting): do not pass closed terms as arguments to lifted decl
|
2019-07-09 14:06:14 -07:00 |
|
Leonardo de Moura
|
0f873b7ba2
|
fix(library/compiler/eager_lambda_lifting): collect type dependencies
|
2019-07-09 13:32:41 -07:00 |
|
Leonardo de Moura
|
ff0d184176
|
chore(stage0): update
|
2019-07-08 22:04:51 -07:00 |
|
Leonardo de Moura
|
324a053f4c
|
fix(library/init/lean/compiler/ir/resetreuse): bug at Dmain
|
2019-07-08 20:37:54 -07:00 |
|
Leonardo de Moura
|
dbc67242a1
|
chore(stage0): update
|
2019-07-08 17:40:30 -07:00 |
|
Leonardo de Moura
|
1a81d60820
|
chore(frontends/lean/parser): simplify binder notation
The `<ident> : <expr>` now requires explicit brackets.
|
2019-07-08 08:54:19 -07:00 |
|
Leonardo de Moura
|
0fc9aa24bc
|
chore(frontends/lean/parser): remove "binder collection" support
This kind of notation will not be supported in the new builtin parser.
If users want they may define their own notation with this feature.
|
2019-07-08 08:36:29 -07:00 |
|
Leonardo de Moura
|
8fa888878f
|
chore(frontends/lean/parser): remove support for ⦃ binders
|
2019-07-07 08:37:49 -07:00 |
|
Leonardo de Moura
|
8944767f6c
|
chore(frontends/lean): Π ==> ∀
|
2019-07-07 08:13:40 -07:00 |
|
Sebastian Ullrich
|
9707672cc8
|
fix(runtime/mpz): fix and document size_t functions
|
2019-07-05 16:27:04 -07:00 |
|
Sebastian Ullrich
|
723e9cc430
|
chore(runtime/object): fix usize_to_nat name
|
2019-07-05 16:26:54 -07:00 |
|
Sebastian Ullrich
|
826a5ee16b
|
chore(shell/lean): profile initialization time
|
2019-07-05 16:21:48 +02:00 |
|
Sebastian Ullrich
|
b41f4a517c
|
chore(bin/leanc): set increased stack size on Windows
|
2019-07-05 11:24:15 +02:00 |
|
Sebastian Ullrich
|
26155442f1
|
fix(CMakeLists): cmake -E copy doesn't support wildcards on Windows
I don't think we'll need archives other than .a if we don't support MSVC
|
2019-07-05 11:24:15 +02:00 |
|
Sebastian Ullrich
|
2c9dce6eed
|
fix(runtime/mpz): use size_t instead of unsigned long for Windows compatibility
|
2019-07-05 11:24:15 +02:00 |
|
Leonardo de Moura
|
ea6eee516b
|
chore(frontends/lean): use => instead of := in match-expressions
Motivation: use same separator used in lambda expressions as in
other programming languages.
|
2019-07-04 11:38:38 -07:00 |
|
Leonardo de Moura
|
bf1f62c115
|
chore(shell/CMakeLists): temporarily remove --output-sync
@kha this option is only available is gnu make version >= 4.0.
|
2019-07-04 10:28:51 -07:00 |
|
Sebastian Ullrich
|
4c650d23d4
|
chore(shell/CMakeLists): avoid overlapping make output
|
2019-07-03 08:30:18 -07:00 |
|
Leonardo de Moura
|
0bee94886e
|
feat(frontends/lean/builtin_exprs): , from ==> from, and cleanup suffices
|
2019-07-02 17:22:50 -07:00 |
|
Leonardo de Moura
|
7ba9a5012a
|
chore(frontends/lean/builtin_exprs): make sure have-expression is consistent with let-expression
|
2019-07-02 16:46:51 -07:00 |
|
Leonardo de Moura
|
92466272ed
|
fix(library/init/lean/compiler/ir/emitcpp): incorrectly emitting unicode characters in the range [128, 255]
For example, "·" was being stored as `\xb7` which is not the valid UTF8.
|
2019-07-02 15:56:32 -07:00 |
|