lean4

Oct 23, 2024

55daa9e · Oct 23, 2024

Name	Name	Last commit message	Last commit date
parent directory ..
Playground	Playground	Add index for DuperXp	Oct 23, 2024
Main.lean	Main.lean	lake init hello	Jul 15, 2022
Playground.lean	Playground.lean	Move some root files into Zulip and revamp annotation script [annotate]	May 20, 2024
README.md	README.md	Add some more in-scope or related stuff	Oct 8, 2024
build.sh	build.sh	Don't run lake update, it causes Mathlib4 to rebuild	Sep 10, 2023
check_noci.sh	check_noci.sh	Add check NoCI to CI, but allow failure	Oct 22, 2024
lake-manifest.json	lake-manifest.json	Now test and annotate can be shared between Lean 4 projects	Oct 22, 2024
lakefile-for-mathlib.lean	lakefile-for-mathlib.lean	Should be `weakLinkArgs`	Jun 12, 2024
lakefile.lean	lakefile.lean	Now test and annotate can be shared between Lean 4 projects	Oct 22, 2024
lean-toolchain	lean-toolchain	Run ./switch.sh to bump Lean to 4.13	Oct 21, 2024
switch.sh	switch.sh	Bump to leanprover/lean4:v4.9.0-rc1	Jun 12, 2024

README.md

See it in action here.

Just trigger it following Quickstart in Lean 4 Manual with the help from the VSCode extension for Lean 4.

lake test

See scripts/test for more details about running individual tests, and test options.

Check out Playground/Zulip/CodeActions.lean.

Explore the following:

Maybe each needs a separate Lean 4 project so these dependencies can be upgraded separately.