git: 4d5291902c3a - main - math/lean4: update 4.25.2 → 4.25.2.20251201

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Tue, 02 Dec 2025 00:47:10 UTC
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=4d5291902c3a66649a78ec44d373a6f811b9aa6b

commit 4d5291902c3a66649a78ec44d373a6f811b9aa6b
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2025-12-02 00:45:20 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2025-12-02 00:47:08 +0000

    math/lean4: update 4.25.2 → 4.25.2.20251201
    
    The previous release's tarball changed unexplainably, and the
    new one is unbuildable, again unexplainably.
    
    This update brings it to the latest revision to solve this problem.
    
    Reported by:    fallout
---
 math/lean4/Makefile                                |   5 +-
 math/lean4/distinfo                                |   6 +-
 math/lean4/files/patch-src_shell_CMakeLists.txt    |  11 -
 .../files/patch-stage0_src_shell_CMakeLists.txt    |  11 -
 math/lean4/pkg-plist                               | 678 +++++++++++++++++----
 5 files changed, 564 insertions(+), 147 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 30652dafea6b..8b5c81aa12bc 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.25.2
+DISTVERSION=	4.25.2-20251201
 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
@@ -25,6 +25,7 @@ USES=		cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build #
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	leanprover
+GH_TAGNAME=	5e165e3
 
 CFLAGS+=	-fPIC
 CXXFLAGS+=	-fPIC
@@ -77,6 +78,6 @@ post-install:
 		lib/lean/libleanshared_1.so \
 		lib/lean/libLake_shared.so
 
-# tests as of 4.25.2: 100% tests passed, 0 tests failed out of 3241
+# tests as of 4.25.2-20251201: 100% tests passed, 0 tests failed out of 3367
 
 .include <bsd.port.mk>
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index ca359438cd41..20923ac21be3 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1764048066
-SHA256 (leanprover-lean4-v4.25.2_GH0.tar.gz) = 831b1d1d3833791e68de087d8f576c4703a5dd82157dd19364629f5df7fcfb2c
-SIZE (leanprover-lean4-v4.25.2_GH0.tar.gz) = 50069767
+TIMESTAMP = 1764606890
+SHA256 (leanprover-lean4-v4.25.2-20251201-5e165e3_GH0.tar.gz) = 70c7265936d4d5393c9778a19d39620b4ce51c75cda1a0d3fbdef685996c5d3d
+SIZE (leanprover-lean4-v4.25.2-20251201-5e165e3_GH0.tar.gz) = 48235866
diff --git a/math/lean4/files/patch-src_shell_CMakeLists.txt b/math/lean4/files/patch-src_shell_CMakeLists.txt
deleted file mode 100644
index 68de472208ff..000000000000
--- a/math/lean4/files/patch-src_shell_CMakeLists.txt
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/shell/CMakeLists.txt.orig	2025-11-18 02:29:21 UTC
-+++ src/shell/CMakeLists.txt
-@@ -57,7 +57,7 @@ endif()
- 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}'")
- 
- # LEAN TESTS
- file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt
deleted file mode 100644
index bd9010ce3d9b..000000000000
--- a/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt
+++ /dev/null
@@ -1,11 +0,0 @@
---- stage0/src/shell/CMakeLists.txt.orig	2025-11-18 02:29:21 UTC
-+++ stage0/src/shell/CMakeLists.txt
-@@ -57,7 +57,7 @@ endif()
- 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}'")
- 
- # LEAN TESTS
- file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index b35afb3ef8ff..ae09be366a40 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -317,11 +317,6 @@ lib/lean/Init/Data/BEq.ir
 lib/lean/Init/Data/BEq.olean
 lib/lean/Init/Data/BEq.olean.private
 lib/lean/Init/Data/BEq.olean.server
-lib/lean/Init/Data/Basic.ilean
-lib/lean/Init/Data/Basic.ir
-lib/lean/Init/Data/Basic.olean
-lib/lean/Init/Data/Basic.olean.private
-lib/lean/Init/Data/Basic.olean.server
 lib/lean/Init/Data/BitVec.ilean
 lib/lean/Init/Data/BitVec.ir
 lib/lean/Init/Data/BitVec.olean
@@ -587,6 +582,11 @@ lib/lean/Init/Data/Int/DivMod/Lemmas.ir
 lib/lean/Init/Data/Int/DivMod/Lemmas.olean
 lib/lean/Init/Data/Int/DivMod/Lemmas.olean.private
 lib/lean/Init/Data/Int/DivMod/Lemmas.olean.server
+lib/lean/Init/Data/Int/DivMod/Pow.ilean
+lib/lean/Init/Data/Int/DivMod/Pow.ir
+lib/lean/Init/Data/Int/DivMod/Pow.olean
+lib/lean/Init/Data/Int/DivMod/Pow.olean.private
+lib/lean/Init/Data/Int/DivMod/Pow.olean.server
 lib/lean/Init/Data/Int/Gcd.ilean
 lib/lean/Init/Data/Int/Gcd.ir
 lib/lean/Init/Data/Int/Gcd.olean
@@ -672,11 +672,21 @@ 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/Take.ilean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.ir
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.olean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.olean.private
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.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
 lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean.private
 lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean.server
+lib/lean/Init/Data/Iterators/Combinators/Take.ilean
+lib/lean/Init/Data/Iterators/Combinators/Take.ir
+lib/lean/Init/Data/Iterators/Combinators/Take.olean
+lib/lean/Init/Data/Iterators/Combinators/Take.olean.private
+lib/lean/Init/Data/Iterators/Combinators/Take.olean.server
 lib/lean/Init/Data/Iterators/Combinators/ULift.ilean
 lib/lean/Init/Data/Iterators/Combinators/ULift.ir
 lib/lean/Init/Data/Iterators/Combinators/ULift.olean
@@ -802,11 +812,21 @@ 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/Take.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.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
 lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean.private
 lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.olean.server
 lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.ilean
 lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.ir
 lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.olean
@@ -847,11 +867,51 @@ lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.ir
 lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean
 lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean.private
 lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Producers.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Producers.ir
+lib/lean/Init/Data/Iterators/Lemmas/Producers.olean
+lib/lean/Init/Data/Iterators/Lemmas/Producers.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Producers.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Producers/List.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Producers/List.ir
+lib/lean/Init/Data/Iterators/Lemmas/Producers/List.olean
+lib/lean/Init/Data/Iterators/Lemmas/Producers/List.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Producers/List.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.ir
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.olean
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.ir
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.olean
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.olean.server
 lib/lean/Init/Data/Iterators/PostconditionMonad.ilean
 lib/lean/Init/Data/Iterators/PostconditionMonad.ir
 lib/lean/Init/Data/Iterators/PostconditionMonad.olean
 lib/lean/Init/Data/Iterators/PostconditionMonad.olean.private
 lib/lean/Init/Data/Iterators/PostconditionMonad.olean.server
+lib/lean/Init/Data/Iterators/Producers.ilean
+lib/lean/Init/Data/Iterators/Producers.ir
+lib/lean/Init/Data/Iterators/Producers.olean
+lib/lean/Init/Data/Iterators/Producers.olean.private
+lib/lean/Init/Data/Iterators/Producers.olean.server
+lib/lean/Init/Data/Iterators/Producers/List.ilean
+lib/lean/Init/Data/Iterators/Producers/List.ir
+lib/lean/Init/Data/Iterators/Producers/List.olean
+lib/lean/Init/Data/Iterators/Producers/List.olean.private
+lib/lean/Init/Data/Iterators/Producers/List.olean.server
+lib/lean/Init/Data/Iterators/Producers/Monadic.ilean
+lib/lean/Init/Data/Iterators/Producers/Monadic.ir
+lib/lean/Init/Data/Iterators/Producers/Monadic.olean
+lib/lean/Init/Data/Iterators/Producers/Monadic.olean.private
+lib/lean/Init/Data/Iterators/Producers/Monadic.olean.server
+lib/lean/Init/Data/Iterators/Producers/Monadic/List.ilean
+lib/lean/Init/Data/Iterators/Producers/Monadic/List.ir
+lib/lean/Init/Data/Iterators/Producers/Monadic/List.olean
+lib/lean/Init/Data/Iterators/Producers/Monadic/List.olean.private
+lib/lean/Init/Data/Iterators/Producers/Monadic/List.olean.server
 lib/lean/Init/Data/Iterators/ToIterator.ilean
 lib/lean/Init/Data/Iterators/ToIterator.ir
 lib/lean/Init/Data/Iterators/ToIterator.olean
@@ -1407,6 +1467,11 @@ 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/IntLemmas.ilean
+lib/lean/Init/Data/Range/Polymorphic/IntLemmas.ir
+lib/lean/Init/Data/Range/Polymorphic/IntLemmas.olean
+lib/lean/Init/Data/Range/Polymorphic/IntLemmas.olean.private
+lib/lean/Init/Data/Range/Polymorphic/IntLemmas.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
@@ -1547,6 +1612,26 @@ lib/lean/Init/Data/Slice/Lemmas.ir
 lib/lean/Init/Data/Slice/Lemmas.olean
 lib/lean/Init/Data/Slice/Lemmas.olean.private
 lib/lean/Init/Data/Slice/Lemmas.olean.server
+lib/lean/Init/Data/Slice/List.ilean
+lib/lean/Init/Data/Slice/List.ir
+lib/lean/Init/Data/Slice/List.olean
+lib/lean/Init/Data/Slice/List.olean.private
+lib/lean/Init/Data/Slice/List.olean.server
+lib/lean/Init/Data/Slice/List/Basic.ilean
+lib/lean/Init/Data/Slice/List/Basic.ir
+lib/lean/Init/Data/Slice/List/Basic.olean
+lib/lean/Init/Data/Slice/List/Basic.olean.private
+lib/lean/Init/Data/Slice/List/Basic.olean.server
+lib/lean/Init/Data/Slice/List/Iterator.ilean
+lib/lean/Init/Data/Slice/List/Iterator.ir
+lib/lean/Init/Data/Slice/List/Iterator.olean
+lib/lean/Init/Data/Slice/List/Iterator.olean.private
+lib/lean/Init/Data/Slice/List/Iterator.olean.server
+lib/lean/Init/Data/Slice/List/Lemmas.ilean
+lib/lean/Init/Data/Slice/List/Lemmas.ir
+lib/lean/Init/Data/Slice/List/Lemmas.olean
+lib/lean/Init/Data/Slice/List/Lemmas.olean.private
+lib/lean/Init/Data/Slice/List/Lemmas.olean.server
 lib/lean/Init/Data/Slice/Notation.ilean
 lib/lean/Init/Data/Slice/Notation.ir
 lib/lean/Init/Data/Slice/Notation.olean
@@ -1582,16 +1667,61 @@ 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/Defs.ilean
+lib/lean/Init/Data/String/Defs.ir
+lib/lean/Init/Data/String/Defs.olean
+lib/lean/Init/Data/String/Defs.olean.private
+lib/lean/Init/Data/String/Defs.olean.server
 lib/lean/Init/Data/String/Extra.ilean
 lib/lean/Init/Data/String/Extra.ir
 lib/lean/Init/Data/String/Extra.olean
 lib/lean/Init/Data/String/Extra.olean.private
 lib/lean/Init/Data/String/Extra.olean.server
+lib/lean/Init/Data/String/Grind.ilean
+lib/lean/Init/Data/String/Grind.ir
+lib/lean/Init/Data/String/Grind.olean
+lib/lean/Init/Data/String/Grind.olean.private
+lib/lean/Init/Data/String/Grind.olean.server
+lib/lean/Init/Data/String/Iterator.ilean
+lib/lean/Init/Data/String/Iterator.ir
+lib/lean/Init/Data/String/Iterator.olean
+lib/lean/Init/Data/String/Iterator.olean.private
+lib/lean/Init/Data/String/Iterator.olean.server
+lib/lean/Init/Data/String/Legacy.ilean
+lib/lean/Init/Data/String/Legacy.ir
+lib/lean/Init/Data/String/Legacy.olean
+lib/lean/Init/Data/String/Legacy.olean.private
+lib/lean/Init/Data/String/Legacy.olean.server
 lib/lean/Init/Data/String/Lemmas.ilean
 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/Lemmas/Basic.ilean
+lib/lean/Init/Data/String/Lemmas/Basic.ir
+lib/lean/Init/Data/String/Lemmas/Basic.olean
+lib/lean/Init/Data/String/Lemmas/Basic.olean.private
+lib/lean/Init/Data/String/Lemmas/Basic.olean.server
+lib/lean/Init/Data/String/Lemmas/Modify.ilean
+lib/lean/Init/Data/String/Lemmas/Modify.ir
+lib/lean/Init/Data/String/Lemmas/Modify.olean
+lib/lean/Init/Data/String/Lemmas/Modify.olean.private
+lib/lean/Init/Data/String/Lemmas/Modify.olean.server
+lib/lean/Init/Data/String/Lemmas/Search.ilean
+lib/lean/Init/Data/String/Lemmas/Search.ir
+lib/lean/Init/Data/String/Lemmas/Search.olean
+lib/lean/Init/Data/String/Lemmas/Search.olean.private
+lib/lean/Init/Data/String/Lemmas/Search.olean.server
+lib/lean/Init/Data/String/Lemmas/Splits.ilean
+lib/lean/Init/Data/String/Lemmas/Splits.ir
+lib/lean/Init/Data/String/Lemmas/Splits.olean
+lib/lean/Init/Data/String/Lemmas/Splits.olean.private
+lib/lean/Init/Data/String/Lemmas/Splits.olean.server
+lib/lean/Init/Data/String/Modify.ilean
+lib/lean/Init/Data/String/Modify.ir
+lib/lean/Init/Data/String/Modify.olean
+lib/lean/Init/Data/String/Modify.olean.private
+lib/lean/Init/Data/String/Modify.olean.server
 lib/lean/Init/Data/String/Pattern.ilean
 lib/lean/Init/Data/String/Pattern.ir
 lib/lean/Init/Data/String/Pattern.olean
@@ -1617,11 +1747,16 @@ 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/PosRaw.ilean
+lib/lean/Init/Data/String/PosRaw.ir
+lib/lean/Init/Data/String/PosRaw.olean
+lib/lean/Init/Data/String/PosRaw.olean.private
+lib/lean/Init/Data/String/PosRaw.olean.server
+lib/lean/Init/Data/String/Search.ilean
+lib/lean/Init/Data/String/Search.ir
+lib/lean/Init/Data/String/Search.olean
+lib/lean/Init/Data/String/Search.olean.private
+lib/lean/Init/Data/String/Search.olean.server
 lib/lean/Init/Data/String/Slice.ilean
 lib/lean/Init/Data/String/Slice.ir
 lib/lean/Init/Data/String/Slice.olean
@@ -1632,6 +1767,26 @@ 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/String/Substring.ilean
+lib/lean/Init/Data/String/Substring.ir
+lib/lean/Init/Data/String/Substring.olean
+lib/lean/Init/Data/String/Substring.olean.private
+lib/lean/Init/Data/String/Substring.olean.server
+lib/lean/Init/Data/String/TakeDrop.ilean
+lib/lean/Init/Data/String/TakeDrop.ir
+lib/lean/Init/Data/String/TakeDrop.olean
+lib/lean/Init/Data/String/TakeDrop.olean.private
+lib/lean/Init/Data/String/TakeDrop.olean.server
+lib/lean/Init/Data/String/Termination.ilean
+lib/lean/Init/Data/String/Termination.ir
+lib/lean/Init/Data/String/Termination.olean
+lib/lean/Init/Data/String/Termination.olean.private
+lib/lean/Init/Data/String/Termination.olean.server
+lib/lean/Init/Data/String/ToSlice.ilean
+lib/lean/Init/Data/String/ToSlice.ir
+lib/lean/Init/Data/String/ToSlice.olean
+lib/lean/Init/Data/String/ToSlice.olean.private
+lib/lean/Init/Data/String/ToSlice.olean.server
 lib/lean/Init/Data/Subtype.ilean
 lib/lean/Init/Data/Subtype.ir
 lib/lean/Init/Data/Subtype.olean
@@ -1852,6 +2007,11 @@ 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/Annotated.ilean
+lib/lean/Init/Grind/Annotated.ir
+lib/lean/Init/Grind/Annotated.olean
+lib/lean/Init/Grind/Annotated.olean.private
+lib/lean/Init/Grind/Annotated.olean.server
 lib/lean/Init/Grind/Attr.ilean
 lib/lean/Init/Grind/Attr.ir
 lib/lean/Init/Grind/Attr.olean
@@ -1862,11 +2022,21 @@ lib/lean/Init/Grind/Cases.ir
 lib/lean/Init/Grind/Cases.olean
 lib/lean/Init/Grind/Cases.olean.private
 lib/lean/Init/Grind/Cases.olean.server
+lib/lean/Init/Grind/Config.ilean
+lib/lean/Init/Grind/Config.ir
+lib/lean/Init/Grind/Config.olean
+lib/lean/Init/Grind/Config.olean.private
+lib/lean/Init/Grind/Config.olean.server
 lib/lean/Init/Grind/Ext.ilean
 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/FieldNormNum.ilean
+lib/lean/Init/Grind/FieldNormNum.ir
+lib/lean/Init/Grind/FieldNormNum.olean
+lib/lean/Init/Grind/FieldNormNum.olean.private
+lib/lean/Init/Grind/FieldNormNum.olean.server
 lib/lean/Init/Grind/Injective.ilean
 lib/lean/Init/Grind/Injective.ir
 lib/lean/Init/Grind/Injective.olean
@@ -1882,6 +2052,11 @@ lib/lean/Init/Grind/Lemmas.ir
 lib/lean/Init/Grind/Lemmas.olean
 lib/lean/Init/Grind/Lemmas.olean.private
 lib/lean/Init/Grind/Lemmas.olean.server
+lib/lean/Init/Grind/Lint.ilean
+lib/lean/Init/Grind/Lint.ir
+lib/lean/Init/Grind/Lint.olean
+lib/lean/Init/Grind/Lint.olean.private
+lib/lean/Init/Grind/Lint.olean.server
 lib/lean/Init/Grind/Module.ilean
 lib/lean/Init/Grind/Module.ir
 lib/lean/Init/Grind/Module.olean
@@ -2002,6 +2177,11 @@ 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/OfScientific.ilean
+lib/lean/Init/Grind/Ring/OfScientific.ir
+lib/lean/Init/Grind/Ring/OfScientific.olean
+lib/lean/Init/Grind/Ring/OfScientific.olean.private
+lib/lean/Init/Grind/Ring/OfScientific.olean.server
 lib/lean/Init/Grind/Ring/ToInt.ilean
 lib/lean/Init/Grind/Ring/ToInt.ir
 lib/lean/Init/Grind/Ring/ToInt.olean
@@ -3292,6 +3472,11 @@ lib/lean/Lean/Compiler/IR/ToIRType.ir
 lib/lean/Lean/Compiler/IR/ToIRType.olean
 lib/lean/Lean/Compiler/IR/ToIRType.olean.private
 lib/lean/Lean/Compiler/IR/ToIRType.olean.server
+lib/lean/Lean/Compiler/IR/Toposort.ilean
+lib/lean/Lean/Compiler/IR/Toposort.ir
+lib/lean/Lean/Compiler/IR/Toposort.olean
+lib/lean/Lean/Compiler/IR/Toposort.olean.private
+lib/lean/Lean/Compiler/IR/Toposort.olean.server
 lib/lean/Lean/Compiler/IR/UnboxResult.ilean
 lib/lean/Lean/Compiler/IR/UnboxResult.ir
 lib/lean/Lean/Compiler/IR/UnboxResult.olean
@@ -3422,6 +3607,11 @@ lib/lean/Lean/Compiler/LCNF/Internalize.ir
 lib/lean/Lean/Compiler/LCNF/Internalize.olean
 lib/lean/Lean/Compiler/LCNF/Internalize.olean.private
 lib/lean/Lean/Compiler/LCNF/Internalize.olean.server
+lib/lean/Lean/Compiler/LCNF/Irrelevant.ilean
+lib/lean/Lean/Compiler/LCNF/Irrelevant.ir
+lib/lean/Lean/Compiler/LCNF/Irrelevant.olean
+lib/lean/Lean/Compiler/LCNF/Irrelevant.olean.private
+lib/lean/Lean/Compiler/LCNF/Irrelevant.olean.server
 lib/lean/Lean/Compiler/LCNF/JoinPoints.ilean
 lib/lean/Lean/Compiler/LCNF/JoinPoints.ir
 lib/lean/Lean/Compiler/LCNF/JoinPoints.olean
@@ -3652,6 +3842,11 @@ lib/lean/Lean/Compiler/MetaAttr.ir
 lib/lean/Lean/Compiler/MetaAttr.olean
 lib/lean/Lean/Compiler/MetaAttr.olean.private
 lib/lean/Lean/Compiler/MetaAttr.olean.server
+lib/lean/Lean/Compiler/ModPkgExt.ilean
+lib/lean/Lean/Compiler/ModPkgExt.ir
+lib/lean/Lean/Compiler/ModPkgExt.olean
+lib/lean/Lean/Compiler/ModPkgExt.olean.private
+lib/lean/Lean/Compiler/ModPkgExt.olean.server
 lib/lean/Lean/Compiler/NameMangling.ilean
 lib/lean/Lean/Compiler/NameMangling.ir
 lib/lean/Lean/Compiler/NameMangling.olean
@@ -4132,6 +4327,11 @@ lib/lean/Lean/Elab/Command/Scope.ir
 lib/lean/Lean/Elab/Command/Scope.olean
 lib/lean/Lean/Elab/Command/Scope.olean.private
 lib/lean/Lean/Elab/Command/Scope.olean.server
+lib/lean/Lean/Elab/Command/WithWeakNamespace.ilean
+lib/lean/Lean/Elab/Command/WithWeakNamespace.ir
+lib/lean/Lean/Elab/Command/WithWeakNamespace.olean
+lib/lean/Lean/Elab/Command/WithWeakNamespace.olean.private
+lib/lean/Lean/Elab/Command/WithWeakNamespace.olean.server
 lib/lean/Lean/Elab/ComputedFields.ilean
 lib/lean/Lean/Elab/ComputedFields.ir
 lib/lean/Lean/Elab/ComputedFields.olean
@@ -4257,6 +4457,21 @@ lib/lean/Lean/Elab/Do.ir
 lib/lean/Lean/Elab/Do.olean
 lib/lean/Lean/Elab/Do.olean.private
 lib/lean/Lean/Elab/Do.olean.server
+lib/lean/Lean/Elab/Do/Basic.ilean
+lib/lean/Lean/Elab/Do/Basic.ir
+lib/lean/Lean/Elab/Do/Basic.olean
+lib/lean/Lean/Elab/Do/Basic.olean.private
+lib/lean/Lean/Elab/Do/Basic.olean.server
+lib/lean/Lean/Elab/Do/Legacy.ilean
+lib/lean/Lean/Elab/Do/Legacy.ir
+lib/lean/Lean/Elab/Do/Legacy.olean
+lib/lean/Lean/Elab/Do/Legacy.olean.private
+lib/lean/Lean/Elab/Do/Legacy.olean.server
+lib/lean/Lean/Elab/Do/Switch.ilean
+lib/lean/Lean/Elab/Do/Switch.ir
+lib/lean/Lean/Elab/Do/Switch.olean
+lib/lean/Lean/Elab/Do/Switch.olean.private
+lib/lean/Lean/Elab/Do/Switch.olean.server
 lib/lean/Lean/Elab/DocString.ilean
 lib/lean/Lean/Elab/DocString.ir
 lib/lean/Lean/Elab/DocString.olean
@@ -4432,6 +4647,11 @@ lib/lean/Lean/Elab/Open.ir
 lib/lean/Lean/Elab/Open.olean
 lib/lean/Lean/Elab/Open.olean.private
 lib/lean/Lean/Elab/Open.olean.server
+lib/lean/Lean/Elab/Parallel.ilean
+lib/lean/Lean/Elab/Parallel.ir
+lib/lean/Lean/Elab/Parallel.olean
+lib/lean/Lean/Elab/Parallel.olean.private
+lib/lean/Lean/Elab/Parallel.olean.server
 lib/lean/Lean/Elab/ParseImportsFast.ilean
 lib/lean/Lean/Elab/ParseImportsFast.ir
 lib/lean/Lean/Elab/ParseImportsFast.olean
@@ -4882,6 +5102,11 @@ lib/lean/Lean/Elab/Tactic/Config.ir
 lib/lean/Lean/Elab/Tactic/Config.olean
 lib/lean/Lean/Elab/Tactic/Config.olean.private
 lib/lean/Lean/Elab/Tactic/Config.olean.server
+lib/lean/Lean/Elab/Tactic/ConfigSetter.ilean
+lib/lean/Lean/Elab/Tactic/ConfigSetter.ir
+lib/lean/Lean/Elab/Tactic/ConfigSetter.olean
+lib/lean/Lean/Elab/Tactic/ConfigSetter.olean.private
+lib/lean/Lean/Elab/Tactic/ConfigSetter.olean.server
 lib/lean/Lean/Elab/Tactic/Congr.ilean
 lib/lean/Lean/Elab/Tactic/Congr.ir
 lib/lean/Lean/Elab/Tactic/Congr.olean
@@ -5127,6 +5352,16 @@ lib/lean/Lean/Elab/Tactic/Grind.ir
 lib/lean/Lean/Elab/Tactic/Grind.olean
 lib/lean/Lean/Elab/Tactic/Grind.olean.private
 lib/lean/Lean/Elab/Tactic/Grind.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/Anchor.ilean
+lib/lean/Lean/Elab/Tactic/Grind/Anchor.ir
+lib/lean/Lean/Elab/Tactic/Grind/Anchor.olean
+lib/lean/Lean/Elab/Tactic/Grind/Anchor.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/Anchor.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/Annotated.ilean
+lib/lean/Lean/Elab/Tactic/Grind/Annotated.ir
+lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean
+lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean.server
 lib/lean/Lean/Elab/Tactic/Grind/Basic.ilean
 lib/lean/Lean/Elab/Tactic/Grind/Basic.ir
 lib/lean/Lean/Elab/Tactic/Grind/Basic.olean
@@ -5137,6 +5372,11 @@ lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.ir
 lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean
 lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean.private
 lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/Config.ilean
+lib/lean/Lean/Elab/Tactic/Grind/Config.ir
+lib/lean/Lean/Elab/Tactic/Grind/Config.olean
+lib/lean/Lean/Elab/Tactic/Grind/Config.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/Config.olean.server
 lib/lean/Lean/Elab/Tactic/Grind/Filter.ilean
 lib/lean/Lean/Elab/Tactic/Grind/Filter.ir
 lib/lean/Lean/Elab/Tactic/Grind/Filter.olean
@@ -5147,11 +5387,26 @@ lib/lean/Lean/Elab/Tactic/Grind/Have.ir
 lib/lean/Lean/Elab/Tactic/Grind/Have.olean
 lib/lean/Lean/Elab/Tactic/Grind/Have.olean.private
 lib/lean/Lean/Elab/Tactic/Grind/Have.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/Lint.ilean
+lib/lean/Lean/Elab/Tactic/Grind/Lint.ir
+lib/lean/Lean/Elab/Tactic/Grind/Lint.olean
+lib/lean/Lean/Elab/Tactic/Grind/Lint.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/Lint.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.ilean
+lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.ir
+lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.olean
+lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.olean.server
 lib/lean/Lean/Elab/Tactic/Grind/Main.ilean
 lib/lean/Lean/Elab/Tactic/Grind/Main.ir
 lib/lean/Lean/Elab/Tactic/Grind/Main.olean
 lib/lean/Lean/Elab/Tactic/Grind/Main.olean.private
 lib/lean/Lean/Elab/Tactic/Grind/Main.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/Param.ilean
+lib/lean/Lean/Elab/Tactic/Grind/Param.ir
+lib/lean/Lean/Elab/Tactic/Grind/Param.olean
+lib/lean/Lean/Elab/Tactic/Grind/Param.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/Param.olean.server
 lib/lean/Lean/Elab/Tactic/Grind/ShowState.ilean
 lib/lean/Lean/Elab/Tactic/Grind/ShowState.ir
 lib/lean/Lean/Elab/Tactic/Grind/ShowState.olean
@@ -5332,6 +5587,11 @@ lib/lean/Lean/Elab/Tactic/Unfold.ir
 lib/lean/Lean/Elab/Tactic/Unfold.olean
 lib/lean/Lean/Elab/Tactic/Unfold.olean.private
 lib/lean/Lean/Elab/Tactic/Unfold.olean.server
+lib/lean/Lean/Elab/Task.ilean
+lib/lean/Lean/Elab/Task.ir
+lib/lean/Lean/Elab/Task.olean
+lib/lean/Lean/Elab/Task.olean.private
+lib/lean/Lean/Elab/Task.olean.server
 lib/lean/Lean/Elab/Term.ilean
 lib/lean/Lean/Elab/Term.ir
 lib/lean/Lean/Elab/Term.olean
@@ -5387,6 +5647,11 @@ lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.ir
 lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.olean
 lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.olean.private
 lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.olean.server
+lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.ilean
+lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.ir
+lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.olean
+lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.olean.private
+lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.olean.server
 lib/lean/Lean/ErrorExplanations/InductiveParamMismatch.ilean
 lib/lean/Lean/ErrorExplanations/InductiveParamMismatch.ir
 lib/lean/Lean/ErrorExplanations/InductiveParamMismatch.olean
@@ -5427,6 +5692,11 @@ lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.ir
 lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.olean
 lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.olean.private
 lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.olean.server
+lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.ilean
+lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.ir
+lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.olean
+lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.olean.private
+lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.olean.server
 lib/lean/Lean/ErrorExplanations/UnknownIdentifier.ilean
 lib/lean/Lean/ErrorExplanations/UnknownIdentifier.ir
 lib/lean/Lean/ErrorExplanations/UnknownIdentifier.olean
@@ -5502,6 +5772,36 @@ lib/lean/Lean/Level.ir
 lib/lean/Lean/Level.olean
 lib/lean/Lean/Level.olean.private
 lib/lean/Lean/Level.olean.server
+lib/lean/Lean/LibrarySuggestions.ilean
+lib/lean/Lean/LibrarySuggestions.ir
+lib/lean/Lean/LibrarySuggestions.olean
+lib/lean/Lean/LibrarySuggestions.olean.private
+lib/lean/Lean/LibrarySuggestions.olean.server
+lib/lean/Lean/LibrarySuggestions/Basic.ilean
+lib/lean/Lean/LibrarySuggestions/Basic.ir
+lib/lean/Lean/LibrarySuggestions/Basic.olean
+lib/lean/Lean/LibrarySuggestions/Basic.olean.private
+lib/lean/Lean/LibrarySuggestions/Basic.olean.server
+lib/lean/Lean/LibrarySuggestions/Default.ilean
+lib/lean/Lean/LibrarySuggestions/Default.ir
+lib/lean/Lean/LibrarySuggestions/Default.olean
+lib/lean/Lean/LibrarySuggestions/Default.olean.private
+lib/lean/Lean/LibrarySuggestions/Default.olean.server
+lib/lean/Lean/LibrarySuggestions/MePo.ilean
+lib/lean/Lean/LibrarySuggestions/MePo.ir
+lib/lean/Lean/LibrarySuggestions/MePo.olean
+lib/lean/Lean/LibrarySuggestions/MePo.olean.private
+lib/lean/Lean/LibrarySuggestions/MePo.olean.server
+lib/lean/Lean/LibrarySuggestions/SineQuaNon.ilean
+lib/lean/Lean/LibrarySuggestions/SineQuaNon.ir
+lib/lean/Lean/LibrarySuggestions/SineQuaNon.olean
+lib/lean/Lean/LibrarySuggestions/SineQuaNon.olean.private
+lib/lean/Lean/LibrarySuggestions/SineQuaNon.olean.server
+lib/lean/Lean/LibrarySuggestions/SymbolFrequency.ilean
+lib/lean/Lean/LibrarySuggestions/SymbolFrequency.ir
+lib/lean/Lean/LibrarySuggestions/SymbolFrequency.olean
+lib/lean/Lean/LibrarySuggestions/SymbolFrequency.olean.private
+lib/lean/Lean/LibrarySuggestions/SymbolFrequency.olean.server
 lib/lean/Lean/Linter.ilean
 lib/lean/Lean/Linter.ir
 lib/lean/Lean/Linter.olean
@@ -5637,6 +5937,11 @@ lib/lean/Lean/Meta/Canonicalizer.ir
 lib/lean/Lean/Meta/Canonicalizer.olean
 lib/lean/Lean/Meta/Canonicalizer.olean.private
 lib/lean/Lean/Meta/Canonicalizer.olean.server
+lib/lean/Lean/Meta/CasesInfo.ilean
+lib/lean/Lean/Meta/CasesInfo.ir
+lib/lean/Lean/Meta/CasesInfo.olean
+lib/lean/Lean/Meta/CasesInfo.olean.private
+lib/lean/Lean/Meta/CasesInfo.olean.server
 lib/lean/Lean/Meta/Check.ilean
 lib/lean/Lean/Meta/Check.ir
 lib/lean/Lean/Meta/Check.olean
@@ -5722,6 +6027,11 @@ lib/lean/Lean/Meta/Constructions/RecOn.ir
 lib/lean/Lean/Meta/Constructions/RecOn.olean
 lib/lean/Lean/Meta/Constructions/RecOn.olean.private
 lib/lean/Lean/Meta/Constructions/RecOn.olean.server
+lib/lean/Lean/Meta/Constructions/SparseCasesOn.ilean
+lib/lean/Lean/Meta/Constructions/SparseCasesOn.ir
+lib/lean/Lean/Meta/Constructions/SparseCasesOn.olean
+lib/lean/Lean/Meta/Constructions/SparseCasesOn.olean.private
+lib/lean/Lean/Meta/Constructions/SparseCasesOn.olean.server
 lib/lean/Lean/Meta/CtorRecognizer.ilean
 lib/lean/Lean/Meta/CtorRecognizer.ir
 lib/lean/Lean/Meta/CtorRecognizer.olean
@@ -5802,6 +6112,11 @@ lib/lean/Lean/Meta/GlobalInstances.ir
 lib/lean/Lean/Meta/GlobalInstances.olean
 lib/lean/Lean/Meta/GlobalInstances.olean.private
 lib/lean/Lean/Meta/GlobalInstances.olean.server
+lib/lean/Lean/Meta/HasNotBit.ilean
+lib/lean/Lean/Meta/HasNotBit.ir
+lib/lean/Lean/Meta/HasNotBit.olean
+lib/lean/Lean/Meta/HasNotBit.olean.private
+lib/lean/Lean/Meta/HasNotBit.olean.server
 lib/lean/Lean/Meta/Hint.ilean
 lib/lean/Lean/Meta/Hint.ir
 lib/lean/Lean/Meta/Hint.olean
@@ -5937,6 +6252,16 @@ lib/lean/Lean/Meta/Match/MatcherInfo.ir
 lib/lean/Lean/Meta/Match/MatcherInfo.olean
 lib/lean/Lean/Meta/Match/MatcherInfo.olean.private
 lib/lean/Lean/Meta/Match/MatcherInfo.olean.server
+lib/lean/Lean/Meta/Match/SimpH.ilean
+lib/lean/Lean/Meta/Match/SimpH.ir
+lib/lean/Lean/Meta/Match/SimpH.olean
+lib/lean/Lean/Meta/Match/SimpH.olean.private
+lib/lean/Lean/Meta/Match/SimpH.olean.server
+lib/lean/Lean/Meta/Match/SolveOverlap.ilean
+lib/lean/Lean/Meta/Match/SolveOverlap.ir
+lib/lean/Lean/Meta/Match/SolveOverlap.olean
+lib/lean/Lean/Meta/Match/SolveOverlap.olean.private
+lib/lean/Lean/Meta/Match/SolveOverlap.olean.server
 lib/lean/Lean/Meta/Match/Value.ilean
 lib/lean/Lean/Meta/Match/Value.ir
 lib/lean/Lean/Meta/Match/Value.olean
@@ -5987,6 +6312,11 @@ lib/lean/Lean/Meta/PProdN.ir
 lib/lean/Lean/Meta/PProdN.olean
 lib/lean/Lean/Meta/PProdN.olean.private
 lib/lean/Lean/Meta/PProdN.olean.server
+lib/lean/Lean/Meta/ProdN.ilean
+lib/lean/Lean/Meta/ProdN.ir
+lib/lean/Lean/Meta/ProdN.olean
+lib/lean/Lean/Meta/ProdN.olean.private
+lib/lean/Lean/Meta/ProdN.olean.server
 lib/lean/Lean/Meta/RecursorInfo.ilean
 lib/lean/Lean/Meta/RecursorInfo.ir
 lib/lean/Lean/Meta/RecursorInfo.olean
@@ -6312,6 +6642,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.olean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.ir
+lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.olean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.olean
@@ -6467,11 +6802,21 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.olean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.ir
+lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.olean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.ir
+lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.olean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.olean
@@ -6482,6 +6827,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.ir
+lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.olean
+lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.olean
@@ -6597,36 +6947,6 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.olean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.olean
@@ -6677,6 +6997,11 @@ lib/lean/Lean/Meta/Tactic/Grind/CheckResult.ir
 lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean
 lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/CollectParams.ilean
+lib/lean/Lean/Meta/Tactic/Grind/CollectParams.ir
+lib/lean/Lean/Meta/Tactic/Grind/CollectParams.olean
+lib/lean/Lean/Meta/Tactic/Grind/CollectParams.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/CollectParams.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Core.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Core.ir
 lib/lean/Lean/Meta/Tactic/Grind/Core.olean
@@ -6712,6 +7037,11 @@ lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.ir
 lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean
 lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.ilean
+lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.ir
+lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.olean
+lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/EqResolution.ilean
 lib/lean/Lean/Meta/Tactic/Grind/EqResolution.ir
 lib/lean/Lean/Meta/Tactic/Grind/EqResolution.olean
@@ -6732,11 +7062,26 @@ lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.ir
 lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.olean
 lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Filter.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Filter.ir
+lib/lean/Lean/Meta/Tactic/Grind/Filter.olean
+lib/lean/Lean/Meta/Tactic/Grind/Filter.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Filter.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Finish.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Finish.ir
+lib/lean/Lean/Meta/Tactic/Grind/Finish.olean
+lib/lean/Lean/Meta/Tactic/Grind/Finish.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Finish.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/ForallProp.ilean
 lib/lean/Lean/Meta/Tactic/Grind/ForallProp.ir
 lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean
 lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/FunCC.ilean
+lib/lean/Lean/Meta/Tactic/Grind/FunCC.ir
+lib/lean/Lean/Meta/Tactic/Grind/FunCC.olean
+lib/lean/Lean/Meta/Tactic/Grind/FunCC.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/FunCC.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Injection.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Injection.ir
 lib/lean/Lean/Meta/Tactic/Grind/Injection.olean
@@ -6897,11 +7242,6 @@ lib/lean/Lean/Meta/Tactic/Grind/RevertAll.ir
 lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean
 lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/SearchM.ilean
-lib/lean/Lean/Meta/Tactic/Grind/SearchM.ir
-lib/lean/Lean/Meta/Tactic/Grind/SearchM.olean
-lib/lean/Lean/Meta/Tactic/Grind/SearchM.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/SearchM.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Simp.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Simp.ir
 lib/lean/Lean/Meta/Tactic/Grind/Simp.olean
@@ -7392,21 +7732,6 @@ lib/lean/Lean/ParserCompiler/Attribute.ir
 lib/lean/Lean/ParserCompiler/Attribute.olean
 lib/lean/Lean/ParserCompiler/Attribute.olean.private
 lib/lean/Lean/ParserCompiler/Attribute.olean.server
-lib/lean/Lean/PremiseSelection.ilean
-lib/lean/Lean/PremiseSelection.ir
-lib/lean/Lean/PremiseSelection.olean
-lib/lean/Lean/PremiseSelection.olean.private
-lib/lean/Lean/PremiseSelection.olean.server
-lib/lean/Lean/PremiseSelection/Basic.ilean
-lib/lean/Lean/PremiseSelection/Basic.ir
-lib/lean/Lean/PremiseSelection/Basic.olean
-lib/lean/Lean/PremiseSelection/Basic.olean.private
-lib/lean/Lean/PremiseSelection/Basic.olean.server
-lib/lean/Lean/PremiseSelection/MePo.ilean
-lib/lean/Lean/PremiseSelection/MePo.ir
-lib/lean/Lean/PremiseSelection/MePo.olean
-lib/lean/Lean/PremiseSelection/MePo.olean.private
-lib/lean/Lean/PremiseSelection/MePo.olean.server
 lib/lean/Lean/PrettyPrinter.ilean
 lib/lean/Lean/PrettyPrinter.ir
 lib/lean/Lean/PrettyPrinter.olean
@@ -7647,6 +7972,16 @@ lib/lean/Lean/Server/InfoUtils.ir
 lib/lean/Lean/Server/InfoUtils.olean
 lib/lean/Lean/Server/InfoUtils.olean.private
 lib/lean/Lean/Server/InfoUtils.olean.server
+lib/lean/Lean/Server/Logging.ilean
+lib/lean/Lean/Server/Logging.ir
+lib/lean/Lean/Server/Logging.olean
+lib/lean/Lean/Server/Logging.olean.private
+lib/lean/Lean/Server/Logging.olean.server
+lib/lean/Lean/Server/ProtocolOverview.ilean
+lib/lean/Lean/Server/ProtocolOverview.ir
+lib/lean/Lean/Server/ProtocolOverview.olean
+lib/lean/Lean/Server/ProtocolOverview.olean.private
+lib/lean/Lean/Server/ProtocolOverview.olean.server
 lib/lean/Lean/Server/References.ilean
 lib/lean/Lean/Server/References.ir
 lib/lean/Lean/Server/References.olean
@@ -7887,6 +8222,11 @@ lib/lean/Lean/Util/PPExt.ir
 lib/lean/Lean/Util/PPExt.olean
 lib/lean/Lean/Util/PPExt.olean.private
 lib/lean/Lean/Util/PPExt.olean.server
+lib/lean/Lean/Util/ParamMinimizer.ilean
+lib/lean/Lean/Util/ParamMinimizer.ir
+lib/lean/Lean/Util/ParamMinimizer.olean
+lib/lean/Lean/Util/ParamMinimizer.olean.private
+lib/lean/Lean/Util/ParamMinimizer.olean.server
 lib/lean/Lean/Util/Path.ilean
 lib/lean/Lean/Util/Path.ir
 lib/lean/Lean/Util/Path.olean
@@ -8199,6 +8539,16 @@ lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.ir
 lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.olean
 lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.olean.private
 lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.olean.server
+lib/lean/Std/Data/DTreeMap/Internal/Zipper.ilean
+lib/lean/Std/Data/DTreeMap/Internal/Zipper.ir
+lib/lean/Std/Data/DTreeMap/Internal/Zipper.olean
+lib/lean/Std/Data/DTreeMap/Internal/Zipper.olean.private
+lib/lean/Std/Data/DTreeMap/Internal/Zipper.olean.server
+lib/lean/Std/Data/DTreeMap/Iterator.ilean
+lib/lean/Std/Data/DTreeMap/Iterator.ir
+lib/lean/Std/Data/DTreeMap/Iterator.olean
+lib/lean/Std/Data/DTreeMap/Iterator.olean.private
+lib/lean/Std/Data/DTreeMap/Iterator.olean.server
 lib/lean/Std/Data/DTreeMap/Lemmas.ilean
 lib/lean/Std/Data/DTreeMap/Lemmas.ir
 lib/lean/Std/Data/DTreeMap/Lemmas.olean
@@ -8219,16 +8569,31 @@ lib/lean/Std/Data/DTreeMap/Raw/Basic.ir
 lib/lean/Std/Data/DTreeMap/Raw/Basic.olean
 lib/lean/Std/Data/DTreeMap/Raw/Basic.olean.private
 lib/lean/Std/Data/DTreeMap/Raw/Basic.olean.server
+lib/lean/Std/Data/DTreeMap/Raw/Iterator.ilean
+lib/lean/Std/Data/DTreeMap/Raw/Iterator.ir
+lib/lean/Std/Data/DTreeMap/Raw/Iterator.olean
+lib/lean/Std/Data/DTreeMap/Raw/Iterator.olean.private
+lib/lean/Std/Data/DTreeMap/Raw/Iterator.olean.server
 lib/lean/Std/Data/DTreeMap/Raw/Lemmas.ilean
 lib/lean/Std/Data/DTreeMap/Raw/Lemmas.ir
 lib/lean/Std/Data/DTreeMap/Raw/Lemmas.olean
 lib/lean/Std/Data/DTreeMap/Raw/Lemmas.olean.private
 lib/lean/Std/Data/DTreeMap/Raw/Lemmas.olean.server
+lib/lean/Std/Data/DTreeMap/Raw/Slice.ilean
+lib/lean/Std/Data/DTreeMap/Raw/Slice.ir
+lib/lean/Std/Data/DTreeMap/Raw/Slice.olean
+lib/lean/Std/Data/DTreeMap/Raw/Slice.olean.private
+lib/lean/Std/Data/DTreeMap/Raw/Slice.olean.server
 lib/lean/Std/Data/DTreeMap/Raw/WF.ilean
 lib/lean/Std/Data/DTreeMap/Raw/WF.ir
 lib/lean/Std/Data/DTreeMap/Raw/WF.olean
 lib/lean/Std/Data/DTreeMap/Raw/WF.olean.private
 lib/lean/Std/Data/DTreeMap/Raw/WF.olean.server
+lib/lean/Std/Data/DTreeMap/Slice.ilean
+lib/lean/Std/Data/DTreeMap/Slice.ir
+lib/lean/Std/Data/DTreeMap/Slice.olean
+lib/lean/Std/Data/DTreeMap/Slice.olean.private
+lib/lean/Std/Data/DTreeMap/Slice.olean.server
 lib/lean/Std/Data/ExtDHashMap.ilean
 lib/lean/Std/Data/ExtDHashMap.ir
 lib/lean/Std/Data/ExtDHashMap.olean
@@ -8449,11 +8814,6 @@ lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.ir
 lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.olean
 lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.olean.private
 lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.olean.server
-lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.ilean
-lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.ir
-lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.olean
-lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.olean.private
-lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.olean.server
 lib/lean/Std/Data/Iterators/Combinators/Monadic/TakeWhile.ilean
 lib/lean/Std/Data/Iterators/Combinators/Monadic/TakeWhile.ir
 lib/lean/Std/Data/Iterators/Combinators/Monadic/TakeWhile.olean
@@ -8469,11 +8829,6 @@ lib/lean/Std/Data/Iterators/Combinators/StepSize.ir
 lib/lean/Std/Data/Iterators/Combinators/StepSize.olean
 lib/lean/Std/Data/Iterators/Combinators/StepSize.olean.private
 lib/lean/Std/Data/Iterators/Combinators/StepSize.olean.server
-lib/lean/Std/Data/Iterators/Combinators/Take.ilean
-lib/lean/Std/Data/Iterators/Combinators/Take.ir
-lib/lean/Std/Data/Iterators/Combinators/Take.olean
-lib/lean/Std/Data/Iterators/Combinators/Take.olean.private
-lib/lean/Std/Data/Iterators/Combinators/Take.olean.server
 lib/lean/Std/Data/Iterators/Combinators/TakeWhile.ilean
*** 634 LINES SKIPPED ***