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

311 commits

Author SHA1 Message Date
Sebastian Ullrich
7809b269ca chore: avoid xargs in update-stage0 2022-11-20 10:22:20 -08:00
Leonardo de Moura
9022fb8d48 fix: custom update-stage0 for osx 2022-11-19 19:20:13 -08:00
Sebastian Ullrich
9f2182fdd9 chore: update script/apply.lean semantics 2022-11-07 19:47:04 -08:00
Sebastian Ullrich
5be816244e chore: update script/apply.lean syntax 2022-11-07 19:47:04 -08:00
Siddharth
e3f064ef87
Bump up to LLVM 15 (#1691) 2022-10-14 14:43:13 +00: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
Sebastian Ullrich
4934104eaf chore: update script/reformat.lean 2022-05-13 11:55:44 +02:00
Sebastian Ullrich
c755aa81bd fix: properly distinguish between internal and public linker flags 2022-05-02 13:53:52 +02:00
Sebastian Ullrich
4a9bc88a4e chore: fix USE_GMP=OFF by removing GMP linking customization 2022-03-26 16:29:52 +01:00
Sebastian Ullrich
7ce5b0c4ff feat: CI: build darwin_aarch64 2022-03-26 16:29:52 +01:00
Sebastian Ullrich
7e853621eb feat: CI: build linux_aarch64 2022-03-25 17:45:15 +01:00
Sebastian Ullrich
e49949b781 chore: prepare-llvm-linux: fix include path order 
should really be `-isystem-after`, but clang ignores it...??
 2022-03-24 12:33:33 +01:00
Sebastian Ullrich
75b3012a37 chore: prepare-llvm-linux: stop relying on /usr 2022-03-24 12:33:33 +01:00
Sebastian Ullrich
bba0baf92c chore: CI: I'm sure they work fine 2022-03-22 12:22:23 +01:00
Sebastian Ullrich
82049c519c chore: CI: fix MinGW library root 2022-03-22 12:22:23 +01:00
Sebastian Ullrich
f3279824a3 fix: Windows: do not use standard sysroot 2022-01-30 17:43:14 +01:00
Sebastian Ullrich
ccf1292e07 fix: rework header/lib handling with bundled clang 
* use `-nostdinc` to make sure system headers don't affect us
* include clang headers with `-isystem`, which suppresses all those warnings
* do not use default sysroot on Windows after all, since that can be a
  surprising location

Fixes #922
 2022-01-20 16:05:54 +01:00
Sebastian Ullrich
068ea1beb4 fix: leanc: do not change sysroot 
Apparently clang is smart enough to look up runtime files missing from
the sysroot in the installation directory automatically.
 2021-12-19 18:55:57 +01:00
Gabriel Ebner
448d2cd951 feat: add script to reformat lean files 2021-12-15 11:42:38 +00:00
Sebastian Ullrich
8f88b1f3f8 feat: bundle llvm-ar with Lean 2021-11-25 15:05:06 +01:00
Sebastian Ullrich
ad10495afa chore: macOS: build with system c++ 2021-11-20 11:04:39 +01:00
Sebastian Ullrich
99aee53172 fix: restore macOS compile flags 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
74a616a965 chore: final cleanup? 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
ad2fe8de80 feat: bundle LLVM on macOS 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
3db3fb1429 feat: bundle LLVM on Windows 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
749158c8c1 perf: strip LLVM binaries 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
27bc6397a0 fix: actually link against GMP statically 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
42ee91bcda fix: Linux: bundle zlib 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
8f4e59d9b5 chore: update lean-llvm 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
2cb625e9c4 chore: update lean-llvm 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
b236273780 feat: link external dependencies statically again 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
5bbc160f4b feat: use custom, more minimal LLVM build 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
d2a1e20dd0 feat: bundling LLVM on Linux 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
524be36d23 feat: build & bundle Lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
4ac9873880 fix: update-stage0 2021-10-07 12:55:55 +02: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
eb72fba635 refactor: build C files using leanmake/leanc in stage 0 as well 2021-08-18 13:54:52 +02:00
Wojciech Nawrocki
c772dc49ef chore: use leanc for all C code 2021-06-06 15:34:44 +02:00
Sebastian Ullrich
6664f58a0e chore: link lean using leanc 2021-03-06 10:17:50 +01:00
Sebastian Ullrich
8a3808bd45 chore: nightly releases 2021-01-04 13:46:20 +01:00
Sebastian Ullrich
65c1bc8952 fix: gen_constants_cpp.py: mark constants as persistent 2020-11-29 18:59:39 +01:00
Sebastian Ullrich
ab6b1b4918 chore: delete obsolete scripts 2020-10-14 19:14:00 +02:00
Sebastian Ullrich
c077363c43 chore: delete horrible CamelCase conversion scripts no-one should ever use again 2020-10-14 19:09:47 +02:00
Sebastian Ullrich
d5f58d27b0 chore: delete StyleCheck 2020-10-14 19:07:52 +02:00
Sebastian Ullrich
485a1d67f8 chore: update CI 2020-06-10 21:30:38 +02:00
Sebastian Ullrich
26dab90b1b chore: update-stage0 output should not depend on locale 2020-05-20 10:35:43 +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
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