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

187 commits

Author SHA1 Message Date
euprunin
cda6733f97
chore: fix spelling mistakes in non-Lean files (#5430) 
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
 2024-09-23 21:11:20 +00:00
Sebastian Ullrich
c2761dc270
feat: Lake shared library (#5143) 
Fixes #2436 #5050

Next step: when libLake_shared is in stage 0, --load-dynlib it when
building stage 1 Lake
 2024-09-09 09:05:54 +00:00
Markus Himmel
c237c1f9fb
feat: link LibUV (#4963) 2024-08-12 12:33:24 +00:00
David Thrane Christiansen
8fef03d1cc
feat: support Lake for building Lean core oleans (#3886) 
This is from a ~~pair~~triple programming session with @tydeu and
@mhuisi.

If stage 1 is built with `-DUSE_LAKE=ON`, the CMake run will generate
`lakefile.toml` files for the root, `src`, and `tests`. These Lake
configuration files can then be used to build core oleans. While they do
not yet allow Lake to be used to build the Lean binaries. they do allow
Lake to be used for working interactively with the Lean source. In our
preliminary experiments, this allowed updates to `Init.Data.Nat` to be
noticed automatically when reloading downstream files, rather than
requiring a full manual compiler rebuild. This will make it easier to
work on the system.

As part of this change, Lake is added to stage 0. This allows Lake to
function in `src`, which uses the stage 0 toolchain.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2024-06-13 16:18:24 +00:00
Joachim Breitner
74adb0961c
chore: add ./script/rebase-stage0.sh (#3984) 
heavily based on an script by Kim.
 2024-05-02 12:26:25 +00:00
Kim Morrison
f2a54ec0eb
feat: script to summarize issues (#3952) 2024-04-24 06:11:07 +00:00
Sebastian Ullrich
2dcd42f395
feat: trace.profiler export to Firefox Profiler (#3801) 
Reusing the best profiling UI out there

Usage:
```
lean -Dtrace.profiler=true -Dtrace.profiler.output=profile.json foo.lean ...
```
then open `profile.json` in https://profiler.firefox.com/.

See also `script/collideProfiles.lean` for minimizing and merging
profiles.
 2024-04-15 12:13:14 +00:00
Sebastian Ullrich
992000a672
fix: C++ exceptions across shared libraries on Linux (#3500) 
Server interruptions in C++ started to fail after #3421
 2024-02-26 10:35:11 +00:00
Scott Morrison
8b8e001794
chore: add missing copyright headers (#3411) 2024-02-20 01:49:55 +00:00
Joachim Breitner
fa26d222cb
chore: refactor pr release workflow (#3020) 
In particular:

* Do not use deprecated `potiuk/get-workflow-origin`.
* Use a bare checkout to push PR to `pr-releases`
* Replace `script/most-recent-nightly-tag.sh` by a one-liner inside the
workflow, so that th workflow is self-contained
 2023-12-12 00:45:10 +00:00
Scott Morrison
a422f3f2c9
chore: script/most-recent-nightly-tag uses https rather than ssh repo URL (#2951) 
The https URL suffices, and does not require that the caller has an
appropriate ssh key.
 2023-11-23 10:27:46 +00:00
Scott Morrison
9efdde23e0
fix: most-recently-nightly-tag does not assume a 'nightly' remote (#2947) 
`script/most-recent-nightly-tag.sh` determines the most recent nightly
release in your current git history.

Previously it was assuming that you had a `nightly` remote, to pull tags
from. Now it just pulls directly from the repository by URL.
 2023-11-22 10:56:39 +00:00
Scott Morrison
f201f63e49
chore: fix identification of most recent nightly tag (#2827) 2023-11-06 03:53:06 +00:00
Scott Morrison
da32b5f837
feat: use nightly-testing-YYYY-MM-DD branches on Mathlib for testing PRs, and be more conservative about launching Mathlib CI (#2798) 2023-11-02 12:07:06 +11:00
int-y1
ce4ae37c19 chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
Siddharth Bhat
496460020a fix: disabling forwarding --target to lean. 
This will ensure that we do not invoke `lean --target` without compiling
using LLVM.
 2023-08-14 13:33:46 +02:00
Henrik
8d3af73853 feat: Linux LLVM CI for stage1+ 2023-08-14 13:33:46 +02:00
Siddharth Bhat
146296b5fa feat: enable LLVM in stage1+ compiler 2023-08-14 13:33:46 +02:00
Sebastian Ullrich
53477089fe chore: remove unused macOS dependencies 2023-07-26 15:36:36 +02:00
Sebastian Ullrich
978a5b2528 fix: loading libc++ on macOS Sonoma 2023-07-26 15:36:36 +02:00
Sebastian Ullrich
90aab46071 chore: fix update-stage0 2023-07-17 10:38:35 +02:00
Sebastian Ullrich
092e26179b chore: fix script/reformat.lean 2022-11-28 15:47:17 +01:00
Gabriel Ebner
1e79d659f2 chore: bundle libatomic in releases 2022-11-23 16:42:37 -08:00
Siddharth
4d47c8abc6
feat: add LLVM C API bindings (#1497) 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2022-11-21 09:50:01 +01:00
Sebastian Ullrich
9c3a283eb1 chore: update-stage0: simplify 2022-11-20 10:22:20 -08:00
Sebastian Ullrich
5053cb02b7 chore: don't copy .lean files to stage0 2022-11-20 10:22:20 -08:00
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