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

70 commits

Author SHA1 Message Date
Sebastian Ullrich
3b4b2cc89d
fix: do not dllexport symbols in core static libraries (#3601) 
On Windows, we now compile all core `.o`s twice, once with and without
`dllexport`, for use in the shipped dynamic and static libraries,
respectively. On other platforms, we export always as before to avoid
the duplicate work.

---------

Co-authored-by: tydeu <tydeu@hatpress.net>
 2024-03-15 11:58:34 +00:00
Sebastian Ullrich
fb2ec54b60
chore: build Lean .os in parallel to rest of core (#3682) 
Previously, we only did `Init/*.{o,olean}+Lean/*.olean` in parallel
 2024-03-14 15:14:37 +00:00
Sebastian Ullrich
61fba365f2
fix: revert shared library split on non-Windows platforms (#3529) 
Avoids the performance hit and fixes #3528.
 2024-02-29 19:15:01 +00:00
Sebastian Ullrich
4d94147643
chore: build Lean in parallel to Init (#3455) 
A, for now, less problematic subset of #3103
 2024-02-23 10:44:58 +00:00
Sebastian Ullrich
8193af33e3
fix: split libInit_shared out of libleanshared (#3421) 
Avoids hitting the Windows limit on symbols per shared library soon
 2024-02-22 19:16:32 +00:00
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