Date: Mon, 24 Nov 2025 18:27:01 +0000 From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: ecfba1814540 - main - math/lean4: update 4.23.0=?utf-8?Q? =E2=86=92 4.2?=5.1 Message-ID: <6924a375.c5a8.550faf91@gitrepo.freebsd.org>
next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=ecfba1814540c148bd24a243b22d01742643f99d commit ecfba1814540c148bd24a243b22d01742643f99d Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2025-11-24 18:07:21 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2025-11-24 18:26:56 +0000 math/lean4: update 4.23.0 → 4.25.1 --- math/lean4/Makefile | 19 +- math/lean4/distinfo | 6 +- math/lean4/files/patch-src_CMakeLists.txt | 17 +- math/lean4/files/patch-src_shell_CMakeLists.txt | 11 + math/lean4/files/patch-stage0_src_CMakeLists.txt | 17 +- .../patch-stage0_src_runtime_stack__overflow.cpp | 8 - .../files/patch-stage0_src_shell_CMakeLists.txt | 11 + math/lean4/files/patch-tests_lakefile.toml | 10 + math/lean4/pkg-plist | 1813 ++++++++++++++++---- 9 files changed, 1603 insertions(+), 309 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index c6d417be8716..c9e5174d7163 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.23.0 +DISTVERSION= 4.25.1 CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment MAINTAINER= yuri@FreeBSD.org @@ -32,7 +32,6 @@ CXXFLAGS+= -fPIC CMAKE_OFF= USE_MIMALLOC #MAKE_ARGS+= V=1 VERBOSE=1 -#MAKE_JOBS_UNSAFE= yes MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} @@ -48,6 +47,19 @@ pre-everything:: @${ECHO_MSG} " # mount /proc" @${ECHO_MSG} "" +post-patch: + # Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files + @${FIND} ${WRKSRC}/tests -name "lakefile.toml" | while read f; do \ + ${GREP} -q "weakLeancArgs" "$$f" || \ + ( ${PRINTF} 'weakLeancArgs = ["-fPIC"]\n\n' | cat - "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f" ); \ + done + # Add weakLeancArgs to lakefile.lean files that define packages + @${FIND} ${WRKSRC}/tests -name "lakefile.lean" | while read f; do \ + if ${GREP} -q "^package .* where" "$$f" && ! ${GREP} -q "weakLeancArgs" "$$f"; then \ + ${AWK} '/^package .* where$$/ {print; print " weakLeancArgs := #[\"-fPIC\"]"; next} 1' "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f"; \ + fi; \ + done + post-install: # remove empty dirs @${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete @@ -65,7 +77,6 @@ post-install: lib/lean/libleanshared_1.so \ lib/lean/libLake_shared.so -# tests as of 4.20.0: 99% tests passed, 16 tests failed out of 2594, see https://github.com/leanprover/lean4/issues/8628 -# tests as of 4.23.0: 99% tests passed, 10 tests failed out of 2870 +# tests as of 4.25.1: 100% tests passed, 0 tests failed out of 3241 .include <bsd.port.mk> diff --git a/math/lean4/distinfo b/math/lean4/distinfo index da328bb6517b..5dc69960b21c 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1758525947 -SHA256 (leanprover-lean4-v4.23.0_GH0.tar.gz) = 1820cc8fc09f439c448ea39cc14f90e73058c55b12b5aa5cf4d2ca86f0c89099 -SIZE (leanprover-lean4-v4.23.0_GH0.tar.gz) = 45087678 +TIMESTAMP = 1763958547 +SHA256 (leanprover-lean4-v4.25.1_GH0.tar.gz) = 0999ae6aed95eeb4d059142f2a4bd491d10168f8f348f711a767e320d54fea0a +SIZE (leanprover-lean4-v4.25.1_GH0.tar.gz) = 50069728 diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt index d7658e68a521..d71c117b8802 100644 --- a/math/lean4/files/patch-src_CMakeLists.txt +++ b/math/lean4/files/patch-src_CMakeLists.txt @@ -1,6 +1,6 @@ ---- src/CMakeLists.txt.orig 2025-05-07 10:26:21 UTC +--- src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +++ src/CMakeLists.txt -@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") +@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") @@ -14,10 +14,21 @@ + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") + string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") ++ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") -@@ -801,7 +811,7 @@ endif() +@@ -586,6 +597,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu + # Lean code only needs this one include + string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include") + ++# Include extra flags (e.g., -fPIC on FreeBSD) ++string(APPEND LEANC_OPTS " ${LEANC_EXTRA_FLAGS}") ++ + # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc` + string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) + string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") +@@ -814,7 +828,7 @@ endif() file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) endif() diff --git a/math/lean4/files/patch-src_shell_CMakeLists.txt b/math/lean4/files/patch-src_shell_CMakeLists.txt new file mode 100644 index 000000000000..3858f69f9aa7 --- /dev/null +++ b/math/lean4/files/patch-src_shell_CMakeLists.txt @@ -0,0 +1,11 @@ +--- src/shell/CMakeLists.txt.orig 2025-11-17 18:29:21 UTC ++++ src/shell/CMakeLists.txt +@@ -57,7 +57,7 @@ if(${EMSCRIPTEN}) + endif() + + # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers +-set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") ++set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") + + set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${LEAN_BIN}) + diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt index 184415ffa3d9..7ec7241aa2f2 100644 --- a/math/lean4/files/patch-stage0_src_CMakeLists.txt +++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt @@ -1,6 +1,6 @@ ---- stage0/src/CMakeLists.txt.orig 2025-05-06 09:12:17 UTC +--- stage0/src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +++ stage0/src/CMakeLists.txt -@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") +@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") @@ -14,10 +14,21 @@ + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") + string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") ++ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") -@@ -798,7 +808,7 @@ endif() +@@ -586,6 +597,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu + # Lean code only needs this one include + string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include") + ++# Include extra flags (e.g., -fPIC on FreeBSD) ++string(APPEND LEANC_OPTS " ${LEANC_EXTRA_FLAGS}") ++ + # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc` + string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) + string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") +@@ -814,7 +828,7 @@ endif() file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) endif() diff --git a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp index 638daf3af176..cb4949c8e4d2 100644 --- a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp +++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp @@ -11,11 +11,3 @@ #ifdef LEAN_WINDOWS #include <windows.h> #else -@@ -20,6 +24,7 @@ Port of the corresponding Rust code (see links below). - #include <lean/lean.h> - #include <initializer_list> - #include "runtime/stack_overflow.h" -+ - - namespace lean { - // stack guard of the main thread diff --git a/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt new file mode 100644 index 000000000000..075908dbdd63 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt @@ -0,0 +1,11 @@ +--- stage0/src/shell/CMakeLists.txt.orig 2025-11-17 18:29:21 UTC ++++ stage0/src/shell/CMakeLists.txt +@@ -57,7 +57,7 @@ if(${EMSCRIPTEN}) + endif() + + # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers +-set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") ++set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") + + set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${LEAN_BIN}) + diff --git a/math/lean4/files/patch-tests_lakefile.toml b/math/lean4/files/patch-tests_lakefile.toml new file mode 100644 index 000000000000..3a01b013943d --- /dev/null +++ b/math/lean4/files/patch-tests_lakefile.toml @@ -0,0 +1,10 @@ +--- tests/lakefile.toml.orig 2025-11-17 18:29:21 UTC ++++ tests/lakefile.toml +@@ -1,5 +1,7 @@ + name = "tests" + ++weakLeancArgs = ["-fPIC"] ++ + # Allow `module` in tests when opened in the language server. + # Enabled during actual test runs in the respective test_single.sh. + moreGlobalServerArgs = ["-Dexperimental.module=true"] diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 20f5d941e24a..b35afb3ef8ff 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -377,6 +377,21 @@ lib/lean/Init/Data/ByteArray/Basic.ir lib/lean/Init/Data/ByteArray/Basic.olean lib/lean/Init/Data/ByteArray/Basic.olean.private lib/lean/Init/Data/ByteArray/Basic.olean.server +lib/lean/Init/Data/ByteArray/Bootstrap.ilean +lib/lean/Init/Data/ByteArray/Bootstrap.ir +lib/lean/Init/Data/ByteArray/Bootstrap.olean +lib/lean/Init/Data/ByteArray/Bootstrap.olean.private +lib/lean/Init/Data/ByteArray/Bootstrap.olean.server +lib/lean/Init/Data/ByteArray/Extra.ilean +lib/lean/Init/Data/ByteArray/Extra.ir +lib/lean/Init/Data/ByteArray/Extra.olean +lib/lean/Init/Data/ByteArray/Extra.olean.private +lib/lean/Init/Data/ByteArray/Extra.olean.server +lib/lean/Init/Data/ByteArray/Lemmas.ilean +lib/lean/Init/Data/ByteArray/Lemmas.ir +lib/lean/Init/Data/ByteArray/Lemmas.olean +lib/lean/Init/Data/ByteArray/Lemmas.olean.private +lib/lean/Init/Data/ByteArray/Lemmas.olean.server lib/lean/Init/Data/Cast.ilean lib/lean/Init/Data/Cast.ir lib/lean/Init/Data/Cast.olean @@ -402,6 +417,31 @@ lib/lean/Init/Data/Char/Order.ir lib/lean/Init/Data/Char/Order.olean lib/lean/Init/Data/Char/Order.olean.private lib/lean/Init/Data/Char/Order.olean.server +lib/lean/Init/Data/Dyadic.ilean +lib/lean/Init/Data/Dyadic.ir +lib/lean/Init/Data/Dyadic.olean +lib/lean/Init/Data/Dyadic.olean.private +lib/lean/Init/Data/Dyadic.olean.server +lib/lean/Init/Data/Dyadic/Basic.ilean +lib/lean/Init/Data/Dyadic/Basic.ir +lib/lean/Init/Data/Dyadic/Basic.olean +lib/lean/Init/Data/Dyadic/Basic.olean.private +lib/lean/Init/Data/Dyadic/Basic.olean.server +lib/lean/Init/Data/Dyadic/Instances.ilean +lib/lean/Init/Data/Dyadic/Instances.ir +lib/lean/Init/Data/Dyadic/Instances.olean +lib/lean/Init/Data/Dyadic/Instances.olean.private +lib/lean/Init/Data/Dyadic/Instances.olean.server +lib/lean/Init/Data/Dyadic/Inv.ilean +lib/lean/Init/Data/Dyadic/Inv.ir +lib/lean/Init/Data/Dyadic/Inv.olean +lib/lean/Init/Data/Dyadic/Inv.olean.private +lib/lean/Init/Data/Dyadic/Inv.olean.server +lib/lean/Init/Data/Dyadic/Round.ilean +lib/lean/Init/Data/Dyadic/Round.ir +lib/lean/Init/Data/Dyadic/Round.olean +lib/lean/Init/Data/Dyadic/Round.olean.private +lib/lean/Init/Data/Dyadic/Round.olean.server lib/lean/Init/Data/Fin.ilean lib/lean/Init/Data/Fin.ir lib/lean/Init/Data/Fin.olean @@ -607,6 +647,11 @@ lib/lean/Init/Data/Iterators/Combinators/FilterMap.ir lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.private lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Combinators/FlatMap.ilean +lib/lean/Init/Data/Iterators/Combinators/FlatMap.ir +lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean +lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean.server lib/lean/Init/Data/Iterators/Combinators/Monadic.ilean lib/lean/Init/Data/Iterators/Combinators/Monadic.ir lib/lean/Init/Data/Iterators/Combinators/Monadic.olean @@ -622,6 +667,11 @@ lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.ir lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.private lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.ilean +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.ir +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean.server lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ilean lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ir lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean @@ -727,6 +777,11 @@ lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean.private lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.ilean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.ir +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.olean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Combinators/FlatMap.olean.server lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.ilean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.olean @@ -742,6 +797,11 @@ lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean.private lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.ilean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.ir +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean.server lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ilean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean @@ -797,6 +857,11 @@ lib/lean/Init/Data/Iterators/ToIterator.ir lib/lean/Init/Data/Iterators/ToIterator.olean lib/lean/Init/Data/Iterators/ToIterator.olean.private lib/lean/Init/Data/Iterators/ToIterator.olean.server +lib/lean/Init/Data/LawfulHashable.ilean +lib/lean/Init/Data/LawfulHashable.ir +lib/lean/Init/Data/LawfulHashable.olean +lib/lean/Init/Data/LawfulHashable.olean.private +lib/lean/Init/Data/LawfulHashable.olean.server lib/lean/Init/Data/List.ilean lib/lean/Init/Data/List.ir lib/lean/Init/Data/List.olean @@ -1042,6 +1107,11 @@ lib/lean/Init/Data/Nat/Control.ir lib/lean/Init/Data/Nat/Control.olean lib/lean/Init/Data/Nat/Control.olean.private lib/lean/Init/Data/Nat/Control.olean.server +lib/lean/Init/Data/Nat/Coprime.ilean +lib/lean/Init/Data/Nat/Coprime.ir +lib/lean/Init/Data/Nat/Coprime.olean +lib/lean/Init/Data/Nat/Coprime.olean.private +lib/lean/Init/Data/Nat/Coprime.olean.server lib/lean/Init/Data/Nat/Div.ilean lib/lean/Init/Data/Nat/Div.ir lib/lean/Init/Data/Nat/Div.olean @@ -1187,6 +1257,41 @@ lib/lean/Init/Data/Ord.ir lib/lean/Init/Data/Ord.olean lib/lean/Init/Data/Ord.olean.private lib/lean/Init/Data/Ord.olean.server +lib/lean/Init/Data/Ord/Array.ilean +lib/lean/Init/Data/Ord/Array.ir +lib/lean/Init/Data/Ord/Array.olean +lib/lean/Init/Data/Ord/Array.olean.private +lib/lean/Init/Data/Ord/Array.olean.server +lib/lean/Init/Data/Ord/Basic.ilean +lib/lean/Init/Data/Ord/Basic.ir +lib/lean/Init/Data/Ord/Basic.olean +lib/lean/Init/Data/Ord/Basic.olean.private +lib/lean/Init/Data/Ord/Basic.olean.server +lib/lean/Init/Data/Ord/BitVec.ilean +lib/lean/Init/Data/Ord/BitVec.ir +lib/lean/Init/Data/Ord/BitVec.olean +lib/lean/Init/Data/Ord/BitVec.olean.private +lib/lean/Init/Data/Ord/BitVec.olean.server +lib/lean/Init/Data/Ord/SInt.ilean +lib/lean/Init/Data/Ord/SInt.ir +lib/lean/Init/Data/Ord/SInt.olean +lib/lean/Init/Data/Ord/SInt.olean.private +lib/lean/Init/Data/Ord/SInt.olean.server +lib/lean/Init/Data/Ord/String.ilean +lib/lean/Init/Data/Ord/String.ir +lib/lean/Init/Data/Ord/String.olean +lib/lean/Init/Data/Ord/String.olean.private +lib/lean/Init/Data/Ord/String.olean.server +lib/lean/Init/Data/Ord/UInt.ilean +lib/lean/Init/Data/Ord/UInt.ir +lib/lean/Init/Data/Ord/UInt.olean +lib/lean/Init/Data/Ord/UInt.olean.private +lib/lean/Init/Data/Ord/UInt.olean.server +lib/lean/Init/Data/Ord/Vector.ilean +lib/lean/Init/Data/Ord/Vector.ir +lib/lean/Init/Data/Ord/Vector.olean +lib/lean/Init/Data/Ord/Vector.olean.private +lib/lean/Init/Data/Ord/Vector.olean.server lib/lean/Init/Data/Order.ilean lib/lean/Init/Data/Order.ir lib/lean/Init/Data/Order.olean @@ -1197,16 +1302,41 @@ lib/lean/Init/Data/Order/Classes.ir lib/lean/Init/Data/Order/Classes.olean lib/lean/Init/Data/Order/Classes.olean.private lib/lean/Init/Data/Order/Classes.olean.server +lib/lean/Init/Data/Order/ClassesExtra.ilean +lib/lean/Init/Data/Order/ClassesExtra.ir +lib/lean/Init/Data/Order/ClassesExtra.olean +lib/lean/Init/Data/Order/ClassesExtra.olean.private +lib/lean/Init/Data/Order/ClassesExtra.olean.server lib/lean/Init/Data/Order/Factories.ilean lib/lean/Init/Data/Order/Factories.ir lib/lean/Init/Data/Order/Factories.olean lib/lean/Init/Data/Order/Factories.olean.private lib/lean/Init/Data/Order/Factories.olean.server +lib/lean/Init/Data/Order/FactoriesExtra.ilean +lib/lean/Init/Data/Order/FactoriesExtra.ir +lib/lean/Init/Data/Order/FactoriesExtra.olean +lib/lean/Init/Data/Order/FactoriesExtra.olean.private +lib/lean/Init/Data/Order/FactoriesExtra.olean.server lib/lean/Init/Data/Order/Lemmas.ilean lib/lean/Init/Data/Order/Lemmas.ir lib/lean/Init/Data/Order/Lemmas.olean lib/lean/Init/Data/Order/Lemmas.olean.private lib/lean/Init/Data/Order/Lemmas.olean.server +lib/lean/Init/Data/Order/LemmasExtra.ilean +lib/lean/Init/Data/Order/LemmasExtra.ir +lib/lean/Init/Data/Order/LemmasExtra.olean +lib/lean/Init/Data/Order/LemmasExtra.olean.private +lib/lean/Init/Data/Order/LemmasExtra.olean.server +lib/lean/Init/Data/Order/Ord.ilean +lib/lean/Init/Data/Order/Ord.ir +lib/lean/Init/Data/Order/Ord.olean +lib/lean/Init/Data/Order/Ord.olean.private +lib/lean/Init/Data/Order/Ord.olean.server +lib/lean/Init/Data/Order/PackageFactories.ilean +lib/lean/Init/Data/Order/PackageFactories.ir +lib/lean/Init/Data/Order/PackageFactories.olean +lib/lean/Init/Data/Order/PackageFactories.olean.private +lib/lean/Init/Data/Order/PackageFactories.olean.server lib/lean/Init/Data/PLift.ilean lib/lean/Init/Data/PLift.ir lib/lean/Init/Data/PLift.olean @@ -1257,6 +1387,31 @@ lib/lean/Init/Data/Range/Polymorphic/Basic.ir lib/lean/Init/Data/Range/Polymorphic/Basic.olean lib/lean/Init/Data/Range/Polymorphic/Basic.olean.private lib/lean/Init/Data/Range/Polymorphic/Basic.olean.server +lib/lean/Init/Data/Range/Polymorphic/BitVec.ilean +lib/lean/Init/Data/Range/Polymorphic/BitVec.ir +lib/lean/Init/Data/Range/Polymorphic/BitVec.olean +lib/lean/Init/Data/Range/Polymorphic/BitVec.olean.private +lib/lean/Init/Data/Range/Polymorphic/BitVec.olean.server +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.ilean +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.ir +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.olean +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.olean.private +lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.olean.server +lib/lean/Init/Data/Range/Polymorphic/Instances.ilean +lib/lean/Init/Data/Range/Polymorphic/Instances.ir +lib/lean/Init/Data/Range/Polymorphic/Instances.olean +lib/lean/Init/Data/Range/Polymorphic/Instances.olean.private +lib/lean/Init/Data/Range/Polymorphic/Instances.olean.server +lib/lean/Init/Data/Range/Polymorphic/Int.ilean +lib/lean/Init/Data/Range/Polymorphic/Int.ir +lib/lean/Init/Data/Range/Polymorphic/Int.olean +lib/lean/Init/Data/Range/Polymorphic/Int.olean.private +lib/lean/Init/Data/Range/Polymorphic/Int.olean.server +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.ilean +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.ir +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.olean +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.olean.private +lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.olean.server lib/lean/Init/Data/Range/Polymorphic/Iterators.ilean lib/lean/Init/Data/Range/Polymorphic/Iterators.ir lib/lean/Init/Data/Range/Polymorphic/Iterators.olean @@ -1287,16 +1442,41 @@ lib/lean/Init/Data/Range/Polymorphic/RangeIterator.ir lib/lean/Init/Data/Range/Polymorphic/RangeIterator.olean lib/lean/Init/Data/Range/Polymorphic/RangeIterator.olean.private lib/lean/Init/Data/Range/Polymorphic/RangeIterator.olean.server +lib/lean/Init/Data/Range/Polymorphic/SInt.ilean +lib/lean/Init/Data/Range/Polymorphic/SInt.ir +lib/lean/Init/Data/Range/Polymorphic/SInt.olean +lib/lean/Init/Data/Range/Polymorphic/SInt.olean.private +lib/lean/Init/Data/Range/Polymorphic/SInt.olean.server lib/lean/Init/Data/Range/Polymorphic/Stream.ilean lib/lean/Init/Data/Range/Polymorphic/Stream.ir lib/lean/Init/Data/Range/Polymorphic/Stream.olean lib/lean/Init/Data/Range/Polymorphic/Stream.olean.private lib/lean/Init/Data/Range/Polymorphic/Stream.olean.server +lib/lean/Init/Data/Range/Polymorphic/UInt.ilean +lib/lean/Init/Data/Range/Polymorphic/UInt.ir +lib/lean/Init/Data/Range/Polymorphic/UInt.olean +lib/lean/Init/Data/Range/Polymorphic/UInt.olean.private +lib/lean/Init/Data/Range/Polymorphic/UInt.olean.server lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.ilean lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.ir lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.olean lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.olean.private lib/lean/Init/Data/Range/Polymorphic/UpwardEnumerable.olean.server +lib/lean/Init/Data/Rat.ilean +lib/lean/Init/Data/Rat.ir +lib/lean/Init/Data/Rat.olean +lib/lean/Init/Data/Rat.olean.private +lib/lean/Init/Data/Rat.olean.server +lib/lean/Init/Data/Rat/Basic.ilean +lib/lean/Init/Data/Rat/Basic.ir +lib/lean/Init/Data/Rat/Basic.olean +lib/lean/Init/Data/Rat/Basic.olean.private +lib/lean/Init/Data/Rat/Basic.olean.server +lib/lean/Init/Data/Rat/Lemmas.ilean +lib/lean/Init/Data/Rat/Lemmas.ir +lib/lean/Init/Data/Rat/Lemmas.olean +lib/lean/Init/Data/Rat/Lemmas.olean.private +lib/lean/Init/Data/Rat/Lemmas.olean.server lib/lean/Init/Data/Repr.ilean lib/lean/Init/Data/Repr.ir lib/lean/Init/Data/Repr.olean @@ -1392,6 +1572,16 @@ lib/lean/Init/Data/String/Basic.ir lib/lean/Init/Data/String/Basic.olean lib/lean/Init/Data/String/Basic.olean.private lib/lean/Init/Data/String/Basic.olean.server +lib/lean/Init/Data/String/Bootstrap.ilean +lib/lean/Init/Data/String/Bootstrap.ir +lib/lean/Init/Data/String/Bootstrap.olean +lib/lean/Init/Data/String/Bootstrap.olean.private +lib/lean/Init/Data/String/Bootstrap.olean.server +lib/lean/Init/Data/String/Decode.ilean +lib/lean/Init/Data/String/Decode.ir +lib/lean/Init/Data/String/Decode.olean +lib/lean/Init/Data/String/Decode.olean.private +lib/lean/Init/Data/String/Decode.olean.server lib/lean/Init/Data/String/Extra.ilean lib/lean/Init/Data/String/Extra.ir lib/lean/Init/Data/String/Extra.olean @@ -1402,6 +1592,46 @@ lib/lean/Init/Data/String/Lemmas.ir lib/lean/Init/Data/String/Lemmas.olean lib/lean/Init/Data/String/Lemmas.olean.private lib/lean/Init/Data/String/Lemmas.olean.server +lib/lean/Init/Data/String/Pattern.ilean +lib/lean/Init/Data/String/Pattern.ir +lib/lean/Init/Data/String/Pattern.olean +lib/lean/Init/Data/String/Pattern.olean.private +lib/lean/Init/Data/String/Pattern.olean.server +lib/lean/Init/Data/String/Pattern/Basic.ilean +lib/lean/Init/Data/String/Pattern/Basic.ir +lib/lean/Init/Data/String/Pattern/Basic.olean +lib/lean/Init/Data/String/Pattern/Basic.olean.private +lib/lean/Init/Data/String/Pattern/Basic.olean.server +lib/lean/Init/Data/String/Pattern/Char.ilean +lib/lean/Init/Data/String/Pattern/Char.ir +lib/lean/Init/Data/String/Pattern/Char.olean +lib/lean/Init/Data/String/Pattern/Char.olean.private +lib/lean/Init/Data/String/Pattern/Char.olean.server +lib/lean/Init/Data/String/Pattern/Pred.ilean +lib/lean/Init/Data/String/Pattern/Pred.ir +lib/lean/Init/Data/String/Pattern/Pred.olean +lib/lean/Init/Data/String/Pattern/Pred.olean.private +lib/lean/Init/Data/String/Pattern/Pred.olean.server +lib/lean/Init/Data/String/Pattern/String.ilean +lib/lean/Init/Data/String/Pattern/String.ir +lib/lean/Init/Data/String/Pattern/String.olean +lib/lean/Init/Data/String/Pattern/String.olean.private +lib/lean/Init/Data/String/Pattern/String.olean.server +lib/lean/Init/Data/String/Repr.ilean +lib/lean/Init/Data/String/Repr.ir +lib/lean/Init/Data/String/Repr.olean +lib/lean/Init/Data/String/Repr.olean.private +lib/lean/Init/Data/String/Repr.olean.server +lib/lean/Init/Data/String/Slice.ilean +lib/lean/Init/Data/String/Slice.ir +lib/lean/Init/Data/String/Slice.olean +lib/lean/Init/Data/String/Slice.olean.private +lib/lean/Init/Data/String/Slice.olean.server +lib/lean/Init/Data/String/Stream.ilean +lib/lean/Init/Data/String/Stream.ir +lib/lean/Init/Data/String/Stream.olean +lib/lean/Init/Data/String/Stream.olean.private +lib/lean/Init/Data/String/Stream.olean.server lib/lean/Init/Data/Subtype.ilean lib/lean/Init/Data/Subtype.ir lib/lean/Init/Data/Subtype.olean @@ -1452,6 +1682,11 @@ lib/lean/Init/Data/ToString/Macro.ir lib/lean/Init/Data/ToString/Macro.olean lib/lean/Init/Data/ToString/Macro.olean.private lib/lean/Init/Data/ToString/Macro.olean.server +lib/lean/Init/Data/ToString/Name.ilean +lib/lean/Init/Data/ToString/Name.ir +lib/lean/Init/Data/ToString/Name.olean +lib/lean/Init/Data/ToString/Name.olean.private +lib/lean/Init/Data/ToString/Name.olean.server lib/lean/Init/Data/UInt.ilean lib/lean/Init/Data/UInt.ir lib/lean/Init/Data/UInt.olean @@ -1577,6 +1812,11 @@ lib/lean/Init/Data/Vector/Range.ir lib/lean/Init/Data/Vector/Range.olean lib/lean/Init/Data/Vector/Range.olean.private lib/lean/Init/Data/Vector/Range.olean.server +lib/lean/Init/Data/Vector/Stream.ilean +lib/lean/Init/Data/Vector/Stream.ir +lib/lean/Init/Data/Vector/Stream.olean +lib/lean/Init/Data/Vector/Stream.olean.private +lib/lean/Init/Data/Vector/Stream.olean.server lib/lean/Init/Data/Vector/Zip.ilean lib/lean/Init/Data/Vector/Zip.ir lib/lean/Init/Data/Vector/Zip.olean @@ -1607,6 +1847,11 @@ lib/lean/Init/Grind.ir lib/lean/Init/Grind.olean lib/lean/Init/Grind.olean.private lib/lean/Init/Grind.olean.server +lib/lean/Init/Grind/AC.ilean +lib/lean/Init/Grind/AC.ir +lib/lean/Init/Grind/AC.olean +lib/lean/Init/Grind/AC.olean.private +lib/lean/Init/Grind/AC.olean.server lib/lean/Init/Grind/Attr.ilean lib/lean/Init/Grind/Attr.ir lib/lean/Init/Grind/Attr.olean @@ -1622,6 +1867,16 @@ lib/lean/Init/Grind/Ext.ir lib/lean/Init/Grind/Ext.olean lib/lean/Init/Grind/Ext.olean.private lib/lean/Init/Grind/Ext.olean.server +lib/lean/Init/Grind/Injective.ilean +lib/lean/Init/Grind/Injective.ir +lib/lean/Init/Grind/Injective.olean +lib/lean/Init/Grind/Injective.olean.private +lib/lean/Init/Grind/Injective.olean.server +lib/lean/Init/Grind/Interactive.ilean +lib/lean/Init/Grind/Interactive.ir +lib/lean/Init/Grind/Interactive.olean +lib/lean/Init/Grind/Interactive.olean.private +lib/lean/Init/Grind/Interactive.olean.server lib/lean/Init/Grind/Lemmas.ilean lib/lean/Init/Grind/Lemmas.ir lib/lean/Init/Grind/Lemmas.olean @@ -1642,6 +1897,16 @@ lib/lean/Init/Grind/Module/Envelope.ir lib/lean/Init/Grind/Module/Envelope.olean lib/lean/Init/Grind/Module/Envelope.olean.private lib/lean/Init/Grind/Module/Envelope.olean.server +lib/lean/Init/Grind/Module/NatModuleNorm.ilean +lib/lean/Init/Grind/Module/NatModuleNorm.ir +lib/lean/Init/Grind/Module/NatModuleNorm.olean +lib/lean/Init/Grind/Module/NatModuleNorm.olean.private +lib/lean/Init/Grind/Module/NatModuleNorm.olean.server +lib/lean/Init/Grind/Module/OfNatModule.ilean +lib/lean/Init/Grind/Module/OfNatModule.ir +lib/lean/Init/Grind/Module/OfNatModule.olean +lib/lean/Init/Grind/Module/OfNatModule.olean.private +lib/lean/Init/Grind/Module/OfNatModule.olean.server lib/lean/Init/Grind/Norm.ilean lib/lean/Init/Grind/Norm.ir lib/lean/Init/Grind/Norm.olean @@ -1652,6 +1917,11 @@ lib/lean/Init/Grind/Offset.ir lib/lean/Init/Grind/Offset.olean lib/lean/Init/Grind/Offset.olean.private lib/lean/Init/Grind/Offset.olean.server +lib/lean/Init/Grind/Order.ilean +lib/lean/Init/Grind/Order.ir +lib/lean/Init/Grind/Order.olean +lib/lean/Init/Grind/Order.olean.private +lib/lean/Init/Grind/Order.olean.server lib/lean/Init/Grind/Ordered.ilean lib/lean/Init/Grind/Ordered.ir lib/lean/Init/Grind/Ordered.olean @@ -1682,6 +1952,11 @@ lib/lean/Init/Grind/Ordered/Order.ir lib/lean/Init/Grind/Ordered/Order.olean lib/lean/Init/Grind/Ordered/Order.olean.private lib/lean/Init/Grind/Ordered/Order.olean.server +lib/lean/Init/Grind/Ordered/Rat.ilean +lib/lean/Init/Grind/Ordered/Rat.ir +lib/lean/Init/Grind/Ordered/Rat.olean +lib/lean/Init/Grind/Ordered/Rat.olean.private +lib/lean/Init/Grind/Ordered/Rat.olean.server lib/lean/Init/Grind/Ordered/Ring.ilean lib/lean/Init/Grind/Ordered/Ring.ir lib/lean/Init/Grind/Ordered/Ring.olean @@ -1707,6 +1982,16 @@ lib/lean/Init/Grind/Ring/Basic.ir lib/lean/Init/Grind/Ring/Basic.olean lib/lean/Init/Grind/Ring/Basic.olean.private lib/lean/Init/Grind/Ring/Basic.olean.server +lib/lean/Init/Grind/Ring/CommSemiringAdapter.ilean +lib/lean/Init/Grind/Ring/CommSemiringAdapter.ir +lib/lean/Init/Grind/Ring/CommSemiringAdapter.olean +lib/lean/Init/Grind/Ring/CommSemiringAdapter.olean.private +lib/lean/Init/Grind/Ring/CommSemiringAdapter.olean.server +lib/lean/Init/Grind/Ring/CommSolver.ilean +lib/lean/Init/Grind/Ring/CommSolver.ir +lib/lean/Init/Grind/Ring/CommSolver.olean +lib/lean/Init/Grind/Ring/CommSolver.olean.private +lib/lean/Init/Grind/Ring/CommSolver.olean.server lib/lean/Init/Grind/Ring/Envelope.ilean lib/lean/Init/Grind/Ring/Envelope.ir lib/lean/Init/Grind/Ring/Envelope.olean @@ -1717,16 +2002,6 @@ lib/lean/Init/Grind/Ring/Field.ir lib/lean/Init/Grind/Ring/Field.olean lib/lean/Init/Grind/Ring/Field.olean.private lib/lean/Init/Grind/Ring/Field.olean.server -lib/lean/Init/Grind/Ring/OfSemiring.ilean -lib/lean/Init/Grind/Ring/OfSemiring.ir -lib/lean/Init/Grind/Ring/OfSemiring.olean -lib/lean/Init/Grind/Ring/OfSemiring.olean.private -lib/lean/Init/Grind/Ring/OfSemiring.olean.server -lib/lean/Init/Grind/Ring/Poly.ilean -lib/lean/Init/Grind/Ring/Poly.ir -lib/lean/Init/Grind/Ring/Poly.olean -lib/lean/Init/Grind/Ring/Poly.olean.private -lib/lean/Init/Grind/Ring/Poly.olean.server lib/lean/Init/Grind/Ring/ToInt.ilean lib/lean/Init/Grind/Ring/ToInt.ir lib/lean/Init/Grind/Ring/ToInt.olean @@ -1787,6 +2062,11 @@ lib/lean/Init/GrindInstances/Ring/Nat.ir lib/lean/Init/GrindInstances/Ring/Nat.olean lib/lean/Init/GrindInstances/Ring/Nat.olean.private lib/lean/Init/GrindInstances/Ring/Nat.olean.server +lib/lean/Init/GrindInstances/Ring/Rat.ilean +lib/lean/Init/GrindInstances/Ring/Rat.ir +lib/lean/Init/GrindInstances/Ring/Rat.olean +lib/lean/Init/GrindInstances/Ring/Rat.olean.private +lib/lean/Init/GrindInstances/Ring/Rat.olean.server lib/lean/Init/GrindInstances/Ring/SInt.ilean lib/lean/Init/GrindInstances/Ring/SInt.ir lib/lean/Init/GrindInstances/Ring/SInt.olean @@ -1837,6 +2117,11 @@ lib/lean/Init/Internal/Order/Tactic.ir lib/lean/Init/Internal/Order/Tactic.olean lib/lean/Init/Internal/Order/Tactic.olean.private lib/lean/Init/Internal/Order/Tactic.olean.server +lib/lean/Init/LawfulBEqTactics.ilean +lib/lean/Init/LawfulBEqTactics.ir +lib/lean/Init/LawfulBEqTactics.olean +lib/lean/Init/LawfulBEqTactics.olean.private +lib/lean/Init/LawfulBEqTactics.olean.server lib/lean/Init/MacroTrace.ilean lib/lean/Init/MacroTrace.ir lib/lean/Init/MacroTrace.olean @@ -1847,11 +2132,21 @@ lib/lean/Init/Meta.ir lib/lean/Init/Meta.olean lib/lean/Init/Meta.olean.private lib/lean/Init/Meta.olean.server +lib/lean/Init/Meta/Defs.ilean +lib/lean/Init/Meta/Defs.ir +lib/lean/Init/Meta/Defs.olean +lib/lean/Init/Meta/Defs.olean.private +lib/lean/Init/Meta/Defs.olean.server lib/lean/Init/MetaTypes.ilean lib/lean/Init/MetaTypes.ir lib/lean/Init/MetaTypes.olean lib/lean/Init/MetaTypes.olean.private lib/lean/Init/MetaTypes.olean.server +lib/lean/Init/MethodSpecsSimp.ilean +lib/lean/Init/MethodSpecsSimp.ir +lib/lean/Init/MethodSpecsSimp.olean +lib/lean/Init/MethodSpecsSimp.olean.private +lib/lean/Init/MethodSpecsSimp.olean.server lib/lean/Init/Notation.ilean lib/lean/Init/Notation.ir lib/lean/Init/Notation.olean @@ -2023,307 +2318,785 @@ lib/lean/Init/While.olean lib/lean/Init/While.olean.private lib/lean/Init/While.olean.server lib/lean/Lake.ilean +lib/lean/Lake.ir lib/lean/Lake.olean +lib/lean/Lake.olean.private +lib/lean/Lake.olean.server lib/lean/Lake/Build.ilean +lib/lean/Lake/Build.ir lib/lean/Lake/Build.olean +lib/lean/Lake/Build.olean.private +lib/lean/Lake/Build.olean.server lib/lean/Lake/Build/Actions.ilean +lib/lean/Lake/Build/Actions.ir lib/lean/Lake/Build/Actions.olean +lib/lean/Lake/Build/Actions.olean.private +lib/lean/Lake/Build/Actions.olean.server lib/lean/Lake/Build/Common.ilean +lib/lean/Lake/Build/Common.ir lib/lean/Lake/Build/Common.olean +lib/lean/Lake/Build/Common.olean.private +lib/lean/Lake/Build/Common.olean.server lib/lean/Lake/Build/Context.ilean +lib/lean/Lake/Build/Context.ir lib/lean/Lake/Build/Context.olean +lib/lean/Lake/Build/Context.olean.private +lib/lean/Lake/Build/Context.olean.server lib/lean/Lake/Build/Data.ilean +lib/lean/Lake/Build/Data.ir lib/lean/Lake/Build/Data.olean +lib/lean/Lake/Build/Data.olean.private +lib/lean/Lake/Build/Data.olean.server lib/lean/Lake/Build/Executable.ilean +lib/lean/Lake/Build/Executable.ir lib/lean/Lake/Build/Executable.olean +lib/lean/Lake/Build/Executable.olean.private +lib/lean/Lake/Build/Executable.olean.server lib/lean/Lake/Build/ExternLib.ilean +lib/lean/Lake/Build/ExternLib.ir lib/lean/Lake/Build/ExternLib.olean +lib/lean/Lake/Build/ExternLib.olean.private +lib/lean/Lake/Build/ExternLib.olean.server lib/lean/Lake/Build/Facets.ilean +lib/lean/Lake/Build/Facets.ir lib/lean/Lake/Build/Facets.olean +lib/lean/Lake/Build/Facets.olean.private +lib/lean/Lake/Build/Facets.olean.server lib/lean/Lake/Build/Fetch.ilean +lib/lean/Lake/Build/Fetch.ir lib/lean/Lake/Build/Fetch.olean +lib/lean/Lake/Build/Fetch.olean.private +lib/lean/Lake/Build/Fetch.olean.server lib/lean/Lake/Build/Index.ilean +lib/lean/Lake/Build/Index.ir lib/lean/Lake/Build/Index.olean +lib/lean/Lake/Build/Index.olean.private +lib/lean/Lake/Build/Index.olean.server lib/lean/Lake/Build/Info.ilean +lib/lean/Lake/Build/Info.ir lib/lean/Lake/Build/Info.olean +lib/lean/Lake/Build/Info.olean.private +lib/lean/Lake/Build/Info.olean.server +lib/lean/Lake/Build/Infos.ilean +lib/lean/Lake/Build/Infos.ir +lib/lean/Lake/Build/Infos.olean +lib/lean/Lake/Build/Infos.olean.private +lib/lean/Lake/Build/Infos.olean.server lib/lean/Lake/Build/InitFacets.ilean +lib/lean/Lake/Build/InitFacets.ir lib/lean/Lake/Build/InitFacets.olean +lib/lean/Lake/Build/InitFacets.olean.private +lib/lean/Lake/Build/InitFacets.olean.server lib/lean/Lake/Build/InputFile.ilean +lib/lean/Lake/Build/InputFile.ir lib/lean/Lake/Build/InputFile.olean +lib/lean/Lake/Build/InputFile.olean.private +lib/lean/Lake/Build/InputFile.olean.server lib/lean/Lake/Build/Job.ilean +lib/lean/Lake/Build/Job.ir lib/lean/Lake/Build/Job.olean +lib/lean/Lake/Build/Job.olean.private +lib/lean/Lake/Build/Job.olean.server lib/lean/Lake/Build/Job/Basic.ilean +lib/lean/Lake/Build/Job/Basic.ir lib/lean/Lake/Build/Job/Basic.olean +lib/lean/Lake/Build/Job/Basic.olean.private +lib/lean/Lake/Build/Job/Basic.olean.server lib/lean/Lake/Build/Job/Monad.ilean +lib/lean/Lake/Build/Job/Monad.ir lib/lean/Lake/Build/Job/Monad.olean +lib/lean/Lake/Build/Job/Monad.olean.private +lib/lean/Lake/Build/Job/Monad.olean.server lib/lean/Lake/Build/Job/Register.ilean +lib/lean/Lake/Build/Job/Register.ir lib/lean/Lake/Build/Job/Register.olean +lib/lean/Lake/Build/Job/Register.olean.private +lib/lean/Lake/Build/Job/Register.olean.server lib/lean/Lake/Build/Key.ilean +lib/lean/Lake/Build/Key.ir lib/lean/Lake/Build/Key.olean +lib/lean/Lake/Build/Key.olean.private +lib/lean/Lake/Build/Key.olean.server lib/lean/Lake/Build/Library.ilean +lib/lean/Lake/Build/Library.ir lib/lean/Lake/Build/Library.olean +lib/lean/Lake/Build/Library.olean.private +lib/lean/Lake/Build/Library.olean.server lib/lean/Lake/Build/Module.ilean +lib/lean/Lake/Build/Module.ir lib/lean/Lake/Build/Module.olean +lib/lean/Lake/Build/Module.olean.private +lib/lean/Lake/Build/Module.olean.server lib/lean/Lake/Build/ModuleArtifacts.ilean +lib/lean/Lake/Build/ModuleArtifacts.ir lib/lean/Lake/Build/ModuleArtifacts.olean +lib/lean/Lake/Build/ModuleArtifacts.olean.private +lib/lean/Lake/Build/ModuleArtifacts.olean.server lib/lean/Lake/Build/Package.ilean +lib/lean/Lake/Build/Package.ir lib/lean/Lake/Build/Package.olean +lib/lean/Lake/Build/Package.olean.private +lib/lean/Lake/Build/Package.olean.server lib/lean/Lake/Build/Run.ilean +lib/lean/Lake/Build/Run.ir lib/lean/Lake/Build/Run.olean +lib/lean/Lake/Build/Run.olean.private +lib/lean/Lake/Build/Run.olean.server lib/lean/Lake/Build/Store.ilean +lib/lean/Lake/Build/Store.ir lib/lean/Lake/Build/Store.olean +lib/lean/Lake/Build/Store.olean.private +lib/lean/Lake/Build/Store.olean.server lib/lean/Lake/Build/Target.ilean +lib/lean/Lake/Build/Target.ir lib/lean/Lake/Build/Target.olean +lib/lean/Lake/Build/Target.olean.private +lib/lean/Lake/Build/Target.olean.server lib/lean/Lake/Build/Target/Basic.ilean +lib/lean/Lake/Build/Target/Basic.ir lib/lean/Lake/Build/Target/Basic.olean +lib/lean/Lake/Build/Target/Basic.olean.private +lib/lean/Lake/Build/Target/Basic.olean.server lib/lean/Lake/Build/Target/Fetch.ilean +lib/lean/Lake/Build/Target/Fetch.ir lib/lean/Lake/Build/Target/Fetch.olean +lib/lean/Lake/Build/Target/Fetch.olean.private +lib/lean/Lake/Build/Target/Fetch.olean.server lib/lean/Lake/Build/Targets.ilean +lib/lean/Lake/Build/Targets.ir lib/lean/Lake/Build/Targets.olean +lib/lean/Lake/Build/Targets.olean.private +lib/lean/Lake/Build/Targets.olean.server lib/lean/Lake/Build/Topological.ilean +lib/lean/Lake/Build/Topological.ir lib/lean/Lake/Build/Topological.olean +lib/lean/Lake/Build/Topological.olean.private +lib/lean/Lake/Build/Topological.olean.server lib/lean/Lake/Build/Trace.ilean +lib/lean/Lake/Build/Trace.ir lib/lean/Lake/Build/Trace.olean +lib/lean/Lake/Build/Trace.olean.private +lib/lean/Lake/Build/Trace.olean.server lib/lean/Lake/CLI.ilean +lib/lean/Lake/CLI.ir lib/lean/Lake/CLI.olean +lib/lean/Lake/CLI.olean.private +lib/lean/Lake/CLI.olean.server lib/lean/Lake/CLI/Actions.ilean +lib/lean/Lake/CLI/Actions.ir lib/lean/Lake/CLI/Actions.olean +lib/lean/Lake/CLI/Actions.olean.private +lib/lean/Lake/CLI/Actions.olean.server lib/lean/Lake/CLI/Build.ilean +lib/lean/Lake/CLI/Build.ir lib/lean/Lake/CLI/Build.olean +lib/lean/Lake/CLI/Build.olean.private +lib/lean/Lake/CLI/Build.olean.server lib/lean/Lake/CLI/Error.ilean +lib/lean/Lake/CLI/Error.ir lib/lean/Lake/CLI/Error.olean +lib/lean/Lake/CLI/Error.olean.private +lib/lean/Lake/CLI/Error.olean.server lib/lean/Lake/CLI/Help.ilean +lib/lean/Lake/CLI/Help.ir lib/lean/Lake/CLI/Help.olean +lib/lean/Lake/CLI/Help.olean.private +lib/lean/Lake/CLI/Help.olean.server lib/lean/Lake/CLI/Init.ilean +lib/lean/Lake/CLI/Init.ir lib/lean/Lake/CLI/Init.olean +lib/lean/Lake/CLI/Init.olean.private +lib/lean/Lake/CLI/Init.olean.server lib/lean/Lake/CLI/Main.ilean +lib/lean/Lake/CLI/Main.ir lib/lean/Lake/CLI/Main.olean +lib/lean/Lake/CLI/Main.olean.private +lib/lean/Lake/CLI/Main.olean.server lib/lean/Lake/CLI/Serve.ilean +lib/lean/Lake/CLI/Serve.ir lib/lean/Lake/CLI/Serve.olean +lib/lean/Lake/CLI/Serve.olean.private +lib/lean/Lake/CLI/Serve.olean.server lib/lean/Lake/CLI/Translate.ilean +lib/lean/Lake/CLI/Translate.ir lib/lean/Lake/CLI/Translate.olean +lib/lean/Lake/CLI/Translate.olean.private +lib/lean/Lake/CLI/Translate.olean.server lib/lean/Lake/CLI/Translate/Lean.ilean +lib/lean/Lake/CLI/Translate/Lean.ir lib/lean/Lake/CLI/Translate/Lean.olean +lib/lean/Lake/CLI/Translate/Lean.olean.private +lib/lean/Lake/CLI/Translate/Lean.olean.server lib/lean/Lake/CLI/Translate/Toml.ilean +lib/lean/Lake/CLI/Translate/Toml.ir lib/lean/Lake/CLI/Translate/Toml.olean +lib/lean/Lake/CLI/Translate/Toml.olean.private +lib/lean/Lake/CLI/Translate/Toml.olean.server lib/lean/Lake/Config.ilean +lib/lean/Lake/Config.ir lib/lean/Lake/Config.olean +lib/lean/Lake/Config.olean.private +lib/lean/Lake/Config.olean.server lib/lean/Lake/Config/Artifact.ilean +lib/lean/Lake/Config/Artifact.ir lib/lean/Lake/Config/Artifact.olean +lib/lean/Lake/Config/Artifact.olean.private +lib/lean/Lake/Config/Artifact.olean.server lib/lean/Lake/Config/Cache.ilean +lib/lean/Lake/Config/Cache.ir lib/lean/Lake/Config/Cache.olean +lib/lean/Lake/Config/Cache.olean.private +lib/lean/Lake/Config/Cache.olean.server lib/lean/Lake/Config/ConfigDecl.ilean +lib/lean/Lake/Config/ConfigDecl.ir lib/lean/Lake/Config/ConfigDecl.olean +lib/lean/Lake/Config/ConfigDecl.olean.private +lib/lean/Lake/Config/ConfigDecl.olean.server lib/lean/Lake/Config/ConfigTarget.ilean +lib/lean/Lake/Config/ConfigTarget.ir *** 2541 LINES SKIPPED ***
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?6924a375.c5a8.550faf91>