Leonardo de Moura
350cf4d262
chore: copy runtime files to include/lean
2020-05-22 14:04:24 -07:00
Leonardo de Moura
5eae116e66
chore: update stage0
2020-05-22 11:23:38 -07:00
Leonardo de Moura
ae3a433f9c
chore: add Std to CMakeLists.txt
...
@Kha did I miss anything?
2020-05-22 11:19:14 -07:00
Leonardo de Moura
82e4cc9749
chore: update stage0
2020-05-22 11:11:31 -07:00
Leonardo de Moura
7897769732
chore: move BinomialHeap to Std
2020-05-22 11:10:47 -07:00
Leonardo de Moura
e5218319fc
chore: update stage0
...
I had to use `make -Cstage1 update-stage0`
2020-05-22 10:59:38 -07:00
Leonardo de Moura
efba802011
feat: start Std package
2020-05-22 10:58:44 -07:00
Leonardo de Moura
83d1b62a99
chore: update stage0
2020-05-22 09:37:35 -07:00
Leonardo de Moura
ee0fb1bfd8
chore: fix test
...
@Kha
I was having several errors of the form
```
224: /Users/leonardodemoura/projects/lean4/build/release/stage0.5/bin/../include/lean/runtime/exception.h:23:13: error: exception specification of overriding function is more lax than base version
224: virtual ~throwable() noexcept;
224: ^
224: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/exception:102:13: note: overridden virtual function is here
224: virtual ~exception() _NOEXCEPT;
224: ^
224: In file included from myfuns.cpp:1:
```
As far as I can tell, the error ocurrs because my compiler uses an old
C++ standard if the option `-std` is not used.
I guess `-std=c++11` would also works, but I decided to use the same
standard we used to compile Lean.
2020-05-22 09:33:46 -07:00
Sebastian Ullrich
f45fcb4898
test: add tests/compiler/foreign and doc/examples/compiler
2020-05-22 09:22:26 -07:00
Sebastian Ullrich
36e040ecfa
test: reimplement compiler/foreign on top of leanmake
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
5bce603c64
chore: update stage0
2020-05-21 17:17:55 -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
3d166f6400
chore: fix syntax
...
This is a set of examples that exposes problems with the old frontend
elaborator. These issues have been fixed in the new frontend.
2020-05-21 09:57:35 -07:00
Leonardo de Moura
a01552d361
chore: fix some tests
...
Two of them are still broken due to a bug in the new elaborator.
2020-05-21 09:50:20 -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
64f21e0248
chore: update stage0
2020-05-20 17:01:49 -07:00
Leonardo de Moura
f427a6bd3f
feat: new structure instance syntax
2020-05-20 16:57:58 -07:00
Leonardo de Moura
3ea9edbd13
chore: test for simulating old { Prod . ... } syntax
2020-05-20 16:06:57 -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
70c57ce0f0
chore: update stage0
2020-05-20 15:50:51 -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
5aff998aa3
chore: update stage0
2020-05-20 15:30:06 -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
8d9543d9c2
chore: update stage0
2020-05-20 15:09:12 -07:00
Leonardo de Moura
bd58048449
chore: { <source> with ... } syntax
2020-05-20 15:08:43 -07:00
Leonardo de Moura
eef2ca66a1
chore: update stage0
2020-05-20 13:10:12 -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
493cbd5582
chore: update stage0
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
26dab90b1b
chore: update-stage0 output should not depend on locale
2020-05-20 10:35:43 +02:00
Sebastian Ullrich
3c8400d30f
chore: CI: check update-stage0
2020-05-19 11:31:36 -07:00
Leonardo de Moura
9da4f09c67
chore: update stage0
2020-05-19 11:29:32 -07:00
Sebastian Ullrich
6a0410f8f0
feat: make import A import A.olean instead of A/Default.olean
2020-05-19 11:29:32 -07:00
Leonardo de Moura
abbd79a749
chore: update stage0
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
