Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
Find a file
Reijo Jaakkola 32897440dc
fix: change IO.FS.Handle.read to return empty array at EOF
Make EOF handling in IO.FS.Handle consistent with EOF handling in
IO.FS.Handle.getLine. Previously returned error at EOF which ended up
causing segmentation fault. Remove the declaration of g_io_error_eof,
since it becomes redundant.

Closes #349
2021-06-08 13:17:53 +02:00
.github chore: restore LEANC_EXTRA_FLAGS 2021-06-06 15:34:44 +02:00
doc doc: clarify RFC issues 2021-06-04 14:12:59 +02:00
images
lean4-mode chore: lean4-mode: prefer cdot on \. 2021-06-07 13:16:41 +02:00
nix chore: update Nix, Nixpkgs, vscode-lean4 2021-06-06 15:00:40 +02:00
script chore: use leanc for all C code 2021-06-06 15:34:44 +02:00
src fix: change IO.FS.Handle.read to return empty array at EOF 2021-06-08 13:17:53 +02:00
stage0 chore: update stage0 2021-06-07 12:10:10 +02:00
tests fix: change IO.FS.Handle.read to return empty array at EOF 2021-06-08 13:17:53 +02:00
tmp chore: remove tactic framework dependency 2020-11-10 14:32:58 -08:00
.gitattributes chore: restore marking stage0/ as binary files, which we lost at some point 2020-08-14 11:12:13 +02:00
.gitignore chore: ignore result files from nix build 2020-11-24 19:16:27 +01:00
CMakeLists.txt feat: Lean.js can compile itself 2021-06-06 15:34:44 +02:00
CONTRIBUTING.md doc: more changes 2021-05-13 16:11:57 -07:00
default.nix doc: setup 2021-01-03 13:21:58 +01:00
flake.lock chore: update Nix, Nixpkgs, vscode-lean4 2021-06-06 15:00:40 +02:00
flake.nix chore: restore LEANC_EXTRA_FLAGS 2021-06-06 15:34:44 +02:00
LICENSE
README.md doc: contribution guidelines & README update 2021-01-12 14:38:36 -08:00
shell.nix doc: update dev setup editor instructions 2021-02-02 17:30:51 +01:00

This is the repository for Lean 4, which is currently being released as milestone releases towards a first stable release. Lean 3 is still the latest stable release.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.