mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
40e8f4c5fb
This PR turns on the new `do` elaborator in Init, Lean, Std, Lake and the testsuite. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
97 lines
2.8 KiB
TOML
97 lines
2.8 KiB
TOML
# This file allows lake to build Lean, Init, and Lake as Lean libraries.
|
|
#
|
|
# This is the file used when working with the stage0 compiler on the libraries
|
|
#
|
|
# It is not yet possible to build the compiler and other tooling executables with Lake; to build
|
|
# them, please consult the instructions in doc/dev/index.md.
|
|
|
|
name = "lean4"
|
|
bootstrap = true
|
|
|
|
defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc", "LeanChecker"]
|
|
|
|
# Have Lake use CMake's build type (e.g., `Release`, `Debug`) where possible
|
|
buildType = "${CMAKE_BUILD_TYPE_TOML}"
|
|
|
|
# The root of all the compiler output directories
|
|
buildDir = "${CMAKE_BINARY_DIR}"
|
|
|
|
# Enables the Lake artifact cache if configured via CMake
|
|
# (i.e., for stage 1 when the CMake `USE_LAKE_CACHE` option is set).
|
|
enableArtifactCache = ${LAKE_ARTIFACT_CACHE_TOML}
|
|
|
|
# Ensure build artifacts end up in the build directory even when the Lake
|
|
# local artifact cache is enabled. This is necessary because subsequent stages
|
|
# will expect the previous stage's artifacts to be in the build directory.
|
|
restoreAllArtifacts = true
|
|
|
|
# Lean expects its libraries to always have a `lib` prefix
|
|
libPrefixOnWindows = true
|
|
|
|
# The directory of Lean source files (i.e., `src`)
|
|
srcDir = "${LEAN_SOURCE_DIR}"
|
|
|
|
# Destination C files and other intermediate representations
|
|
irDir = "lib/temp"
|
|
|
|
# Destination for olean files
|
|
leanLibDir = "lib/lean"
|
|
|
|
# Destination for static libraries
|
|
nativeLibDir = "lib/lean"
|
|
|
|
# Additional options derived from the CMake configuration
|
|
# For example, CI will set `-DwarningAsError=true` through this
|
|
moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]
|
|
|
|
# Uncomment to limit number of reported errors further in case of overwhelming cmdline output
|
|
#weakLeanArgs = ["-DmaxErrors=1"]
|
|
|
|
${LEAN_EXTRA_LAKEFILE_TOML}
|
|
|
|
[[lean_lib]]
|
|
name = "Init"
|
|
defaultFacets = ["static", "static.export"]
|
|
leanOptions = { backward.do.legacy = false }
|
|
|
|
[[lean_lib]]
|
|
name = "Std"
|
|
defaultFacets = ["static", "static.export"]
|
|
leanOptions = { backward.do.legacy = false }
|
|
|
|
[[lean_lib]]
|
|
name = "Lean"
|
|
defaultFacets = ["static", "static.export"]
|
|
leanOptions = { backward.do.legacy = false }
|
|
globs = [
|
|
# Library root
|
|
"Lean",
|
|
# Deliberate orphan file so `import Lean` does not induce an LLVM dependency
|
|
"Lean.Compiler.IR.EmitLLVM",
|
|
# New compiler orphan file used in tests
|
|
"Lean.Compiler.LCNF.Probing",
|
|
]
|
|
|
|
[[lean_lib]]
|
|
name = "Lake"
|
|
srcDir = "lake"
|
|
# Build Lake and all its submodules (which may not be imported elsewhere)
|
|
globs = ["Lake.*"]
|
|
defaultFacets = ["static", "static.export"]
|
|
leanOptions = { backward.do.legacy = false }
|
|
|
|
[[lean_lib]]
|
|
name = "LakeMain"
|
|
srcDir = "lake"
|
|
defaultFacets = ["static.export"]
|
|
leanOptions = { backward.do.legacy = false }
|
|
|
|
[[lean_lib]]
|
|
name = "Leanc"
|
|
srcDir = "${CMAKE_BINARY_DIR}/leanc"
|
|
defaultFacets = ["static"]
|
|
|
|
[[lean_lib]]
|
|
name = "LeanChecker"
|
|
defaultFacets = ["static"]
|