git: 9bcf1534aa79 - main - math/lean4: update 4.34.1 → 4.35.0

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Tue, 13 Oct 2026 22:57:36 UTC
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=9bcf1534aa79c923ed5a56fa1ae206d738bc82ab

commit 9bcf1534aa79c923ed5a56fa1ae206d738bc82ab
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2026-10-13 22:17:47 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2026-10-13 22:57:26 +0000

    math/lean4: update 4.34.1 → 4.35.0
---
 math/lean4/Makefile                              |   12 +-
 math/lean4/distinfo                              |   12 +-
 math/lean4/files/patch-CMakeLists.txt            |    4 +-
 math/lean4/files/patch-src_CMakeLists.txt        |   26 +-
 math/lean4/files/patch-src_include_lean_lean.h   |    4 +-
 math/lean4/files/patch-stage0_src_CMakeLists.txt |   12 +
 math/lean4/files/patch-tests_CMakeLists.txt      |   10 +-
 math/lean4/pkg-plist                             | 1062 +++++++++++++---------
 8 files changed, 678 insertions(+), 464 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 40643f167cd2..6bc18b91d105 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.34.1
+DISTVERSION=	4.35.0
 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
@@ -30,7 +30,8 @@ USES=		cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build #
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	leanprover
-GH_TUPLE=	microsoft:mimalloc:v3.4.4:mimalloc/cmake/mimalloc/src/mimalloc
+GH_TUPLE=	microsoft:mimalloc:v3.4.5:mimalloc/cmake/mimalloc/src/mimalloc \
+		Kha:lean4lean:lean4-bundle-4.35:lean4lean/ext/lean4lean
 
 CFLAGS+=	-fPIC
 CXXFLAGS+=	-fPIC
@@ -84,6 +85,12 @@ pre-everything::
 	@${ECHO_MSG} ""
 
 post-patch:
+	# Disable git downloads of optional checkers (not built by default)
+	@${REINPLACE_CMD} -E \
+		-e 's|GIT_REPOSITORY https://github.com/(ammkrn/nanoda_lib\|leanprover/con-leche\|leanprover/con-ron)|DOWNLOAD_COMMAND ""|' \
+		-e '/GIT_TAG [0-9a-f]{40}/d' \
+		-e '/GIT_SUBMODULES ""/d' \
+		${WRKSRC}/src/CMakeLists.txt ${WRKSRC}/stage0/src/CMakeLists.txt
 	# Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files
 	# Skip inputFile test: its translate-config test expects exact TOML-to-Lean output
 	@${FIND} ${WRKSRC}/tests -name "lakefile.toml" -not -path "*/inputFile/*" | while read f; do \
@@ -121,5 +128,6 @@ post-install:
 # tests as of 4.33.1: 100% tests passed, 0 tests failed out of 3988
 # tests as of 4.34.0: 100% tests pass (individual testsuite runs have intermittent failures with different tests, but all individual tests pass when run separately)
 # tests as of 4.34.1: 99% tests passed, 1 tests failed out of 4068: the 2 months old test cacheTransfer/test.sh fails, see https://github.com/leanprover/lean4/issues/15335
+# tests as of 4.35.0: 99% tests passed, 2 tests failed out of 4218: same cacheTransfer/test.sh failure, pkg/float failure
 
 .include <bsd.port.mk>
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index 36ca075362dc..7fa826b09a66 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,5 +1,7 @@
-TIMESTAMP = 1790373274
-SHA256 (leanprover-lean4-v4.34.1_GH0.tar.gz) = 9bb0bed7bae752a281e9923163d50da4193e36480cf5f639658e2e1502294056
-SIZE (leanprover-lean4-v4.34.1_GH0.tar.gz) = 87768894
-SHA256 (microsoft-mimalloc-v3.4.4_GH0.tar.gz) = 8ba991a7266983bd5eefc36e140c24734f720fd9b1fd79ddaeff44ea85d16760
-SIZE (microsoft-mimalloc-v3.4.4_GH0.tar.gz) = 1422232
+TIMESTAMP = 1791876408
+SHA256 (leanprover-lean4-v4.35.0_GH0.tar.gz) = 6747b099d03d3675f2716e7cf5924a16bfbf75822b13a3d36f51f933ffcc307b
+SIZE (leanprover-lean4-v4.35.0_GH0.tar.gz) = 90233735
+SHA256 (microsoft-mimalloc-v3.4.5_GH0.tar.gz) = 19a43af0645c57d348e729d5b31e23e912582911bb1047f795790834d3416221
+SIZE (microsoft-mimalloc-v3.4.5_GH0.tar.gz) = 1423876
+SHA256 (Kha-lean4lean-lean4-bundle-4.35_GH0.tar.gz) = 8e0b486737e8b812753317bc504e6e3afc3716398b0a2c19516a1143177291a9
+SIZE (Kha-lean4lean-lean4-bundle-4.35_GH0.tar.gz) = 444970
diff --git a/math/lean4/files/patch-CMakeLists.txt b/math/lean4/files/patch-CMakeLists.txt
index a33475f08b7f..28d52eb87b17 100644
--- a/math/lean4/files/patch-CMakeLists.txt
+++ b/math/lean4/files/patch-CMakeLists.txt
@@ -1,4 +1,4 @@
---- CMakeLists.txt.orig	2026-09-24 17:27:27 UTC
+--- CMakeLists.txt.orig	2026-10-12 15:51:15 UTC
 +++ CMakeLists.txt
 @@ -129,14 +129,8 @@ if(USE_MIMALLOC)
  if(USE_MIMALLOC)
@@ -6,7 +6,7 @@
      mimalloc
 -    GIT_REPOSITORY https://github.com/microsoft/mimalloc
 -    GIT_BRANCH dev3
--    GIT_TAG v3.4.4
+-    GIT_TAG v3.4.5
 -    # Unnecessarily deep directory structure, but it saves us from a complicated
 -    # stage0 update for now. If we ever update the other dependencies like
 -    # cadical, it might be worth reorganizing the directory structure.
diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt
index 8098ed7948d6..635399ff4c7a 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	2026-07-22 17:50:04 UTC
+--- src/CMakeLists.txt.orig	2026-10-12 15:51:15 UTC
 +++ src/CMakeLists.txt
-@@ -407,7 +407,7 @@ endif()
+@@ -452,7 +452,7 @@ endif()
    endif()
  endif()
  
@@ -9,7 +9,7 @@
  
  # Pick up `llvm-config` to setup LLVM flags.
  if(LLVM)
-@@ -549,7 +549,7 @@ endif()
+@@ -594,7 +594,7 @@ endif()
    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm")
  endif()
  
@@ -18,8 +18,8 @@
    if(BSYMBOLIC)
      string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
      string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
-@@ -562,6 +562,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
-     " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
+@@ -611,6 +611,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+     " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLeanExport.a.export -Wl,-soname=libLake_shared.so"
    )
    string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
 +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
@@ -38,7 +38,7 @@
  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")
-@@ -720,6 +733,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
+@@ -783,6 +796,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")
  
@@ -48,7 +48,19 @@
  # 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}}")
-@@ -1037,7 +1053,7 @@ install(
+@@ -1036,8 +1052,9 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+     lean4lean
+     PREFIX lean4lean
+     EXCLUDE_FROM_ALL ON
+-    GIT_REPOSITORY https://github.com/Kha/lean4lean
+-    GIT_TAG lean4-bundle-4.35
++    SOURCE_DIR ${LEAN_SOURCE_DIR}/../ext/lean4lean
++    DOWNLOAD_COMMAND ""
++    UPDATE_COMMAND ""
+     PATCH_COMMAND bash ${LEAN_SOURCE_DIR}/../script/lean4lean-minimal-init.sh
+     CONFIGURE_COMMAND ""
+     BUILD_COMMAND lake build lean4lean
+@@ -1202,7 +1219,7 @@ install(
  
  install(
    DIRECTORY "${CMAKE_SOURCE_DIR}/"
diff --git a/math/lean4/files/patch-src_include_lean_lean.h b/math/lean4/files/patch-src_include_lean_lean.h
index 85a25f0ea4ad..e84a5a255f8f 100644
--- a/math/lean4/files/patch-src_include_lean_lean.h
+++ b/math/lean4/files/patch-src_include_lean_lean.h
@@ -1,4 +1,4 @@
---- src/include/lean/lean.h.orig	2026-07-22 17:50:04 UTC
+--- src/include/lean/lean.h.orig	2026-10-12 15:51:15 UTC
 +++ src/include/lean/lean.h
 @@ -17,6 +17,10 @@ Author: Leonardo de Moura
  #include <lean/mimalloc.h>
@@ -11,7 +11,7 @@
  #ifdef __cplusplus
  #include <atomic>
  #include <stdlib.h>
-@@ -484,7 +488,15 @@ __attribute__((nothrow))
+@@ -570,7 +574,15 @@ __attribute__((nothrow))
  // `__attribute__((nothrow))` to be present or `noexcept`.
  __attribute__((nothrow))
  #endif
diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt
index 1b499230c8d4..ee8803d714cc 100644
--- a/math/lean4/files/patch-stage0_src_CMakeLists.txt
+++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt
@@ -48,6 +48,18 @@
  # 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}}")
+@@ -1036,8 +1052,9 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+     lean4lean
+     PREFIX lean4lean
+     EXCLUDE_FROM_ALL ON
+-    GIT_REPOSITORY https://github.com/Kha/lean4lean
+-    GIT_TAG lean4-bundle-4.35
++    SOURCE_DIR ${LEAN_SOURCE_DIR}/../ext/lean4lean
++    DOWNLOAD_COMMAND ""
++    UPDATE_COMMAND ""
+     PATCH_COMMAND bash ${LEAN_SOURCE_DIR}/../script/lean4lean-minimal-init.sh
+     CONFIGURE_COMMAND ""
+     BUILD_COMMAND lake build lean4lean
 @@ -1037,7 +1053,7 @@ install(
  
  install(
diff --git a/math/lean4/files/patch-tests_CMakeLists.txt b/math/lean4/files/patch-tests_CMakeLists.txt
index 9589cbd73125..900af248b241 100644
--- a/math/lean4/files/patch-tests_CMakeLists.txt
+++ b/math/lean4/files/patch-tests_CMakeLists.txt
@@ -7,11 +7,11 @@
 
 -- Disable the lint.py test because it calls git to find the list of tracked files to lint.
 
---- tests/CMakeLists.txt.orig	2026-08-21 10:26:01 UTC
+--- tests/CMakeLists.txt.orig	2026-10-12 15:51:15 UTC
 +++ tests/CMakeLists.txt
-@@ -21,6 +21,13 @@ endif()
- 
- set(LEAN_BIN "${MANGLED_BINARY_DIR}/bin")
+@@ -31,6 +31,13 @@ string(APPEND TEST_VARS " SCRIPT_DIR='${MANGLED_SOURCE
+ string(APPEND TEST_VARS " BUILD_DIR='${MANGLED_BINARY_DIR}'")
+ string(APPEND TEST_VARS " SCRIPT_DIR='${MANGLED_SOURCE_DIR}/../script'")
  
 +# FreeBSD: prepend test-bin (contains 'make' -> gmake symlink) to PATH so that tests
 +# using GNU make syntax (e.g. reverse-ffi) work correctly with FreeBSD's BSD make.
@@ -36,7 +36,7 @@
  set(WITH_TEST_ENV "${CMAKE_CURRENT_SOURCE_DIR}/with_stage${STAGE}_test_env.sh")
  set(WITH_BENCH_ENV "${CMAKE_CURRENT_SOURCE_DIR}/with_stage${STAGE}_bench_env.sh")
  
-@@ -309,7 +322,7 @@ endforeach(T)
+@@ -313,7 +326,7 @@ endforeach(T)
  endforeach(T)
  
  # Lint test suite and parts of the repository.
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 6b716149cbdf..f5f76934f812 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -2,6 +2,7 @@ bin/lake
 bin/lean
 bin/leanc
 bin/leanchecker
+bin/leanexport
 bin/leanir
 bin/leanmake
 include/lean/config.h
@@ -604,6 +605,12 @@ lib/lean/Init/Data/Dyadic/Round.ir.sig
 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/Erased.ilean
+lib/lean/Init/Data/Erased.ir
+lib/lean/Init/Data/Erased.ir.sig
+lib/lean/Init/Data/Erased.olean
+lib/lean/Init/Data/Erased.olean.private
+lib/lean/Init/Data/Erased.olean.server
 lib/lean/Init/Data/Fin.ilean
 lib/lean/Init/Data/Fin.ir
 lib/lean/Init/Data/Fin.ir.sig
@@ -646,12 +653,24 @@ lib/lean/Init/Data/Fin/Log2.ir.sig
 lib/lean/Init/Data/Fin/Log2.olean
 lib/lean/Init/Data/Fin/Log2.olean.private
 lib/lean/Init/Data/Fin/Log2.olean.server
+lib/lean/Init/Data/Fin/MinMax.ilean
+lib/lean/Init/Data/Fin/MinMax.ir
+lib/lean/Init/Data/Fin/MinMax.ir.sig
+lib/lean/Init/Data/Fin/MinMax.olean
+lib/lean/Init/Data/Fin/MinMax.olean.private
+lib/lean/Init/Data/Fin/MinMax.olean.server
 lib/lean/Init/Data/Fin/OverflowAware.ilean
 lib/lean/Init/Data/Fin/OverflowAware.ir
 lib/lean/Init/Data/Fin/OverflowAware.ir.sig
 lib/lean/Init/Data/Fin/OverflowAware.olean
 lib/lean/Init/Data/Fin/OverflowAware.olean.private
 lib/lean/Init/Data/Fin/OverflowAware.olean.server
+lib/lean/Init/Data/Fin/Package.ilean
+lib/lean/Init/Data/Fin/Package.ir
+lib/lean/Init/Data/Fin/Package.ir.sig
+lib/lean/Init/Data/Fin/Package.olean
+lib/lean/Init/Data/Fin/Package.olean.private
+lib/lean/Init/Data/Fin/Package.olean.server
 lib/lean/Init/Data/Float.ilean
 lib/lean/Init/Data/Float.ir
 lib/lean/Init/Data/Float.ir.sig
@@ -742,6 +761,12 @@ lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.ir.sig
 lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.olean
 lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.olean.private
 lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Fma.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Fma.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Fma.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Fma.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Fma.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Fma.olean.server
 lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.ilean
 lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.ir
 lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.ir.sig
@@ -982,6 +1007,12 @@ lib/lean/Init/Data/Int/Order.ir.sig
 lib/lean/Init/Data/Int/Order.olean
 lib/lean/Init/Data/Int/Order.olean.private
 lib/lean/Init/Data/Int/Order.olean.server
+lib/lean/Init/Data/Int/Package.ilean
+lib/lean/Init/Data/Int/Package.ir
+lib/lean/Init/Data/Int/Package.ir.sig
+lib/lean/Init/Data/Int/Package.olean
+lib/lean/Init/Data/Int/Package.olean.private
+lib/lean/Init/Data/Int/Package.olean.server
 lib/lean/Init/Data/Int/Pow.ilean
 lib/lean/Init/Data/Int/Pow.ir
 lib/lean/Init/Data/Int/Pow.ir.sig
@@ -1870,6 +1901,18 @@ lib/lean/Init/Data/Nat/Order.ir.sig
 lib/lean/Init/Data/Nat/Order.olean
 lib/lean/Init/Data/Nat/Order.olean.private
 lib/lean/Init/Data/Nat/Order.olean.server
+lib/lean/Init/Data/Nat/Package.ilean
+lib/lean/Init/Data/Nat/Package.ir
+lib/lean/Init/Data/Nat/Package.ir.sig
+lib/lean/Init/Data/Nat/Package.olean
+lib/lean/Init/Data/Nat/Package.olean.private
+lib/lean/Init/Data/Nat/Package.olean.server
+lib/lean/Init/Data/Nat/PowMod.ilean
+lib/lean/Init/Data/Nat/PowMod.ir
+lib/lean/Init/Data/Nat/PowMod.ir.sig
+lib/lean/Init/Data/Nat/PowMod.olean
+lib/lean/Init/Data/Nat/PowMod.olean.private
+lib/lean/Init/Data/Nat/PowMod.olean.server
 lib/lean/Init/Data/Nat/Power2.ilean
 lib/lean/Init/Data/Nat/Power2.ir
 lib/lean/Init/Data/Nat/Power2.ir.sig
@@ -2362,6 +2405,12 @@ lib/lean/Init/Data/SInt/Lemmas.ir.sig
 lib/lean/Init/Data/SInt/Lemmas.olean
 lib/lean/Init/Data/SInt/Lemmas.olean.private
 lib/lean/Init/Data/SInt/Lemmas.olean.server
+lib/lean/Init/Data/SInt/Package.ilean
+lib/lean/Init/Data/SInt/Package.ir
+lib/lean/Init/Data/SInt/Package.ir.sig
+lib/lean/Init/Data/SInt/Package.olean
+lib/lean/Init/Data/SInt/Package.olean.private
+lib/lean/Init/Data/SInt/Package.olean.server
 lib/lean/Init/Data/Slice.ilean
 lib/lean/Init/Data/Slice.ir
 lib/lean/Init/Data/Slice.ir.sig
@@ -2986,6 +3035,12 @@ lib/lean/Init/Data/UInt/Log2.ir.sig
 lib/lean/Init/Data/UInt/Log2.olean
 lib/lean/Init/Data/UInt/Log2.olean.private
 lib/lean/Init/Data/UInt/Log2.olean.server
+lib/lean/Init/Data/UInt/Package.ilean
+lib/lean/Init/Data/UInt/Package.ir
+lib/lean/Init/Data/UInt/Package.ir.sig
+lib/lean/Init/Data/UInt/Package.olean
+lib/lean/Init/Data/UInt/Package.olean.private
+lib/lean/Init/Data/UInt/Package.olean.server
 lib/lean/Init/Data/ULift.ilean
 lib/lean/Init/Data/ULift.ir
 lib/lean/Init/Data/ULift.ir.sig
@@ -3208,6 +3263,12 @@ lib/lean/Init/Grind/Homo/BitVec.ir.sig
 lib/lean/Init/Grind/Homo/BitVec.olean
 lib/lean/Init/Grind/Homo/BitVec.olean.private
 lib/lean/Init/Grind/Homo/BitVec.olean.server
+lib/lean/Init/Grind/Homo/Extra.ilean
+lib/lean/Init/Grind/Homo/Extra.ir
+lib/lean/Init/Grind/Homo/Extra.ir.sig
+lib/lean/Init/Grind/Homo/Extra.olean
+lib/lean/Init/Grind/Homo/Extra.olean.private
+lib/lean/Init/Grind/Homo/Extra.olean.server
 lib/lean/Init/Grind/Homo/Fin.ilean
 lib/lean/Init/Grind/Homo/Fin.ir
 lib/lean/Init/Grind/Homo/Fin.ir.sig
@@ -3220,12 +3281,6 @@ lib/lean/Init/Grind/Homo/ISize.ir.sig
 lib/lean/Init/Grind/Homo/ISize.olean
 lib/lean/Init/Grind/Homo/ISize.olean.private
 lib/lean/Init/Grind/Homo/ISize.olean.server
-lib/lean/Init/Grind/Homo/Int.ilean
-lib/lean/Init/Grind/Homo/Int.ir
-lib/lean/Init/Grind/Homo/Int.ir.sig
-lib/lean/Init/Grind/Homo/Int.olean
-lib/lean/Init/Grind/Homo/Int.olean.private
-lib/lean/Init/Grind/Homo/Int.olean.server
 lib/lean/Init/Grind/Homo/Int16.ilean
 lib/lean/Init/Grind/Homo/Int16.ir
 lib/lean/Init/Grind/Homo/Int16.ir.sig
@@ -3250,18 +3305,6 @@ lib/lean/Init/Grind/Homo/Int8.ir.sig
 lib/lean/Init/Grind/Homo/Int8.olean
 lib/lean/Init/Grind/Homo/Int8.olean.private
 lib/lean/Init/Grind/Homo/Int8.olean.server
-lib/lean/Init/Grind/Homo/List.ilean
-lib/lean/Init/Grind/Homo/List.ir
-lib/lean/Init/Grind/Homo/List.ir.sig
-lib/lean/Init/Grind/Homo/List.olean
-lib/lean/Init/Grind/Homo/List.olean.private
-lib/lean/Init/Grind/Homo/List.olean.server
-lib/lean/Init/Grind/Homo/Nat.ilean
-lib/lean/Init/Grind/Homo/Nat.ir
-lib/lean/Init/Grind/Homo/Nat.ir.sig
-lib/lean/Init/Grind/Homo/Nat.olean
-lib/lean/Init/Grind/Homo/Nat.olean.private
-lib/lean/Init/Grind/Homo/Nat.olean.server
 lib/lean/Init/Grind/Homo/UInt16.ilean
 lib/lean/Init/Grind/Homo/UInt16.ir
 lib/lean/Init/Grind/Homo/UInt16.ir.sig
@@ -3466,12 +3509,6 @@ lib/lean/Init/Grind/Ring/OfScientific.ir.sig
 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.ir.sig
-lib/lean/Init/Grind/Ring/ToInt.olean
-lib/lean/Init/Grind/Ring/ToInt.olean.private
-lib/lean/Init/Grind/Ring/ToInt.olean.server
 lib/lean/Init/Grind/Tactics.ilean
 lib/lean/Init/Grind/Tactics.ir
 lib/lean/Init/Grind/Tactics.ir.sig
@@ -3484,12 +3521,6 @@ lib/lean/Init/Grind/ToInt.ir.sig
 lib/lean/Init/Grind/ToInt.olean
 lib/lean/Init/Grind/ToInt.olean.private
 lib/lean/Init/Grind/ToInt.olean.server
-lib/lean/Init/Grind/ToIntLemmas.ilean
-lib/lean/Init/Grind/ToIntLemmas.ir
-lib/lean/Init/Grind/ToIntLemmas.ir.sig
-lib/lean/Init/Grind/ToIntLemmas.olean
-lib/lean/Init/Grind/ToIntLemmas.olean.private
-lib/lean/Init/Grind/ToIntLemmas.olean.server
 lib/lean/Init/Grind/Util.ilean
 lib/lean/Init/Grind/Util.ir
 lib/lean/Init/Grind/Util.ir.sig
@@ -3556,12 +3587,6 @@ lib/lean/Init/GrindInstances/Ring/UInt.ir.sig
 lib/lean/Init/GrindInstances/Ring/UInt.olean
 lib/lean/Init/GrindInstances/Ring/UInt.olean.private
 lib/lean/Init/GrindInstances/Ring/UInt.olean.server
-lib/lean/Init/GrindInstances/ToInt.ilean
-lib/lean/Init/GrindInstances/ToInt.ir
-lib/lean/Init/GrindInstances/ToInt.ir.sig
-lib/lean/Init/GrindInstances/ToInt.olean
-lib/lean/Init/GrindInstances/ToInt.olean.private
-lib/lean/Init/GrindInstances/ToInt.olean.server
 lib/lean/Init/Guard.ilean
 lib/lean/Init/Guard.ir
 lib/lean/Init/Guard.ir.sig
@@ -4126,6 +4151,12 @@ lib/lean/Lake/CLI/BuiltinLint.ir.sig
 lib/lean/Lake/CLI/BuiltinLint.olean
 lib/lean/Lake/CLI/BuiltinLint.olean.private
 lib/lean/Lake/CLI/BuiltinLint.olean.server
+lib/lean/Lake/CLI/Check.ilean
+lib/lean/Lake/CLI/Check.ir
+lib/lean/Lake/CLI/Check.ir.sig
+lib/lean/Lake/CLI/Check.olean
+lib/lean/Lake/CLI/Check.olean.private
+lib/lean/Lake/CLI/Check.olean.server
 lib/lean/Lake/CLI/Error.ilean
 lib/lean/Lake/CLI/Error.ir
 lib/lean/Lake/CLI/Error.ir.sig
@@ -4180,6 +4211,24 @@ lib/lean/Lake/CLI/Translate/Toml.ir.sig
 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/Check/Axioms.ilean
+lib/lean/Lake/Check/Axioms.ir
+lib/lean/Lake/Check/Axioms.ir.sig
+lib/lean/Lake/Check/Axioms.olean
+lib/lean/Lake/Check/Axioms.olean.private
+lib/lean/Lake/Check/Axioms.olean.server
+lib/lean/Lake/Check/Compare.ilean
+lib/lean/Lake/Check/Compare.ir
+lib/lean/Lake/Check/Compare.ir.sig
+lib/lean/Lake/Check/Compare.olean
+lib/lean/Lake/Check/Compare.olean.private
+lib/lean/Lake/Check/Compare.olean.server
+lib/lean/Lake/Check/Util.ilean
+lib/lean/Lake/Check/Util.ir
+lib/lean/Lake/Check/Util.ir.sig
+lib/lean/Lake/Check/Util.olean
+lib/lean/Lake/Check/Util.olean.private
+lib/lean/Lake/Check/Util.olean.server
 lib/lean/Lake/Config.ilean
 lib/lean/Lake/Config.ir
 lib/lean/Lake/Config.ir.sig
@@ -6682,6 +6731,12 @@ lib/lean/Lean/Elab/InfoTree/Types.ir.sig
 lib/lean/Lean/Elab/InfoTree/Types.olean
 lib/lean/Lean/Elab/InfoTree/Types.olean.private
 lib/lean/Lean/Elab/InfoTree/Types.olean.server
+lib/lean/Lean/Elab/InfoTree/Util.ilean
+lib/lean/Lean/Elab/InfoTree/Util.ir
+lib/lean/Lean/Elab/InfoTree/Util.ir.sig
+lib/lean/Lean/Elab/InfoTree/Util.olean
+lib/lean/Lean/Elab/InfoTree/Util.olean.private
+lib/lean/Lean/Elab/InfoTree/Util.olean.server
 lib/lean/Lean/Elab/InfoTrees.ilean
 lib/lean/Lean/Elab/InfoTrees.ir
 lib/lean/Lean/Elab/InfoTrees.ir.sig
@@ -7042,6 +7097,12 @@ lib/lean/Lean/Elab/RecAppSyntax.ir.sig
 lib/lean/Lean/Elab/RecAppSyntax.olean
 lib/lean/Lean/Elab/RecAppSyntax.olean.private
 lib/lean/Lean/Elab/RecAppSyntax.olean.server
+lib/lean/Lean/Elab/Recall.ilean
+lib/lean/Lean/Elab/Recall.ir
+lib/lean/Lean/Elab/Recall.ir.sig
+lib/lean/Lean/Elab/Recall.olean
+lib/lean/Lean/Elab/Recall.olean.private
+lib/lean/Lean/Elab/Recall.olean.server
 lib/lean/Lean/Elab/RecommendedSpelling.ilean
 lib/lean/Lean/Elab/RecommendedSpelling.ir
 lib/lean/Lean/Elab/RecommendedSpelling.ir.sig
@@ -7276,108 +7337,6 @@ lib/lean/Lean/Elab/Tactic/Do/Contract.ir.sig
 lib/lean/Lean/Elab/Tactic/Do/Contract.olean
 lib/lean/Lean/Elab/Tactic/Do/Contract.olean.private
 lib/lean/Lean/Elab/Tactic/Do/Contract.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProc.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProc.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProc.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProc.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProc.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProc.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProcAttr.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProcAttr.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProcAttr.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProcAttr.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProcAttr.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProcAttr.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/LatticeOp.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/LatticeOp.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/LatticeOp.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/LatticeOp.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/LatticeOp.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/LatticeOp.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Util.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Util.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Util.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Util.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Util.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Util.olean.server
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.ilean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.ir
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.ir.sig
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.olean
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.olean.private
-lib/lean/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.olean.server
 lib/lean/Lean/Elab/Tactic/Do/LetElim.ilean
 lib/lean/Lean/Elab/Tactic/Do/LetElim.ir
 lib/lean/Lean/Elab/Tactic/Do/LetElim.ir.sig
@@ -7654,6 +7613,18 @@ lib/lean/Lean/Elab/Tactic/Grind/Have.ir.sig
 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/LetToHave.ilean
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.ir
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.ir.sig
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.olean
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/LiftLet.ilean
+lib/lean/Lean/Elab/Tactic/Grind/LiftLet.ir
+lib/lean/Lean/Elab/Tactic/Grind/LiftLet.ir.sig
+lib/lean/Lean/Elab/Tactic/Grind/LiftLet.olean
+lib/lean/Lean/Elab/Tactic/Grind/LiftLet.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/LiftLet.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.ir.sig
@@ -7864,6 +7835,12 @@ lib/lean/Lean/Elab/Tactic/Rfl.ir.sig
 lib/lean/Lean/Elab/Tactic/Rfl.olean
 lib/lean/Lean/Elab/Tactic/Rfl.olean.private
 lib/lean/Lean/Elab/Tactic/Rfl.olean.server
+lib/lean/Lean/Elab/Tactic/Rwa.ilean
+lib/lean/Lean/Elab/Tactic/Rwa.ir
+lib/lean/Lean/Elab/Tactic/Rwa.ir.sig
+lib/lean/Lean/Elab/Tactic/Rwa.olean
+lib/lean/Lean/Elab/Tactic/Rwa.olean.private
+lib/lean/Lean/Elab/Tactic/Rwa.olean.server
 lib/lean/Lean/Elab/Tactic/Show.ilean
 lib/lean/Lean/Elab/Tactic/Show.ir
 lib/lean/Lean/Elab/Tactic/Show.ir.sig
@@ -7942,6 +7919,102 @@ lib/lean/Lean/Elab/Tactic/Unfold.ir.sig
 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/Tactic/VCGen.ilean
+lib/lean/Lean/Elab/Tactic/VCGen.ir
+lib/lean/Lean/Elab/Tactic/VCGen.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen.olean
+lib/lean/Lean/Elab/Tactic/VCGen.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.ir
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.olean
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/Context.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/Context.ir
+lib/lean/Lean/Elab/Tactic/VCGen/Context.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/Context.olean
+lib/lean/Lean/Elab/Tactic/VCGen/Context.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/Context.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/Driver.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/Driver.ir
+lib/lean/Lean/Elab/Tactic/VCGen/Driver.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/Driver.olean
+lib/lean/Lean/Elab/Tactic/VCGen/Driver.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/Driver.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/Entails.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/Entails.ir
+lib/lean/Lean/Elab/Tactic/VCGen/Entails.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/Entails.olean
+lib/lean/Lean/Elab/Tactic/VCGen/Entails.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/Entails.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProc.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProc.ir
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProc.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProc.olean
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProc.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProc.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.ir
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.olean
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/Frontend.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/Frontend.ir
+lib/lean/Lean/Elab/Tactic/VCGen/Frontend.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/Frontend.olean
+lib/lean/Lean/Elab/Tactic/VCGen/Frontend.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/Frontend.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/LatticeOp.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/LatticeOp.ir
+lib/lean/Lean/Elab/Tactic/VCGen/LatticeOp.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/LatticeOp.olean
+lib/lean/Lean/Elab/Tactic/VCGen/LatticeOp.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/LatticeOp.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/Reduce.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/Reduce.ir
+lib/lean/Lean/Elab/Tactic/VCGen/Reduce.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/Reduce.olean
+lib/lean/Lean/Elab/Tactic/VCGen/Reduce.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/Reduce.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/RuleCache.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/RuleCache.ir
+lib/lean/Lean/Elab/Tactic/VCGen/RuleCache.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/RuleCache.olean
+lib/lean/Lean/Elab/Tactic/VCGen/RuleCache.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/RuleCache.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/RuleConstruction.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/RuleConstruction.ir
+lib/lean/Lean/Elab/Tactic/VCGen/RuleConstruction.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/RuleConstruction.olean
+lib/lean/Lean/Elab/Tactic/VCGen/RuleConstruction.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/RuleConstruction.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/Solve.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/Solve.ir
+lib/lean/Lean/Elab/Tactic/VCGen/Solve.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/Solve.olean
+lib/lean/Lean/Elab/Tactic/VCGen/Solve.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/Solve.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/SpecDB.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/SpecDB.ir
+lib/lean/Lean/Elab/Tactic/VCGen/SpecDB.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/SpecDB.olean
+lib/lean/Lean/Elab/Tactic/VCGen/SpecDB.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/SpecDB.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/Util.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/Util.ir
+lib/lean/Lean/Elab/Tactic/VCGen/Util.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/Util.olean
+lib/lean/Lean/Elab/Tactic/VCGen/Util.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/Util.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/WPApp.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/WPApp.ir
+lib/lean/Lean/Elab/Tactic/VCGen/WPApp.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/WPApp.olean
+lib/lean/Lean/Elab/Tactic/VCGen/WPApp.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/WPApp.olean.server
 lib/lean/Lean/Elab/Task.ilean
 lib/lean/Lean/Elab/Task.ir
 lib/lean/Lean/Elab/Task.ir.sig
@@ -8074,6 +8147,12 @@ lib/lean/Lean/Language/Lean/Types.ir.sig
 lib/lean/Lean/Language/Lean/Types.olean
 lib/lean/Lean/Language/Lean/Types.olean.private
 lib/lean/Lean/Language/Lean/Types.olean.server
+lib/lean/Lean/Language/Lean/Util.ilean
+lib/lean/Lean/Language/Lean/Util.ir
+lib/lean/Lean/Language/Lean/Util.ir.sig
+lib/lean/Lean/Language/Lean/Util.olean
+lib/lean/Lean/Language/Lean/Util.olean.private
+lib/lean/Lean/Language/Lean/Util.olean.server
 lib/lean/Lean/Language/Util.ilean
 lib/lean/Lean/Language/Util.ir
 lib/lean/Lean/Language/Util.ir.sig
@@ -9238,6 +9317,18 @@ lib/lean/Lean/Meta/Sym/IsClass.ir.sig
 lib/lean/Lean/Meta/Sym/IsClass.olean
 lib/lean/Lean/Meta/Sym/IsClass.olean.private
 lib/lean/Lean/Meta/Sym/IsClass.olean.server
+lib/lean/Lean/Meta/Sym/LetToHave.ilean
+lib/lean/Lean/Meta/Sym/LetToHave.ir
+lib/lean/Lean/Meta/Sym/LetToHave.ir.sig
+lib/lean/Lean/Meta/Sym/LetToHave.olean
+lib/lean/Lean/Meta/Sym/LetToHave.olean.private
+lib/lean/Lean/Meta/Sym/LetToHave.olean.server
+lib/lean/Lean/Meta/Sym/LiftLet.ilean
+lib/lean/Lean/Meta/Sym/LiftLet.ir
+lib/lean/Lean/Meta/Sym/LiftLet.ir.sig
+lib/lean/Lean/Meta/Sym/LiftLet.olean
+lib/lean/Lean/Meta/Sym/LiftLet.olean.private
+lib/lean/Lean/Meta/Sym/LiftLet.olean.server
 lib/lean/Lean/Meta/Sym/LitValues.ilean
 lib/lean/Lean/Meta/Sym/LitValues.ir
 lib/lean/Lean/Meta/Sym/LitValues.ir.sig
@@ -10180,18 +10271,6 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.ir.sig
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.olean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.ir.sig
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.olean.server
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.ilean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.ir
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.ir.sig
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.olean
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.olean.private
-lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.ir
 lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.ir.sig
@@ -10426,6 +10505,18 @@ lib/lean/Lean/Meta/Tactic/Grind/Attr.ir.sig
 lib/lean/Lean/Meta/Tactic/Grind/Attr.olean
 lib/lean/Lean/Meta/Tactic/Grind/Attr.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Attr.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide.ilean
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide.ir
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide.ir.sig
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide.olean
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide/Types.ilean
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide/Types.ir
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide/Types.ir.sig
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide/Types.olean
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide/Types.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/BVDecide/Types.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/Beta.ilean
 lib/lean/Lean/Meta/Tactic/Grind/Beta.ir
 lib/lean/Lean/Meta/Tactic/Grind/Beta.ir.sig
@@ -10504,6 +10595,12 @@ lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.ir.sig
 lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.olean
 lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/EMatchAction.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/EMatchDiagnostics.ilean
+lib/lean/Lean/Meta/Tactic/Grind/EMatchDiagnostics.ir
+lib/lean/Lean/Meta/Tactic/Grind/EMatchDiagnostics.ir.sig
+lib/lean/Lean/Meta/Tactic/Grind/EMatchDiagnostics.olean
+lib/lean/Lean/Meta/Tactic/Grind/EMatchDiagnostics.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/EMatchDiagnostics.olean.server
 lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.ilean
 lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.ir
 lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.ir.sig
@@ -10570,6 +10667,12 @@ lib/lean/Lean/Meta/Tactic/Grind/Homo.ir.sig
 lib/lean/Lean/Meta/Tactic/Grind/Homo.olean
 lib/lean/Lean/Meta/Tactic/Grind/Homo.olean.private
 lib/lean/Lean/Meta/Tactic/Grind/Homo.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Homomorphism.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Homomorphism.ir
+lib/lean/Lean/Meta/Tactic/Grind/Homomorphism.ir.sig
+lib/lean/Lean/Meta/Tactic/Grind/Homomorphism.olean
+lib/lean/Lean/Meta/Tactic/Grind/Homomorphism.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Homomorphism.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.ir.sig
@@ -12180,6 +12283,26 @@ lib/lean/Lean/Widget/UserWidget.olean.private
 lib/lean/Lean/Widget/UserWidget.olean.server
 lib/lean/LeanChecker.ilean
 lib/lean/LeanChecker.olean
+lib/lean/LeanExport.ilean
+lib/lean/LeanExport.olean
+lib/lean/LeanExport/Basic.ilean
+lib/lean/LeanExport/Basic.ir
+lib/lean/LeanExport/Basic.ir.sig
+lib/lean/LeanExport/Basic.olean
+lib/lean/LeanExport/Basic.olean.private
+lib/lean/LeanExport/Basic.olean.server
+lib/lean/LeanExport/Json.ilean
+lib/lean/LeanExport/Json.ir
+lib/lean/LeanExport/Json.ir.sig
+lib/lean/LeanExport/Json.olean
+lib/lean/LeanExport/Json.olean.private
+lib/lean/LeanExport/Json.olean.server
+lib/lean/LeanExport/Parse.ilean
+lib/lean/LeanExport/Parse.ir
+lib/lean/LeanExport/Parse.ir.sig
+lib/lean/LeanExport/Parse.olean
+lib/lean/LeanExport/Parse.olean.private
+lib/lean/LeanExport/Parse.olean.server
 lib/lean/LeanIR.ilean
 lib/lean/LeanIR.ir
 lib/lean/LeanIR.ir.sig
@@ -13814,120 +13937,6 @@ lib/lean/Std/Internal.ir.sig
 lib/lean/Std/Internal.olean
 lib/lean/Std/Internal.olean.private
 lib/lean/Std/Internal.olean.server
-lib/lean/Std/Internal/Do.ilean
-lib/lean/Std/Internal/Do.ir
-lib/lean/Std/Internal/Do.ir.sig
-lib/lean/Std/Internal/Do.olean
-lib/lean/Std/Internal/Do.olean.private
-lib/lean/Std/Internal/Do.olean.server
-lib/lean/Std/Internal/Do/Assertion.ilean
-lib/lean/Std/Internal/Do/Assertion.ir
-lib/lean/Std/Internal/Do/Assertion.ir.sig
-lib/lean/Std/Internal/Do/Assertion.olean
-lib/lean/Std/Internal/Do/Assertion.olean.private
-lib/lean/Std/Internal/Do/Assertion.olean.server
-lib/lean/Std/Internal/Do/ExceptPost.ilean
-lib/lean/Std/Internal/Do/ExceptPost.ir
-lib/lean/Std/Internal/Do/ExceptPost.ir.sig
-lib/lean/Std/Internal/Do/ExceptPost.olean
-lib/lean/Std/Internal/Do/ExceptPost.olean.private
-lib/lean/Std/Internal/Do/ExceptPost.olean.server
-lib/lean/Std/Internal/Do/Gadget/ForIn.ilean
-lib/lean/Std/Internal/Do/Gadget/ForIn.ir
-lib/lean/Std/Internal/Do/Gadget/ForIn.ir.sig
-lib/lean/Std/Internal/Do/Gadget/ForIn.olean
-lib/lean/Std/Internal/Do/Gadget/ForIn.olean.private
-lib/lean/Std/Internal/Do/Gadget/ForIn.olean.server
-lib/lean/Std/Internal/Do/Order/Basic.ilean
-lib/lean/Std/Internal/Do/Order/Basic.ir
-lib/lean/Std/Internal/Do/Order/Basic.ir.sig
-lib/lean/Std/Internal/Do/Order/Basic.olean
-lib/lean/Std/Internal/Do/Order/Basic.olean.private
-lib/lean/Std/Internal/Do/Order/Basic.olean.server
-lib/lean/Std/Internal/Do/Order/Heyting.ilean
-lib/lean/Std/Internal/Do/Order/Heyting.ir
-lib/lean/Std/Internal/Do/Order/Heyting.ir.sig
-lib/lean/Std/Internal/Do/Order/Heyting.olean
-lib/lean/Std/Internal/Do/Order/Heyting.olean.private
-lib/lean/Std/Internal/Do/Order/Heyting.olean.server
-lib/lean/Std/Internal/Do/Order/Instances.ilean
-lib/lean/Std/Internal/Do/Order/Instances.ir
-lib/lean/Std/Internal/Do/Order/Instances.ir.sig
-lib/lean/Std/Internal/Do/Order/Instances.olean
-lib/lean/Std/Internal/Do/Order/Instances.olean.private
-lib/lean/Std/Internal/Do/Order/Instances.olean.server
-lib/lean/Std/Internal/Do/Order/Lemmas.ilean
-lib/lean/Std/Internal/Do/Order/Lemmas.ir
-lib/lean/Std/Internal/Do/Order/Lemmas.ir.sig
-lib/lean/Std/Internal/Do/Order/Lemmas.olean
-lib/lean/Std/Internal/Do/Order/Lemmas.olean.private
-lib/lean/Std/Internal/Do/Order/Lemmas.olean.server
-lib/lean/Std/Internal/Do/Order/PreservesSup.ilean
-lib/lean/Std/Internal/Do/Order/PreservesSup.ir
-lib/lean/Std/Internal/Do/Order/PreservesSup.ir.sig
-lib/lean/Std/Internal/Do/Order/PreservesSup.olean
-lib/lean/Std/Internal/Do/Order/PreservesSup.olean.private
-lib/lean/Std/Internal/Do/Order/PreservesSup.olean.server
-lib/lean/Std/Internal/Do/PredTrans.ilean
-lib/lean/Std/Internal/Do/PredTrans.ir
-lib/lean/Std/Internal/Do/PredTrans.ir.sig
-lib/lean/Std/Internal/Do/PredTrans.olean
-lib/lean/Std/Internal/Do/PredTrans.olean.private
-lib/lean/Std/Internal/Do/PredTrans.olean.server
-lib/lean/Std/Internal/Do/Triple.ilean
-lib/lean/Std/Internal/Do/Triple.ir
-lib/lean/Std/Internal/Do/Triple.ir.sig
-lib/lean/Std/Internal/Do/Triple.olean
-lib/lean/Std/Internal/Do/Triple.olean.private
-lib/lean/Std/Internal/Do/Triple.olean.server
-lib/lean/Std/Internal/Do/Triple/Basic.ilean
-lib/lean/Std/Internal/Do/Triple/Basic.ir
-lib/lean/Std/Internal/Do/Triple/Basic.ir.sig
-lib/lean/Std/Internal/Do/Triple/Basic.olean
-lib/lean/Std/Internal/Do/Triple/Basic.olean.private
-lib/lean/Std/Internal/Do/Triple/Basic.olean.server
-lib/lean/Std/Internal/Do/Triple/Gadget.ilean
-lib/lean/Std/Internal/Do/Triple/Gadget.ir
-lib/lean/Std/Internal/Do/Triple/Gadget.ir.sig
-lib/lean/Std/Internal/Do/Triple/Gadget.olean
-lib/lean/Std/Internal/Do/Triple/Gadget.olean.private
-lib/lean/Std/Internal/Do/Triple/Gadget.olean.server
-lib/lean/Std/Internal/Do/Triple/SpecLemmas.ilean
-lib/lean/Std/Internal/Do/Triple/SpecLemmas.ir
-lib/lean/Std/Internal/Do/Triple/SpecLemmas.ir.sig
-lib/lean/Std/Internal/Do/Triple/SpecLemmas.olean
-lib/lean/Std/Internal/Do/Triple/SpecLemmas.olean.private
-lib/lean/Std/Internal/Do/Triple/SpecLemmas.olean.server
-lib/lean/Std/Internal/Do/WP.ilean
-lib/lean/Std/Internal/Do/WP.ir
-lib/lean/Std/Internal/Do/WP.ir.sig
-lib/lean/Std/Internal/Do/WP.olean
-lib/lean/Std/Internal/Do/WP.olean.private
-lib/lean/Std/Internal/Do/WP.olean.server
-lib/lean/Std/Internal/Do/WP/Basic.ilean
-lib/lean/Std/Internal/Do/WP/Basic.ir
-lib/lean/Std/Internal/Do/WP/Basic.ir.sig
-lib/lean/Std/Internal/Do/WP/Basic.olean
-lib/lean/Std/Internal/Do/WP/Basic.olean.private
-lib/lean/Std/Internal/Do/WP/Basic.olean.server
-lib/lean/Std/Internal/Do/WP/Conjunctive.ilean
-lib/lean/Std/Internal/Do/WP/Conjunctive.ir
-lib/lean/Std/Internal/Do/WP/Conjunctive.ir.sig
-lib/lean/Std/Internal/Do/WP/Conjunctive.olean
-lib/lean/Std/Internal/Do/WP/Conjunctive.olean.private
-lib/lean/Std/Internal/Do/WP/Conjunctive.olean.server
-lib/lean/Std/Internal/Do/WP/Frame.ilean
-lib/lean/Std/Internal/Do/WP/Frame.ir
-lib/lean/Std/Internal/Do/WP/Frame.ir.sig
-lib/lean/Std/Internal/Do/WP/Frame.olean
-lib/lean/Std/Internal/Do/WP/Frame.olean.private
-lib/lean/Std/Internal/Do/WP/Frame.olean.server
-lib/lean/Std/Internal/Do/WP/Lemmas.ilean
-lib/lean/Std/Internal/Do/WP/Lemmas.ir
-lib/lean/Std/Internal/Do/WP/Lemmas.ir.sig
-lib/lean/Std/Internal/Do/WP/Lemmas.olean
-lib/lean/Std/Internal/Do/WP/Lemmas.olean.private
*** 801 LINES SKIPPED ***