git: fec276899d15 - main - math/lean4: update 4.11.0 → 4.12.0
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
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