Sebastian Ullrich
|
b3a85631d8
|
chore: set warningAsError in CI only (#3030)
Don't fail local builds because of this
|
2023-12-06 08:18:39 +00:00 |
|
Alexander Bentkamp
|
7dc1618ca5
|
feat: Web Assembly Build (#2599)
Co-authored-by: Rujia Liu <rujialiu@user.noreply.github.com>
|
2023-10-04 09:04:20 +02:00 |
|
tydeu
|
d29b8e5422
|
chore: remove binaries before building them
This is required to avoid "permission denied" errors on Windows if the the file is already in use.
|
2023-08-23 14:33:27 -04:00 |
|
Siddharth Bhat
|
146296b5fa
|
feat: enable LLVM in stage1+ compiler
|
2023-08-14 13:33:46 +02:00 |
|
tydeu
|
8de1c0786c
|
chore: make Lean build shell configurable
|
2023-08-07 23:05:37 +02:00 |
|
Sebastian Ullrich
|
d991f5efe0
|
fix: ship libLake.a
|
2023-07-21 09:19:19 +02:00 |
|
Sebastian Ullrich
|
bcd1673231
|
chore: abort build on panic
|
2022-11-11 16:24:04 +01:00 |
|
Mario Carneiro
|
37252e5fa7
|
chore: remove Bootstrap package
|
2022-09-02 16:39:03 -07:00 |
|
Mario Carneiro
|
bf89c5a0f5
|
chore: move Std -> Bootstrap
|
2022-08-29 01:26:12 -07:00 |
|
Leonardo de Moura
|
713108b7ba
|
chore: re-enable warningAsError
|
2022-08-13 18:07:30 -07:00 |
|
Leonardo de Moura
|
d87d0f47a6
|
chore: temporarily disable warningAsError
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
f4de40d7dc
|
feat: turn on warningAsError
|
2022-07-29 10:31:19 -07:00 |
|
Sebastian Ullrich
|
4a9bc88a4e
|
chore: fix USE_GMP=OFF by removing GMP linking customization
|
2022-03-26 16:29:52 +01:00 |
|
Sebastian Ullrich
|
a7ba103e0a
|
chore: remove leanpkg
|
2022-02-04 19:03:40 +01:00 |
|
Sebastian Ullrich
|
524be36d23
|
feat: build & bundle Lake
|
2021-10-15 06:56:02 -07:00 |
|
Sebastian Ullrich
|
89d6c70273
|
fix: macOS build
|
2021-10-08 18:34:28 +02:00 |
|
Sebastian Ullrich
|
e6927253cf
|
feat: use leanc written in Lean for testing & distribution
building is still handled by a (minimal) Bash script for bootstrapping purposes
|
2021-09-25 09:59:50 +02:00 |
|
Sebastian Ullrich
|
0a6778d05f
|
chore: silence clang warning when exporting Lean function declared in lean.h
|
2021-09-20 18:41:46 +02:00 |
|
Sebastian Ullrich
|
c5940f0149
|
fix: cmake/make dependencies
|
2021-09-09 18:12:55 +02:00 |
|
Sebastian Ullrich
|
a97621467f
|
fix: stdlib.make: missing target
|
2021-09-08 17:24:31 +02:00 |
|
Sebastian Ullrich
|
68a3799b7c
|
refactor: build lean in stdlib.make
|
2021-09-08 17:24:31 +02:00 |
|
Sebastian Ullrich
|
9702fe1981
|
chore: leanc: use C instead of C++ compiler
|
2021-09-08 17:24:31 +02:00 |
|
Sebastian Ullrich
|
82c97d34fa
|
chore: specify accurate dependencies for leanshared
|
2021-08-20 09:42:05 -07:00 |
|
Sebastian Ullrich
|
5f4b1b1d44
|
Revert "Revert "feat: reintroduce libleanshared, link lean & leanpkg against it""
This reverts commit ccbc9d00db.
|
2021-08-20 09:42:05 -07:00 |
|
Sebastian Ullrich
|
ccbc9d00db
|
Revert "feat: reintroduce libleanshared, link lean & leanpkg against it"
|
2021-08-20 15:39:00 +02:00 |
|
Sebastian Ullrich
|
88f3de7a44
|
chore: link leanshared using leanc after all
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
68ecda843b
|
chore: remove STATIC cmake flag
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
df5c1b2a3b
|
chore: fix leanshared flags
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
eb72fba635
|
refactor: build C files using leanmake/leanc in stage 0 as well
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
f46e853899
|
chore: fix Windows link flags
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
92403ae7e1
|
chore: move -fno-semantic-interposition to the right place
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
b0167c6ab0
|
fix: leanpkg rpath
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
617f17facb
|
feat: reintroduce libleanshared, link lean & leanpkg against it
|
2021-08-18 13:54:52 +02:00 |
|
Sebastian Ullrich
|
917eb4d081
|
chore: collect stdlib compilation flags in new header
|
2021-08-12 07:51:50 -07:00 |
|
Sebastian Ullrich
|
efa9369097
|
chore: restore prefer_native flag
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
da4c46370d
|
feat: store elaborator declaration name in info tree
|
2021-06-21 10:17:26 -07:00 |
|
Wojciech Nawrocki
|
c772dc49ef
|
chore: use leanc for all C code
|
2021-06-06 15:34:44 +02:00 |
|
Wojciech Nawrocki
|
4d7ccc7c72
|
feat: Lean.js can compile itself
|
2021-06-06 15:34:44 +02:00 |
|
Sebastian Ullrich
|
ae9b2131c1
|
chore: reset prefer_native
|
2021-04-29 13:37:41 +02:00 |
|
Sebastian Ullrich
|
73cf3533a1
|
fix: count quotation depth in parser correctly
|
2021-04-29 13:33:48 +02:00 |
|
Sebastian Ullrich
|
5644cee2d6
|
chore: reset prefer_native
|
2021-04-05 13:58:15 +02:00 |
|
Sebastian Ullrich
|
98e1baabbd
|
refactor: make trailingNode clean up after itself
Also resolves an issue with emitting both `left` and a partial tree
containing it
|
2021-04-05 13:51:03 +02:00 |
|
Sebastian Ullrich
|
9f6436ebfd
|
chore: reset prefer_native
|
2021-03-22 16:33:37 +01:00 |
|
Sebastian Ullrich
|
725c0c1911
|
chore: implement lhs prec
|
2021-03-22 16:33:37 +01:00 |
|
Sebastian Ullrich
|
c7347bbe0f
|
fix: that's not how Makefiles work
|
2021-01-27 12:34:48 +01:00 |
|
Sebastian Ullrich
|
5fea8fcba3
|
fix: statically link GMP into leanpkg if STATIC=ON
|
2021-01-25 15:24:16 +01:00 |
|
Sebastian Ullrich
|
ddabe1aa6f
|
chore: alternative fix to 15185a1
|
2021-01-25 10:34:34 +01:00 |
|
Leonardo de Moura
|
8bc88bde6b
|
chore: undefine LEAN_PATH
@Kha This doesn't work on my machine. It seems this is a GNU make feature.
|
2021-01-24 17:52:14 -08:00 |
|
Sebastian Ullrich
|
15185a1775
|
fix: unset LEAN_PATH before building stdlib
|
2021-01-24 19:41:16 +01:00 |
|
Sebastian Ullrich
|
02a4383afb
|
fix: stdlib.make
|
2021-01-10 18:10:22 +01:00 |
|