max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
17122 commits 1 branch 0 tags 5.3 GiB
Commit graph

11543 commits

Author SHA1 Message Date
Sebastian Ullrich
e129a65948 fix(shell/CMakeLists): mark libleanstatic.a and libleanstdlib.a as cyclically dependent 2019-07-26 14:38:28 +02:00
Leonardo de Moura
798bbc0662 feat(library/init/system/io): new primitives 2019-07-25 18:12:44 -07:00
Sebastian Ullrich
53a26b94ff chore(util/lean_path): remove leanpkg.path support 
Because Lean 4 will not compile dependencies by itself, there is not much of a
point in it resolving them by itself either. The build tool that ensures that
all dependencies have been built should call `lean` with the `LEAN_PATH`
environment variable set accordingly.
 2019-07-25 17:46:40 -07:00
Leonardo de Moura
804c856282 chore(stage0): update 2019-07-25 17:39:40 -07:00
Leonardo de Moura
92a8b7028e chore(stage0): update 2019-07-25 17:30:47 -07:00
Leonardo de Moura
f6d3fc881d feat(library/init): add platform.cpp 2019-07-25 17:19:50 -07:00
Leonardo de Moura
02f516f09d feat(runtime/io): add primitives 2019-07-25 09:36:37 -07:00
Leonardo de Moura
77a59f4998 feat(library/init/io): add IO.getEnv 2019-07-25 08:31:23 -07:00
Leonardo de Moura
4f3b2eff0c chore(stage0): update 2019-07-24 13:31:23 -07:00
Leonardo de Moura
cf8daf4b24 feat(library/init/lean/elaborator): process header 
TODO:
- improve/fix `setSearchPath`
- add `IO.getEnv`
- add support for relative imports at `absolutizeModuleName`
 2019-07-24 07:37:33 -07:00
Leonardo de Moura
a7f18cff12 chore(stage0): update 2019-07-22 18:53:49 -07:00
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