Leonardo de Moura
b72ebe87bd
chore: move to new frontend
...
@Kha All files at `src/Lean/Elab` are now being compiled with the new
frontend. We can finally claim our elaborator can elaborate itself :)
It is 22% of our code base.
2020-10-16 12:34:07 -07:00
Leonardo de Moura
65abb119f5
chore: move to new frontend
2020-10-16 11:57:19 -07:00
Leonardo de Moura
eabee9ce7e
chore: remove optParam at Eval.lean
2020-10-16 11:50:53 -07:00
Leonardo de Moura
dd4ae81774
chore: move to new frontend
2020-10-16 09:16:33 -07:00
Leonardo de Moura
e02a06ad1c
chore: move to new frontend
2020-10-16 08:40:42 -07:00
Leonardo de Moura
8735820b49
fix: anonymous constructor too restrictive
...
We should support (recursive) inductive datatypes that have only one
constructor. We use this feature in the current `src/Lean` code base.
2020-10-16 07:58:47 -07:00
Sebastian Ullrich
3e09184a39
fix: String.mk, String.toList
2020-10-16 09:42:59 +02:00
Leonardo de Moura
63e982768a
feat: expand nested dos
2020-10-15 17:11:50 -07:00
Leonardo de Moura
14414e3400
feat: nested do parser
2020-10-15 17:04:35 -07:00
Leonardo de Moura
60e4f4fee1
feat: improve notFollowedBy error messages
2020-10-15 17:01:10 -07:00
Leonardo de Moura
e2ecefb67b
chore: add support for error parser in the pretty printer
2020-10-15 16:31:35 -07:00
Leonardo de Moura
f36f7592e6
chore: move to new frontend
2020-10-15 16:18:42 -07:00
Leonardo de Moura
b1e720e6cc
chore: use #lang lean4 instead of new_frontend
2020-10-15 15:40:56 -07:00
Leonardo de Moura
3cfff9df14
chore: remove workarounds
2020-10-15 15:34:36 -07:00
Leonardo de Moura
ef01053d58
fix: set mainModuleName in the new frontend
2020-10-15 15:30:03 -07:00
Leonardo de Moura
d1ad5eb51a
chore: add workarounds
2020-10-15 14:56:38 -07:00
Leonardo de Moura
7d083a7451
chore: move to new frontend
2020-10-15 14:49:23 -07:00
Leonardo de Moura
6c6f3dca87
chore: cleanup
2020-10-15 14:29:27 -07:00
Leonardo de Moura
8753a45452
chore: move to new frontend
2020-10-15 14:19:06 -07:00
Leonardo de Moura
827625a377
perf: add temporary hack for performance issue
...
The compiler frontend implemented in C++ is eagerly inlining local
functions. The new test would take an absurd amount of time without
the new hack.
We remove this hack when we re-implement the compiler frontend in Lean.
2020-10-15 13:37:29 -07:00
Leonardo de Moura
54c1607b36
chore: export Name.eraseMacroScopes
2020-10-15 11:35:32 -07:00
Leonardo de Moura
908e5f7acd
fix: elabDiscrsWitMatchType
2020-10-15 11:00:33 -07:00
Leonardo de Moura
883e07a65f
chore: remove unnecessary annotation
2020-10-15 10:50:48 -07:00
Leonardo de Moura
bdaf648667
fix: synthesizeSyntheticMVarsNoPostponing at elabMatch
2020-10-15 10:44:16 -07:00
Leonardo de Moura
755d9dedbe
chore: move to new frontend
2020-10-15 10:44:16 -07:00
Leonardo de Moura
0ee5e81513
chore: use #lang lean4
2020-10-15 10:44:16 -07:00
Leonardo de Moura
6a7e997534
chore: improve error message
2020-10-15 10:44:16 -07:00
Sebastian Ullrich
5a21725d69
perf: avoid String.toList
2020-10-15 19:43:13 +02:00
Sebastian Ullrich
b0df2be65c
chore: remove old pretty printer
2020-10-15 12:04:55 +02:00
Leonardo de Moura
38c79298ed
chore: cleanup
2020-10-14 17:56:52 -07:00
Leonardo de Moura
64ea6f3bc7
chore: move to new frontend
2020-10-14 17:45:57 -07:00
Leonardo de Moura
95cb76ddb7
chore: move to new frontend
2020-10-14 17:44:06 -07:00
Leonardo de Moura
9a3d785ae3
chore: move to new frontend
2020-10-14 17:38:17 -07:00
Leonardo de Moura
43efdd50f7
chore: move to new frontend
2020-10-14 17:38:17 -07:00
Leonardo de Moura
7be77fb189
chore: move to new frontend
2020-10-14 17:38:17 -07:00
Leonardo de Moura
c84a9f8a0b
chore: move to new frontend
2020-10-14 17:38:17 -07:00
Leonardo de Moura
abed742984
chore: cleanup
2020-10-14 17:38:17 -07:00
Leonardo de Moura
8347dd5826
chore: move to new frontend
2020-10-14 17:38:17 -07:00
Leonardo de Moura
3b34a150ff
chore: use #lang lean4
2020-10-14 17:38:17 -07:00
Leonardo de Moura
4f78142ed6
fix: add temporary hack
...
@Kha This was my first unrecoverable bug. I had to backtrack
approx. 10 commits when I noticed this bug and I couldn't build the
system anymore.
2020-10-14 17:28:34 -07:00
Leonardo de Moura
36220b785e
feat: make new frontend compatible with lean4-mode
2020-10-14 13:20:01 -07:00
Leonardo de Moura
6047d7c2b6
feat: quick and dirty #lang annotation
2020-10-14 13:20:01 -07:00
Leonardo de Moura
cfa02bf16a
chore: add missing :
2020-10-14 13:20:01 -07:00
Leonardo de Moura
5d3e08d43a
chore: documented modification needed to enable the elaboration of commands containing syntax errors
...
cc @Kha
2020-10-14 13:20:01 -07:00
Leonardo de Moura
1afc33278c
refactor: use StateRefT at Frontend
2020-10-14 13:20:01 -07:00
Sebastian Ullrich
67684db0c3
chore: delete more CMake cruft
2020-10-14 19:08:06 +02:00
Sebastian Ullrich
d5f58d27b0
chore: delete StyleCheck
2020-10-14 19:07:52 +02:00
Sebastian Ullrich
c522ea6bfa
chore: remove JSON code from old server
2020-10-14 19:06:08 +02:00
Sebastian Ullrich
32b98a1d4a
chore: remove obsolete build options & other stuff
...
TODO: remove JSON with the old frontend
2020-10-14 18:57:11 +02:00
Sebastian Ullrich
f4ffebf01c
feat: delaborator: use nicer binder name for [anonymous]
...
Fixes #193
2020-10-14 18:38:59 +02:00
