max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
32176 commits 1 branch 0 tags 5.3 GiB
Find a file
Mac Malone a48ca7b0a4
feat: lake: improved platform information & control (#3226) 
This combines a few platform-related changes:

* Add a ternary `platformIndependent` Lean configuration option to
assert whether Lake should assume Lean code is platform-independent. If
`true`, Lake will exclude platform-independent objects like external
libraries or dynlibs created through `precompileModules` from module
traces. If `false`, Lake will add the platform to module traces. If
`none` (the default), Lake will retain the current behavior (modules are
platform-dependent if and only if it depends on native objects).
* Use `System.Platform.target` from #3207 as the platform descriptor in
Lake for the configuration file trace, the cloud release archive, and as
the platform trace in Lean modules and native artifacts (e.g., object
files, and static and shared libraries).
* Do not add the platform descriptor into custom build archive names
(i.e., a user-set `buildArchive` configuration). This allows users to
create cross-platform / platform-independent archives via a name
override should they so desire.

Closes #2754.
2024-01-31 23:56:33 +00:00
.github chore: remove unused GH Pages deployment (#3217) 2024-01-31 10:39:15 +00:00
doc doc: update link target (#3218) 2024-01-26 10:20:22 +00:00
images
nix chore: set warningAsError in CI only (#3030) 2023-12-06 08:18:39 +00:00
script chore: refactor pr release workflow (#3020) 2023-12-12 00:45:10 +00:00
src feat: lake: improved platform information & control (#3226) 2024-01-31 23:56:33 +00:00
stage0 chore: update stage0 2024-01-31 15:48:29 +00:00
tests feat: @[unused_variables_ignore_fn] attribute (#3184) 2024-01-31 19:27:32 +00:00
.gitattributes chore: Do not hide stage0/src/stdlib_flags.h from diffs 2023-09-13 19:29:25 +02:00
.gitignore chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
.ignore chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
CMakeLists.txt feat: embed and check githash in .olean (#2766) 2023-11-27 10:24:43 +00:00
CODEOWNERS doc: widget code owner 2023-12-01 15:46:45 +00:00
CONTRIBUTING.md doc: Adjust contributor's docs to squash merging (#2927) 2023-11-21 10:13:43 +00:00
default.nix doc: setup 2021-01-03 13:21:58 +01:00
flake.lock chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00
flake.nix chore: Nix: use strings instead of URL literals (#2172) 2023-03-28 10:10:24 +02:00
lean-toolchain doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00
lean.code-workspace chore: add the lean4 extension to the vscode workspace (#3059) 2023-12-14 08:58:21 +00:00
LICENSE chore: remove LICENSE header that confused GitHub 2021-11-18 09:42:35 +01:00
LICENSES chore: add GMP license for now 2021-11-18 09:42:35 +01:00
README.md doc: remove nightly and other outdated references (#3027) 2024-01-25 13:53:36 +00:00
RELEASES.md feat: elidible subterms (#3201) 2024-01-31 17:28:29 +00:00
shell.nix chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.