Leonardo de Moura
|
7897769732
|
chore: move BinomialHeap to Std
|
2020-05-22 11:10:47 -07:00 |
|
Leonardo de Moura
|
efba802011
|
feat: start Std package
|
2020-05-22 10:58:44 -07:00 |
|
Sebastian Ullrich
|
f45fcb4898
|
test: add tests/compiler/foreign and doc/examples/compiler
|
2020-05-22 09:22:26 -07:00 |
|
Sebastian Ullrich
|
573a128096
|
feat: leanmake: print out compile flags in analogy to pkg-config/llvm-config
|
2020-05-22 09:22:26 -07:00 |
|
Sebastian Ullrich
|
7b2bcbe683
|
chore: disable inconsequential LLVM warning
Emacs always stops scrolling at this warning while building
|
2020-05-22 09:22:26 -07:00 |
|
Sebastian Ullrich
|
3ffea2dfbd
|
feat: leanmake: add clean target
|
2020-05-22 09:22:26 -07:00 |
|
Sebastian Ullrich
|
38a3c36134
|
feat: make leanmake extensible with custom Makefiles; rename standard Makefile to lean.mk; document
|
2020-05-22 09:22:26 -07:00 |
|
Leonardo de Moura
|
e20f712710
|
fix: but at elabModifyOp
|
2020-05-21 17:17:21 -07:00 |
|
Leonardo de Moura
|
f9f1e5d133
|
fix: bug at mkSubstructSource
|
2020-05-21 16:33:46 -07:00 |
|
Leonardo de Moura
|
7a964ecbea
|
chore: register `Elab.struct trace class
|
2020-05-21 16:33:03 -07:00 |
|
Leonardo de Moura
|
f44fe34661
|
feat: add expandStructInstExpectedType
|
2020-05-21 09:39:18 -07:00 |
|
Leonardo de Moura
|
959a860bdf
|
feat: elaborate new structure instance syntax
|
2020-05-20 18:10:33 -07:00 |
|
Leonardo de Moura
|
f427a6bd3f
|
feat: new structure instance syntax
|
2020-05-20 16:57:58 -07:00 |
|
Leonardo de Moura
|
618d113075
|
chore: remove workaround for bug at new { ... : <expected-type> } syntax
|
2020-05-20 15:56:28 -07:00 |
|
Leonardo de Moura
|
c01da783ca
|
fix: { ... : <expected-type> } syntax in the old frontend
|
2020-05-20 15:49:40 -07:00 |
|
Leonardo de Moura
|
05dda45a22
|
chore: remove { <structure-name> . ... } from stdlib
TODO: fix problems with `{ ... : <expected-type }` new syntax
|
2020-05-20 15:43:21 -07:00 |
|
Leonardo de Moura
|
22ae065d16
|
feat: add { ... : <expected-type> } syntax
It replaces the `{ <struct-name> . ... }` syntax.
|
2020-05-20 15:24:27 -07:00 |
|
Leonardo de Moura
|
bd58048449
|
chore: { <source> with ... } syntax
|
2020-05-20 15:08:43 -07:00 |
|
Leonardo de Moura
|
3f44e8f3df
|
chore: remove .. src syntax from old frontend
|
2020-05-20 13:07:21 -07:00 |
|
Sebastian Ullrich
|
3d891be49e
|
feat: delaborator: do not set whitespace information
|
2020-05-20 11:54:53 -07:00 |
|
Sebastian Ullrich
|
b28eedbd98
|
refactor: make all fields of SourceInfo optional
|
2020-05-20 11:54:53 -07:00 |
|
Sebastian Ullrich
|
0086bdf642
|
feat: use new SourceInfo in syntax quotations
|
2020-05-20 11:54:53 -07:00 |
|
Sebastian Ullrich
|
d420f46432
|
fix: '\r' escape
|
2020-05-20 15:13:24 +02:00 |
|
Sebastian Ullrich
|
dea99e1814
|
fix: imax is not a keyword
|
2020-05-20 15:13:10 +02:00 |
|
Sebastian Ullrich
|
66a0a239a3
|
fix: structure instances missing comma
|
2020-05-20 15:12:42 +02:00 |
|
Sebastian Ullrich
|
6a0410f8f0
|
feat: make import A import A.olean instead of A/Default.olean
|
2020-05-19 11:29:32 -07:00 |
|
Sebastian Ullrich
|
e86758da60
|
chore: add missing preludes in Init/Lean
These aren't really necessary, but it's more consistent with other files and saves me a stage 0 update
|
2020-05-19 11:29:32 -07:00 |
|
Sebastian Ullrich
|
dc56eb7a86
|
chore: remove obsolete built-in search path
|
2020-05-19 11:29:32 -07:00 |
|
Leonardo de Moura
|
c7a5963483
|
fix: missing file
|
2020-05-18 12:15:41 -07:00 |
|
Leonardo de Moura
|
1a77ee4f89
|
chore: delete old runtime directory
|
2020-05-18 11:33:18 -07:00 |
|
Leonardo de Moura
|
e7cbaf1b57
|
chore: adjust CMakeLists.txt
|
2020-05-18 11:32:46 -07:00 |
|
Leonardo de Moura
|
8bdca35282
|
chore: use #include <lean/runtime/...> for runtime .h files
|
2020-05-18 11:30:07 -07:00 |
|
Leonardo de Moura
|
72df1b323a
|
chore: copy runtime files
|
2020-05-18 11:06:26 -07:00 |
|
Sebastian Ullrich
|
9fdcf6ea59
|
refactor: put all includes in include/lean/
|
2020-05-18 11:00:26 -07:00 |
|
Sebastian Ullrich
|
78a3305764
|
chore: duplicate install file
|
2020-05-18 14:51:18 +02:00 |
|
Sebastian Ullrich
|
150f44b61b
|
fix: install
|
2020-05-18 14:38:23 +02:00 |
|
Leonardo de Moura
|
8a4e752f56
|
chore: fix OSX issues
|
2020-05-15 11:07:24 -07:00 |
|
Sebastian Ullrich
|
0918c8602b
|
fix: avoid sed, which doesn't always like \r
|
2020-05-15 19:41:32 +02:00 |
|
Sebastian Ullrich
|
5086c030f3
|
chore: remove obsolete style_check setup
|
2020-05-14 23:13:51 +02:00 |
|
Sebastian Ullrich
|
a6fbf3c20e
|
refactor: make stages internally consistent by compiling the stageN lib with the stageN compiler, rename static libraries
The old stage1 is now stage0.5, which at least suggests that it's not an entirely consistent stage in general
|
2020-05-14 23:13:51 +02:00 |
|
Sebastian Ullrich
|
afd7e5fa6e
|
feat: introduce simple leanmake wrapper
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
aa3bca1cf5
|
refactor: make Makefile reusable
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
984fec7387
|
refactor: move update-stage0 out of Makefile
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
bea0be51b3
|
fix: install
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
342675181a
|
fix: build
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
279746fa6a
|
chore: change stage1-3 into homogeneous ExternalProjects from new top-level /CMakeLists.txt
This ensures stage2+3 are full, standalone Lean installations
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
10253e89ea
|
chore: move bin/ and .oleans into build directory
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
73b4cf329d
|
fix: Windows build
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
5d260c396f
|
fix: macOS build
|
2020-05-14 14:47:54 +02:00 |
|
Sebastian Ullrich
|
5f1a052998
|
feat: replace --make with -o flag that takes an explicit .olean target file name
|
2020-05-14 14:47:54 +02:00 |
|