git: fec276899d15 - main - math/lean4: update 4.11.0 → 4.12.0

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Thu, 03 Oct 2024 09:17:21 UTC
The branch main has been updated by yuri:

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

commit fec276899d1509867529356a07505ae01015d7de
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2024-10-03 07:21:40 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2024-10-03 09:17:09 +0000

    math/lean4: update 4.11.0 → 4.12.0
---
 math/lean4/Makefile  |  12 +-
 math/lean4/distinfo  |   6 +-
 math/lean4/pkg-plist | 453 ++++++++++++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 458 insertions(+), 13 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index aa4a44690ce8..3e7cfb67dfd9 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,7 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.11.0
-PORTREVISION=	1
+DISTVERSION=	4.12.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
@@ -14,8 +13,11 @@ LICENSE_FILE=	${WRKSRC}/LICENSE
 BROKEN_armv7=	compilation fails: ../../.build/stage1/lib/temp/Init/Coe.depend: No such file or directory
 BROKEN_i386=	linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter)
 
-BUILD_DEPENDS=	bash:shells/bash
-LIB_DEPENDS=	libgmp.so:math/gmp
+BUILD_DEPENDS=	bash:shells/bash \
+		cadical:math/cadical
+LIB_DEPENDS=	libgmp.so:math/gmp \
+		libuv.so:devel/libuv
+RUN_DEPENDS=	cadical:math/cadical
 
 USES=		cmake:noninja,testing compiler:c++14-lang gmake python:build # ninja fails + gmake scripts are included in the project
 
@@ -43,6 +45,8 @@ post-install:
 	@${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete
 	# remove stray files
 	@${RM} ${STAGEDIR}${PREFIX}/LICENSE*
+	# remove bin/cadical, workaround for https://github.com/leanprover/lean4/issues/5603
+	@${RM} ${STAGEDIR}${PREFIX}/bin/cadical
 	# strip binaries
 	@cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \
 		bin/lake \
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index fd56f3893df9..d2357b8b5f44 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1725254182
-SHA256 (leanprover-lean4-v4.11.0_GH0.tar.gz) = 8b7fc8e71e107250c7bbf911eb1f450379d874857a26236577aaa624dd5962b5
-SIZE (leanprover-lean4-v4.11.0_GH0.tar.gz) = 25790812
+TIMESTAMP = 1727897287
+SHA256 (leanprover-lean4-v4.12.0_GH0.tar.gz) = 409f623eb9044b3b025951415dfa0db531ed29056a5fba5d556394ad9435e62b
+SIZE (leanprover-lean4-v4.12.0_GH0.tar.gz) = 27334919
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 365f371356e4..8093484c1e97 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -5,6 +5,7 @@ bin/leanmake
 include/lean/config.h
 include/lean/lean.h
 include/lean/lean_gmp.h
+include/lean/lean_libuv.h
 include/lean/version.h
 lib/lean/Init.ilean
 lib/lean/Init.olean
@@ -156,6 +157,8 @@ lib/lean/Init/Data/Int/Gcd.ilean
 lib/lean/Init/Data/Int/Gcd.olean
 lib/lean/Init/Data/Int/Lemmas.ilean
 lib/lean/Init/Data/Int/Lemmas.olean
+lib/lean/Init/Data/Int/LemmasAux.ilean
+lib/lean/Init/Data/Int/LemmasAux.olean
 lib/lean/Init/Data/Int/Order.ilean
 lib/lean/Init/Data/Int/Order.olean
 lib/lean/Init/Data/Int/Pow.ilean
@@ -192,12 +195,26 @@ lib/lean/Init/Data/List/Nat/Pairwise.ilean
 lib/lean/Init/Data/List/Nat/Pairwise.olean
 lib/lean/Init/Data/List/Nat/Range.ilean
 lib/lean/Init/Data/List/Nat/Range.olean
+lib/lean/Init/Data/List/Nat/Sublist.ilean
+lib/lean/Init/Data/List/Nat/Sublist.olean
 lib/lean/Init/Data/List/Nat/TakeDrop.ilean
 lib/lean/Init/Data/List/Nat/TakeDrop.olean
 lib/lean/Init/Data/List/Notation.ilean
 lib/lean/Init/Data/List/Notation.olean
 lib/lean/Init/Data/List/Pairwise.ilean
 lib/lean/Init/Data/List/Pairwise.olean
+lib/lean/Init/Data/List/Perm.ilean
+lib/lean/Init/Data/List/Perm.olean
+lib/lean/Init/Data/List/Range.ilean
+lib/lean/Init/Data/List/Range.olean
+lib/lean/Init/Data/List/Sort.ilean
+lib/lean/Init/Data/List/Sort.olean
+lib/lean/Init/Data/List/Sort/Basic.ilean
+lib/lean/Init/Data/List/Sort/Basic.olean
+lib/lean/Init/Data/List/Sort/Impl.ilean
+lib/lean/Init/Data/List/Sort/Impl.olean
+lib/lean/Init/Data/List/Sort/Lemmas.ilean
+lib/lean/Init/Data/List/Sort/Lemmas.olean
 lib/lean/Init/Data/List/Sublist.ilean
 lib/lean/Init/Data/List/Sublist.olean
 lib/lean/Init/Data/List/TakeDrop.ilean
@@ -256,6 +273,8 @@ lib/lean/Init/Data/Option/Lemmas.ilean
 lib/lean/Init/Data/Option/Lemmas.olean
 lib/lean/Init/Data/Ord.ilean
 lib/lean/Init/Data/Ord.olean
+lib/lean/Init/Data/PLift.ilean
+lib/lean/Init/Data/PLift.olean
 lib/lean/Init/Data/Prod.ilean
 lib/lean/Init/Data/Prod.olean
 lib/lean/Init/Data/Queue.ilean
@@ -296,6 +315,8 @@ lib/lean/Init/Data/UInt/Lemmas.ilean
 lib/lean/Init/Data/UInt/Lemmas.olean
 lib/lean/Init/Data/UInt/Log2.ilean
 lib/lean/Init/Data/UInt/Log2.olean
+lib/lean/Init/Data/ULift.ilean
+lib/lean/Init/Data/ULift.olean
 lib/lean/Init/Dynamic.ilean
 lib/lean/Init/Dynamic.olean
 lib/lean/Init/Ext.ilean
@@ -946,8 +967,6 @@ lib/lean/Lean/Data/OpenDecl.ilean
 lib/lean/Lean/Data/OpenDecl.olean
 lib/lean/Lean/Data/Options.ilean
 lib/lean/Lean/Data/Options.olean
-lib/lean/Lean/Data/Parsec.ilean
-lib/lean/Lean/Data/Parsec.olean
 lib/lean/Lean/Data/PersistentArray.ilean
 lib/lean/Lean/Data/PersistentArray.olean
 lib/lean/Lean/Data/PersistentHashMap.ilean
@@ -1116,12 +1135,16 @@ lib/lean/Lean/Elab/PreDefinition.ilean
 lib/lean/Lean/Elab/PreDefinition.olean
 lib/lean/Lean/Elab/PreDefinition/Basic.ilean
 lib/lean/Lean/Elab/PreDefinition/Basic.olean
+lib/lean/Lean/Elab/PreDefinition/EqUnfold.ilean
+lib/lean/Lean/Elab/PreDefinition/EqUnfold.olean
 lib/lean/Lean/Elab/PreDefinition/Eqns.ilean
 lib/lean/Lean/Elab/PreDefinition/Eqns.olean
 lib/lean/Lean/Elab/PreDefinition/Main.ilean
 lib/lean/Lean/Elab/PreDefinition/Main.olean
 lib/lean/Lean/Elab/PreDefinition/MkInhabitant.ilean
 lib/lean/Lean/Elab/PreDefinition/MkInhabitant.olean
+lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.ilean
+lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.olean
 lib/lean/Lean/Elab/PreDefinition/Structural.ilean
 lib/lean/Lean/Elab/PreDefinition/Structural.olean
 lib/lean/Lean/Elab/PreDefinition/Structural/BRecOn.ilean
@@ -1150,6 +1173,8 @@ lib/lean/Lean/Elab/PreDefinition/TerminationHint.ilean
 lib/lean/Lean/Elab/PreDefinition/TerminationHint.olean
 lib/lean/Lean/Elab/PreDefinition/WF.ilean
 lib/lean/Lean/Elab/PreDefinition/WF.olean
+lib/lean/Lean/Elab/PreDefinition/WF/Basic.ilean
+lib/lean/Lean/Elab/PreDefinition/WF/Basic.olean
 lib/lean/Lean/Elab/PreDefinition/WF/Eqns.ilean
 lib/lean/Lean/Elab/PreDefinition/WF/Eqns.olean
 lib/lean/Lean/Elab/PreDefinition/WF/Fix.ilean
@@ -1188,8 +1213,42 @@ lib/lean/Lean/Elab/SyntheticMVars.ilean
 lib/lean/Lean/Elab/SyntheticMVars.olean
 lib/lean/Lean/Elab/Tactic.ilean
 lib/lean/Lean/Elab/Tactic.olean
+lib/lean/Lean/Elab/Tactic/BVDecide.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/External.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/External.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Attr.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Attr.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/LRAT.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/LRAT.olean
+lib/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.ilean
+lib/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.olean
 lib/lean/Lean/Elab/Tactic/Basic.ilean
 lib/lean/Lean/Elab/Tactic/Basic.olean
+lib/lean/Lean/Elab/Tactic/BoolToPropSimps.ilean
+lib/lean/Lean/Elab/Tactic/BoolToPropSimps.olean
 lib/lean/Lean/Elab/Tactic/BuiltinTactic.ilean
 lib/lean/Lean/Elab/Tactic/BuiltinTactic.olean
 lib/lean/Lean/Elab/Tactic/Cache.ilean
@@ -1290,6 +1349,8 @@ lib/lean/Lean/Elab/Tactic/Unfold.ilean
 lib/lean/Lean/Elab/Tactic/Unfold.olean
 lib/lean/Lean/Elab/Term.ilean
 lib/lean/Lean/Elab/Term.olean
+lib/lean/Lean/Elab/Time.ilean
+lib/lean/Lean/Elab/Time.olean
 lib/lean/Lean/Elab/Util.ilean
 lib/lean/Lean/Elab/Util.olean
 lib/lean/Lean/Environment.ilean
@@ -1852,6 +1913,8 @@ lib/lean/Lean/Util/MonadBacktrack.ilean
 lib/lean/Lean/Util/MonadBacktrack.olean
 lib/lean/Lean/Util/MonadCache.ilean
 lib/lean/Lean/Util/MonadCache.olean
+lib/lean/Lean/Util/NumApps.ilean
+lib/lean/Lean/Util/NumApps.olean
 lib/lean/Lean/Util/NumObjs.ilean
 lib/lean/Lean/Util/NumObjs.olean
 lib/lean/Lean/Util/OccursCheck.ilean
@@ -1934,8 +1997,6 @@ lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.ilean
 lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.olean
 lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.ilean
 lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.olean
-lib/lean/Std/Data/DHashMap/Internal/List/Perm.ilean
-lib/lean/Std/Data/DHashMap/Internal/List/Perm.olean
 lib/lean/Std/Data/DHashMap/Internal/List/Sublist.ilean
 lib/lean/Std/Data/DHashMap/Internal/List/Sublist.olean
 lib/lean/Std/Data/DHashMap/Internal/Model.ilean
@@ -1976,14 +2037,246 @@ lib/lean/Std/Data/HashSet/Raw.ilean
 lib/lean/Std/Data/HashSet/Raw.olean
 lib/lean/Std/Data/HashSet/RawLemmas.ilean
 lib/lean/Std/Data/HashSet/RawLemmas.olean
+lib/lean/Std/Internal.ilean
+lib/lean/Std/Internal.olean
+lib/lean/Std/Internal/Parsec.ilean
+lib/lean/Std/Internal/Parsec.olean
+lib/lean/Std/Internal/Parsec/Basic.ilean
+lib/lean/Std/Internal/Parsec/Basic.olean
+lib/lean/Std/Internal/Parsec/ByteArray.ilean
+lib/lean/Std/Internal/Parsec/ByteArray.olean
+lib/lean/Std/Internal/Parsec/String.ilean
+lib/lean/Std/Internal/Parsec/String.olean
+lib/lean/Std/Sat.ilean
+lib/lean/Std/Sat.olean
+lib/lean/Std/Sat/AIG.ilean
+lib/lean/Std/Sat/AIG.olean
+lib/lean/Std/Sat/AIG/Basic.ilean
+lib/lean/Std/Sat/AIG/Basic.olean
+lib/lean/Std/Sat/AIG/CNF.ilean
+lib/lean/Std/Sat/AIG/CNF.olean
+lib/lean/Std/Sat/AIG/Cached.ilean
+lib/lean/Std/Sat/AIG/Cached.olean
+lib/lean/Std/Sat/AIG/CachedGates.ilean
+lib/lean/Std/Sat/AIG/CachedGates.olean
+lib/lean/Std/Sat/AIG/CachedGatesLemmas.ilean
+lib/lean/Std/Sat/AIG/CachedGatesLemmas.olean
+lib/lean/Std/Sat/AIG/CachedLemmas.ilean
+lib/lean/Std/Sat/AIG/CachedLemmas.olean
+lib/lean/Std/Sat/AIG/If.ilean
+lib/lean/Std/Sat/AIG/If.olean
+lib/lean/Std/Sat/AIG/LawfulOperator.ilean
+lib/lean/Std/Sat/AIG/LawfulOperator.olean
+lib/lean/Std/Sat/AIG/LawfulVecOperator.ilean
+lib/lean/Std/Sat/AIG/LawfulVecOperator.olean
+lib/lean/Std/Sat/AIG/Lemmas.ilean
+lib/lean/Std/Sat/AIG/Lemmas.olean
+lib/lean/Std/Sat/AIG/RefVec.ilean
+lib/lean/Std/Sat/AIG/RefVec.olean
+lib/lean/Std/Sat/AIG/RefVecOperator.ilean
+lib/lean/Std/Sat/AIG/RefVecOperator.olean
+lib/lean/Std/Sat/AIG/RefVecOperator/Fold.ilean
+lib/lean/Std/Sat/AIG/RefVecOperator/Fold.olean
+lib/lean/Std/Sat/AIG/RefVecOperator/Map.ilean
+lib/lean/Std/Sat/AIG/RefVecOperator/Map.olean
+lib/lean/Std/Sat/AIG/RefVecOperator/Zip.ilean
+lib/lean/Std/Sat/AIG/RefVecOperator/Zip.olean
+lib/lean/Std/Sat/AIG/Relabel.ilean
+lib/lean/Std/Sat/AIG/Relabel.olean
+lib/lean/Std/Sat/AIG/RelabelNat.ilean
+lib/lean/Std/Sat/AIG/RelabelNat.olean
+lib/lean/Std/Sat/CNF.ilean
+lib/lean/Std/Sat/CNF.olean
+lib/lean/Std/Sat/CNF/Basic.ilean
+lib/lean/Std/Sat/CNF/Basic.olean
+lib/lean/Std/Sat/CNF/Dimacs.ilean
+lib/lean/Std/Sat/CNF/Dimacs.olean
+lib/lean/Std/Sat/CNF/Literal.ilean
+lib/lean/Std/Sat/CNF/Literal.olean
+lib/lean/Std/Sat/CNF/Relabel.ilean
+lib/lean/Std/Sat/CNF/Relabel.olean
+lib/lean/Std/Sat/CNF/RelabelFin.ilean
+lib/lean/Std/Sat/CNF/RelabelFin.olean
+lib/lean/Std/Tactic.ilean
+lib/lean/Std/Tactic.olean
+lib/lean/Std/Tactic/BVDecide.ilean
+lib/lean/Std/Tactic/BVDecide.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.olean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.ilean
+lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.olean
+lib/lean/Std/Tactic/BVDecide/LRAT.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Actions.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Actions.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Checker.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Parser.olean
+lib/lean/Std/Tactic/BVDecide/Normalize.ilean
+lib/lean/Std/Tactic/BVDecide/Normalize.olean
+lib/lean/Std/Tactic/BVDecide/Normalize/BitVec.ilean
+lib/lean/Std/Tactic/BVDecide/Normalize/BitVec.olean
+lib/lean/Std/Tactic/BVDecide/Normalize/Bool.ilean
+lib/lean/Std/Tactic/BVDecide/Normalize/Bool.olean
+lib/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.ilean
+lib/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.olean
+lib/lean/Std/Tactic/BVDecide/Normalize/Equal.ilean
+lib/lean/Std/Tactic/BVDecide/Normalize/Equal.olean
+lib/lean/Std/Tactic/BVDecide/Normalize/Prop.ilean
+lib/lean/Std/Tactic/BVDecide/Normalize/Prop.olean
+lib/lean/Std/Tactic/BVDecide/Reflect.ilean
+lib/lean/Std/Tactic/BVDecide/Reflect.olean
+lib/lean/Std/Tactic/BVDecide/Syntax.ilean
+lib/lean/Std/Tactic/BVDecide/Syntax.olean
 lib/lean/libInit.a
 lib/lean/libInit_shared.so
 lib/lean/libLake.a
 lib/lean/libLean.a
 lib/lean/libStd.a
 lib/lean/libleancpp.a
+lib/lean/libleanmanifest.a
 lib/lean/libleanrt.a
 lib/lean/libleanshared.so
+lib/lean/libleanshared_1.so
 share/lean/lean.mk
 %%DATADIR%%/src/lean/Init.lean
 %%DATADIR%%/src/lean/Init/BinderPredicates.lean
@@ -2060,6 +2353,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Int/DivModLemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Int/Gcd.lean
 %%DATADIR%%/src/lean/Init/Data/Int/Lemmas.lean
+%%DATADIR%%/src/lean/Init/Data/Int/LemmasAux.lean
 %%DATADIR%%/src/lean/Init/Data/Int/Order.lean
 %%DATADIR%%/src/lean/Init/Data/Int/Pow.lean
 %%DATADIR%%/src/lean/Init/Data/List.lean
@@ -2078,9 +2372,16 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/List/Nat/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/List/Nat/Pairwise.lean
 %%DATADIR%%/src/lean/Init/Data/List/Nat/Range.lean
+%%DATADIR%%/src/lean/Init/Data/List/Nat/Sublist.lean
 %%DATADIR%%/src/lean/Init/Data/List/Nat/TakeDrop.lean
 %%DATADIR%%/src/lean/Init/Data/List/Notation.lean
 %%DATADIR%%/src/lean/Init/Data/List/Pairwise.lean
+%%DATADIR%%/src/lean/Init/Data/List/Perm.lean
+%%DATADIR%%/src/lean/Init/Data/List/Range.lean
+%%DATADIR%%/src/lean/Init/Data/List/Sort.lean
+%%DATADIR%%/src/lean/Init/Data/List/Sort/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/List/Sort/Impl.lean
+%%DATADIR%%/src/lean/Init/Data/List/Sort/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/List/Sublist.lean
 %%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean
 %%DATADIR%%/src/lean/Init/Data/List/Zip.lean
@@ -2110,6 +2411,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Option/Instances.lean
 %%DATADIR%%/src/lean/Init/Data/Option/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Ord.lean
+%%DATADIR%%/src/lean/Init/Data/PLift.lean
 %%DATADIR%%/src/lean/Init/Data/Prod.lean
 %%DATADIR%%/src/lean/Init/Data/Queue.lean
 %%DATADIR%%/src/lean/Init/Data/Random.lean
@@ -2130,6 +2432,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/UInt/Bitwise.lean
 %%DATADIR%%/src/lean/Init/Data/UInt/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean
+%%DATADIR%%/src/lean/Init/Data/ULift.lean
 %%DATADIR%%/src/lean/Init/Dynamic.lean
 %%DATADIR%%/src/lean/Init/Ext.lean
 %%DATADIR%%/src/lean/Init/GetElem.lean
@@ -2327,7 +2630,6 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Data/NameTrie.lean
 %%DATADIR%%/src/lean/Lean/Data/OpenDecl.lean
 %%DATADIR%%/src/lean/Lean/Data/Options.lean
-%%DATADIR%%/src/lean/Lean/Data/Parsec.lean
 %%DATADIR%%/src/lean/Lean/Data/PersistentArray.lean
 %%DATADIR%%/src/lean/Lean/Data/PersistentHashMap.lean
 %%DATADIR%%/src/lean/Lean/Data/PersistentHashSet.lean
@@ -2412,9 +2714,11 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/PatternVar.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Basic.lean
+%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/EqUnfold.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Eqns.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Main.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/MkInhabitant.lean
+%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/BRecOn.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Basic.lean
@@ -2429,6 +2733,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationArgument.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationHint.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF.lean
+%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Basic.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Eqns.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Fix.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -2448,7 +2753,24 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Syntax.lean
 %%DATADIR%%/src/lean/Lean/Elab/SyntheticMVars.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/External.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/LRAT.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Basic.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/BoolToPropSimps.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/BuiltinTactic.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Cache.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Calc.lean
@@ -2499,6 +2821,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Symm.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Unfold.lean
 %%DATADIR%%/src/lean/Lean/Elab/Term.lean
+%%DATADIR%%/src/lean/Lean/Elab/Time.lean
 %%DATADIR%%/src/lean/Lean/Elab/Util.lean
 %%DATADIR%%/src/lean/Lean/Environment.lean
 %%DATADIR%%/src/lean/Lean/Eval.lean
@@ -2781,6 +3104,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Util/LeanOptions.lean
 %%DATADIR%%/src/lean/Lean/Util/MonadBacktrack.lean
 %%DATADIR%%/src/lean/Lean/Util/MonadCache.lean
+%%DATADIR%%/src/lean/Lean/Util/NumApps.lean
 %%DATADIR%%/src/lean/Lean/Util/NumObjs.lean
 %%DATADIR%%/src/lean/Lean/Util/OccursCheck.lean
 %%DATADIR%%/src/lean/Lean/Util/PPExt.lean
@@ -2823,7 +3147,6 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Defs.lean
 %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean
 %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Pairwise.lean
-%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Perm.lean
 %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Sublist.lean
 %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Model.lean
 %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Raw.lean
@@ -2844,6 +3167,121 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Std/Data/HashSet/Lemmas.lean
 %%DATADIR%%/src/lean/Std/Data/HashSet/Raw.lean
 %%DATADIR%%/src/lean/Std/Data/HashSet/RawLemmas.lean
+%%DATADIR%%/src/lean/Std/Internal.lean
+%%DATADIR%%/src/lean/Std/Internal/Parsec.lean
+%%DATADIR%%/src/lean/Std/Internal/Parsec/Basic.lean
+%%DATADIR%%/src/lean/Std/Internal/Parsec/ByteArray.lean
+%%DATADIR%%/src/lean/Std/Internal/Parsec/String.lean
+%%DATADIR%%/src/lean/Std/Sat.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/Basic.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/CNF.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/Cached.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/CachedGates.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/CachedLemmas.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/If.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/LawfulOperator.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/RefVec.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/Relabel.lean
+%%DATADIR%%/src/lean/Std/Sat/AIG/RelabelNat.lean
+%%DATADIR%%/src/lean/Std/Sat/CNF.lean
+%%DATADIR%%/src/lean/Std/Sat/CNF/Basic.lean
+%%DATADIR%%/src/lean/Std/Sat/CNF/Dimacs.lean
+%%DATADIR%%/src/lean/Std/Sat/CNF/Literal.lean
+%%DATADIR%%/src/lean/Std/Sat/CNF/Relabel.lean
+%%DATADIR%%/src/lean/Std/Sat/CNF/RelabelFin.lean
+%%DATADIR%%/src/lean/Std/Tactic.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Actions.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Parser.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Bool.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Prop.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Reflect.lean
+%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Syntax.lean
 %%DATADIR%%/src/lean/lake/Lake.lean
 %%DATADIR%%/src/lean/lake/Lake/Build.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean
@@ -2988,6 +3426,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/clone/test/Main.lean
 %%DATADIR%%/src/lean/lake/tests/clone/test/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/driver/Test.lean
+%%DATADIR%%/src/lean/lake/tests/driver/build.lean
 %%DATADIR%%/src/lean/lake/tests/driver/dep-invalid.lean
 %%DATADIR%%/src/lean/lake/tests/driver/dep-unknown.lean
 %%DATADIR%%/src/lean/lake/tests/driver/dep.lean
@@ -3054,6 +3493,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/precompileArgs/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/rebuild/Main.lean
 %%DATADIR%%/src/lean/lake/tests/rebuild/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/reservoirConfig/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean
 %%DATADIR%%/src/lean/lake/tests/reversion/Main.lean
 %%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean
@@ -3062,3 +3502,4 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/trace/Foo.lean
 %%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean
 %%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean
+%%DATADIR%%/src/lean/lake/tests/versionTags/lakefile.lean