sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity
39,843 Commits 4,240 Branches 120 Tags
master
Commit Graph

67 Commits

Author SHA1 Message Date
Henrik Böving
e5f0d6283a chore: update to c++20 (#12117) 
This PR upgrades Lean's internal toolchain to use C++20 as a preparatory
step for #12044.
 2026-02-11 01:17:40 +00:00
Sebastian Ullrich
11be7e8f4a chore: use lld if available for building core (#10694) 2025-10-08 16:47:30 +00:00
Sebastian Ullrich
535435955b chore: remove broken Nix build (#9910) 2025-08-14 08:31:39 +00:00
Sebastian Ullrich
0afcda8654 chore: robustify Nix shell (#8141) 
* use tarballs directly from releases.nixos.org instead of GitHub
zipballs
* build cadical from source like everyone else since it's so small
 2025-04-28 15:08:32 +00:00
Sebastian Ullrich
d57cbdfb95 chore: CI: bring back coredump tracing (#7625) 2025-03-21 15:25:45 +00:00
Henrik Böving
dc7358b4df feat: upgrade cadical to 2.1.2 (#7347) 
This PR upgrades the CaDiCal we ship and use for bv_decide to version
2.1.2. Additionally it enables binary LRAT proofs on windows by default
as https://github.com/arminbiere/cadical/issues/112 has been fixed.

Version 2.1.3 is already available but as the Bitwuzla authors [have
pointed out](https://github.com/bitwuzla/bitwuzla/pull/129) one needs to
be careful when upgrading CaDiCal so we just move to a version [they
confirmed](6e93389d86)
is fine for now.
 2025-03-05 17:58:58 +00:00
Sebastian Ullrich
07b0e5b7fe chore: compile against glibc 2.26 (#7037) 
This PR relaxes the minimum required glibc version for Lean and Lean
executables to 2.26 on x86-64 Linux
 2025-02-12 09:29:51 +00:00
Henrik Böving
e9bd9807ef fix: Windows stage0 linking (#6622) 
This PR fixes stage0 linking on Windows against winsock.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2025-01-14 09:09:50 +01:00
Sebastian Ullrich
c723ae7f97 chore: CI: build 64-bit platforms consistently with GMP 
fix

arm64?

try different fix

`uses_gmp` .olean bit, bump .olean version

add lean_version

make sure to use cache gmp on x86 Linux
 2024-11-01 22:48:49 +11:00
Henrik Böving
9b6696be1d feat: use libuv for tempfiles (#5135) 
This is currently broken because of linker issues. CC @TwoFX

---------

Co-authored-by: Markus Himmel <markus@lean-fro.org>
 2024-10-14 13:56:56 +00:00
Sebastian Ullrich
6d4ec153ad feat: ship cadical (#4325) 
Co-authored-by: Henrik Böving <hargonix@gmail.com>
 2024-08-23 09:13:27 +00:00
Markus Himmel
c237c1f9fb feat: link LibUV (#4963) 2024-08-12 12:33:24 +00:00
Sebastian Ullrich
efc99b982e chore: deprecate Nix-based build, remove interactive components (#4895) 
Users who prefer the flake build should maintain it externally
 2024-08-02 09:57:34 +00:00
Joachim Breitner
6a8cb7ffa0 chore: nix shell: add gdb (#4476) 
seems to work better when it comes from the same nixpkgs that we use for
building, it seems. And is plain convenient.
 2024-06-18 11:07:20 +00:00
Sebastian Ullrich
a8de4b3b06 chore: CI: use Namespace runners (#4427) 2024-06-12 16:06:41 +00:00
Joachim Breitner
2867b93d51 chore: replace shell.nix with a devShell in flake.nix (#3717) 
as a side effect this pins the “old nixpkgs” revision used by CI for
release builds.
(Not that that old branch is likely to change a lot…)
 2024-03-21 13:24:01 +00:00
Connor Baker
667d54640d chore: Nix: use strings instead of URL literals (#2172) 2023-03-28 10:10:24 +02:00
Sebastian Ullrich
4048455060 chore: Nix: fix asan attribute 2023-03-27 16:48:49 +02:00
Sebastian Ullrich
2a7ae7b28a chore: Nix: explicit src 2023-01-26 13:32:42 +01:00
Sebastian Ullrich
6e34c89cbb chore: Nix: comment out rarely used lean-stage0 input 
Optional inputs would be nice.
 2022-11-14 13:12:07 +01:00
Sebastian Ullrich
0f6bda61c9 chore: Nix: buildLeanPackage devShell 2022-07-08 23:24:04 +02:00
Sebastian Ullrich
ab08bffbec chore: Nix: fix stage0-from-input 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
4a1885f997 chore: update benchmark suite 2022-05-25 18:26:36 +02:00
Sebastian Ullrich
19925f8ec1 chore: Nix: move docs build into sub-flake 
workflow is not ideal right now because of poor support for sub-flakes,
but I also don't want the doc input in the main flake...
 2022-03-26 22:50:04 +01:00
Sebastian Ullrich
720e445755 chore: Nix: update inputs 2022-03-24 12:33:33 +01:00
Sebastian Ullrich
b20ecd02d7 chore: move out lean4-mode 2022-01-24 21:23:53 +01:00
Sebastian Ullrich
5a16745ad9 chore: Nix: add devShell 2021-12-17 09:43:22 +01:00
Michael Burge
6d57299396 chore: set Nix flake's defaultPackage to lean-all for interactive use 
Allows Nix flake to run tutorial and other simple examples out-of-the-box.

Closes #858
 2021-12-09 12:06:25 +01:00
Sebastian Ullrich
e0869bdf55 fix: sanitized build 2021-09-08 17:24:31 +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
e121ae0d78 chore: turn off -Bsymbolic-functions in sanitized build 2021-08-18 13:54:52 +02:00
Wojciech Nawrocki
d92e4a7cf1 chore: restore LEANC_EXTRA_FLAGS 
We now pass them to both compilers and linkers. For example, -pthread should be given to both: https://stackoverflow.com/questions/2127797/significance-of-pthread-flag-when-compiling
 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
c772dc49ef chore: use leanc for all C code 2021-06-06 15:34:44 +02:00
Sebastian Ullrich
7ebe80ad2a chore: update Nix, Nixpkgs, vscode-lean4 2021-06-06 15:00:40 +02:00
Sebastian Ullrich
20cbb4389a fix: Nix: VS Code override 2021-04-21 12:21:02 +02:00
Sebastian Ullrich
e1e5ad30ae chore: Nix: update VS Code 2021-04-11 23:03:56 +02:00
Sebastian Ullrich
c74dd7c683 chore: Nix: stage0debug 2021-01-20 16:48:50 +01:00
Sebastian Ullrich
9ecabe5a06 feat: Nix: integrate vscode-lean4 2021-01-03 19:58:46 +01:00
Sebastian Ullrich
4e3025fe81 feat: Nix: use HEAD as stage0 2020-12-16 18:52:39 +01:00
Sebastian Ullrich
ad5f8f021d feat: Nix: thread-sanitized build 2020-11-29 18:59:39 +01:00
Sebastian Ullrich
03acc5ea1f feat: Nix: sanitized build 2020-11-29 14:08:53 +01:00
Sebastian Ullrich
c432ca72d6 feat: Nix: template for custom packages 2020-11-28 17:36:20 +01:00
Sebastian Ullrich
3a4b61f8c7 feat: Nix: debug builds 2020-11-28 12:37:35 +01:00
Sebastian Ullrich
2c64441910 chore: Nix: disable dirty Git tree warning & fix lean4-diff-test-file 
/cc @leodemoura

Note that you will have to restart Emacs and the "Lean shell" around it for the changes to take effect
 2020-11-24 20:05:24 +01:00
Sebastian Ullrich
6be577b634 fix: CI: Linux release job 2020-11-24 19:16:27 +01:00
Sebastian Ullrich
3e8693fac8 fix: Nix: provide .#lean-package etc. from Lean package 2020-11-24 19:16:27 +01:00
Sebastian Ullrich
e0d9bc2f9b chore: Nix: simplify flake.nix after all and fix shell.nix 2020-11-24 19:16:27 +01:00
Sebastian Ullrich
a5ad46f7be feat: Nix: mdbook 2020-11-24 19:16:27 +01:00
Sebastian Ullrich
58d97def40 chore: Nix: cache .o files on macOS as well 2020-11-24 19:16:27 +01:00