pkgsrc-WIP-changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
lean4: finish update by removing ExternalProjects
Module Name: pkgsrc-wip
Committed By: Thomas Klausner <wiz%NetBSD.org@localhost>
Pushed By: wiz
Date: Sat Oct 17 23:04:57 2026 +0200
Changeset: fd6a582e3fe0db6b4b894647799043beb3199c30
Modified Files:
lean4/PLIST
lean4/distinfo
lean4/patches/patch-src_CMakeLists.txt
lean4/patches/patch-stage0_src_CMakeLists.txt
Removed Files:
lean4/TODO
Log Message:
lean4: finish update by removing ExternalProjects
To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=fd6a582e3fe0db6b4b894647799043beb3199c30
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
diffstat:
lean4/PLIST | 1064 +++++++++++++++----------
lean4/TODO | 1 -
lean4/distinfo | 4 +-
lean4/patches/patch-src_CMakeLists.txt | 87 ++
lean4/patches/patch-stage0_src_CMakeLists.txt | 87 ++
5 files changed, 798 insertions(+), 445 deletions(-)
diffs:
diff --git a/lean4/PLIST b/lean4/PLIST
index 9f3cc7db91..22d0c02707 100644
--- a/lean4/PLIST
+++ b/lean4/PLIST
@@ -1,8 +1,9 @@
-@comment $NetBSD: PLIST,v 1.3 2026/09/26 11:04:54 wiz Exp $
+@comment $NetBSD$
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
-lib/lean/Std/Internal/Do/WP/Lemmas.olean.server
lib/lean/Std/Internal/ForIn.ilean
lib/lean/Std/Internal/ForIn.ir
lib/lean/Std/Internal/ForIn.ir.sig
@@ -13946,6 +13955,60 @@ lib/lean/Std/Internal/ForIn/Lemmas.ir.sig
lib/lean/Std/Internal/ForIn/Lemmas.olean
lib/lean/Std/Internal/ForIn/Lemmas.olean.private
lib/lean/Std/Internal/ForIn/Lemmas.olean.server
+lib/lean/Std/Internal/Order/Basic.ilean
+lib/lean/Std/Internal/Order/Basic.ir
+lib/lean/Std/Internal/Order/Basic.ir.sig
+lib/lean/Std/Internal/Order/Basic.olean
+lib/lean/Std/Internal/Order/Basic.olean.private
+lib/lean/Std/Internal/Order/Basic.olean.server
+lib/lean/Std/Internal/Order/FrameClosure.ilean
+lib/lean/Std/Internal/Order/FrameClosure.ir
+lib/lean/Std/Internal/Order/FrameClosure.ir.sig
+lib/lean/Std/Internal/Order/FrameClosure.olean
+lib/lean/Std/Internal/Order/FrameClosure.olean.private
+lib/lean/Std/Internal/Order/FrameClosure.olean.server
+lib/lean/Std/Internal/Order/Heyting.ilean
+lib/lean/Std/Internal/Order/Heyting.ir
+lib/lean/Std/Internal/Order/Heyting.ir.sig
+lib/lean/Std/Internal/Order/Heyting.olean
+lib/lean/Std/Internal/Order/Heyting.olean.private
+lib/lean/Std/Internal/Order/Heyting.olean.server
+lib/lean/Std/Internal/Order/Instances.ilean
+lib/lean/Std/Internal/Order/Instances.ir
+lib/lean/Std/Internal/Order/Instances.ir.sig
+lib/lean/Std/Internal/Order/Instances.olean
+lib/lean/Std/Internal/Order/Instances.olean.private
+lib/lean/Std/Internal/Order/Instances.olean.server
+lib/lean/Std/Internal/Order/Lemmas.ilean
+lib/lean/Std/Internal/Order/Lemmas.ir
+lib/lean/Std/Internal/Order/Lemmas.ir.sig
+lib/lean/Std/Internal/Order/Lemmas.olean
+lib/lean/Std/Internal/Order/Lemmas.olean.private
+lib/lean/Std/Internal/Order/Lemmas.olean.server
+lib/lean/Std/Internal/Order/OfProp.ilean
+lib/lean/Std/Internal/Order/OfProp.ir
+lib/lean/Std/Internal/Order/OfProp.ir.sig
+lib/lean/Std/Internal/Order/OfProp.olean
+lib/lean/Std/Internal/Order/OfProp.olean.private
+lib/lean/Std/Internal/Order/OfProp.olean.server
+lib/lean/Std/Internal/Order/PredTrans.ilean
+lib/lean/Std/Internal/Order/PredTrans.ir
+lib/lean/Std/Internal/Order/PredTrans.ir.sig
+lib/lean/Std/Internal/Order/PredTrans.olean
+lib/lean/Std/Internal/Order/PredTrans.olean.private
+lib/lean/Std/Internal/Order/PredTrans.olean.server
+lib/lean/Std/Internal/Order/PreservesSup.ilean
+lib/lean/Std/Internal/Order/PreservesSup.ir
+lib/lean/Std/Internal/Order/PreservesSup.ir.sig
+lib/lean/Std/Internal/Order/PreservesSup.olean
+lib/lean/Std/Internal/Order/PreservesSup.olean.private
+lib/lean/Std/Internal/Order/PreservesSup.olean.server
+lib/lean/Std/Internal/Order/PropLattice.ilean
+lib/lean/Std/Internal/Order/PropLattice.ir
+lib/lean/Std/Internal/Order/PropLattice.ir.sig
+lib/lean/Std/Internal/Order/PropLattice.olean
+lib/lean/Std/Internal/Order/PropLattice.olean.private
+lib/lean/Std/Internal/Order/PropLattice.olean.server
lib/lean/Std/Internal/Parsec.ilean
lib/lean/Std/Internal/Parsec.ir
lib/lean/Std/Internal/Parsec.ir.sig
@@ -14162,12 +14225,30 @@ lib/lean/Std/Sat/CNF/Dimacs.ir.sig
lib/lean/Std/Sat/CNF/Dimacs.olean
lib/lean/Std/Sat/CNF/Dimacs.olean.private
lib/lean/Std/Sat/CNF/Dimacs.olean.server
+lib/lean/Std/Sat/CNF/Entails.ilean
+lib/lean/Std/Sat/CNF/Entails.ir
+lib/lean/Std/Sat/CNF/Entails.ir.sig
+lib/lean/Std/Sat/CNF/Entails.olean
+lib/lean/Std/Sat/CNF/Entails.olean.private
+lib/lean/Std/Sat/CNF/Entails.olean.server
lib/lean/Std/Sat/CNF/Literal.ilean
lib/lean/Std/Sat/CNF/Literal.ir
lib/lean/Std/Sat/CNF/Literal.ir.sig
lib/lean/Std/Sat/CNF/Literal.olean
lib/lean/Std/Sat/CNF/Literal.olean.private
lib/lean/Std/Sat/CNF/Literal.olean.server
+lib/lean/Std/Sat/CNF/Negation.ilean
+lib/lean/Std/Sat/CNF/Negation.ir
+lib/lean/Std/Sat/CNF/Negation.ir.sig
+lib/lean/Std/Sat/CNF/Negation.olean
+lib/lean/Std/Sat/CNF/Negation.olean.private
+lib/lean/Std/Sat/CNF/Negation.olean.server
+lib/lean/Std/Sat/CNF/Redundancy.ilean
+lib/lean/Std/Sat/CNF/Redundancy.ir
+lib/lean/Std/Sat/CNF/Redundancy.ir.sig
+lib/lean/Std/Sat/CNF/Redundancy.olean
+lib/lean/Std/Sat/CNF/Redundancy.olean.private
+lib/lean/Std/Sat/CNF/Redundancy.olean.server
lib/lean/Std/Sat/CNF/Relabel.ilean
lib/lean/Std/Sat/CNF/Relabel.ir
lib/lean/Std/Sat/CNF/Relabel.ir.sig
@@ -14180,6 +14261,24 @@ lib/lean/Std/Sat/CNF/RelabelFin.ir.sig
lib/lean/Std/Sat/CNF/RelabelFin.olean
lib/lean/Std/Sat/CNF/RelabelFin.olean.private
lib/lean/Std/Sat/CNF/RelabelFin.olean.server
+lib/lean/Std/Sat/CNF/Sat.ilean
+lib/lean/Std/Sat/CNF/Sat.ir
+lib/lean/Std/Sat/CNF/Sat.ir.sig
+lib/lean/Std/Sat/CNF/Sat.olean
+lib/lean/Std/Sat/CNF/Sat.olean.private
+lib/lean/Std/Sat/CNF/Sat.olean.server
+lib/lean/Std/Sat/CNF/SpecLemmas.ilean
+lib/lean/Std/Sat/CNF/SpecLemmas.ir
+lib/lean/Std/Sat/CNF/SpecLemmas.ir.sig
+lib/lean/Std/Sat/CNF/SpecLemmas.olean
+lib/lean/Std/Sat/CNF/SpecLemmas.olean.private
+lib/lean/Std/Sat/CNF/SpecLemmas.olean.server
+lib/lean/Std/Sat/CNF/Unit.ilean
+lib/lean/Std/Sat/CNF/Unit.ir
+lib/lean/Std/Sat/CNF/Unit.ir.sig
+lib/lean/Std/Sat/CNF/Unit.olean
+lib/lean/Std/Sat/CNF/Unit.olean.private
+lib/lean/Std/Sat/CNF/Unit.olean.server
lib/lean/Std/Sync.ilean
lib/lean/Std/Sync.ir
lib/lean/Std/Sync.ir.sig
@@ -14660,126 +14759,60 @@ lib/lean/Std/Tactic/BVDecide/LRAT/Checker.ir.sig
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean.private
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.olean.server
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ilean
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ir
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ir.sig
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean.private
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.olean.server
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ilean
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ir
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ir.sig
@@ -15122,12 +15155,133 @@ lib/lean/Std/Time/Zoned/ZoneRules.ir.sig
lib/lean/Std/Time/Zoned/ZoneRules.olean
lib/lean/Std/Time/Zoned/ZoneRules.olean.private
lib/lean/Std/Time/Zoned/ZoneRules.olean.server
+lib/lean/Std/WP.ilean
+lib/lean/Std/WP.ir
+lib/lean/Std/WP.ir.sig
+lib/lean/Std/WP.olean
+lib/lean/Std/WP.olean.private
+lib/lean/Std/WP.olean.server
+lib/lean/Std/WP/Assertion.ilean
+lib/lean/Std/WP/Assertion.ir
+lib/lean/Std/WP/Assertion.ir.sig
+lib/lean/Std/WP/Assertion.olean
+lib/lean/Std/WP/Assertion.olean.private
+lib/lean/Std/WP/Assertion.olean.server
+lib/lean/Std/WP/Basic.ilean
+lib/lean/Std/WP/Basic.ir
+lib/lean/Std/WP/Basic.ir.sig
+lib/lean/Std/WP/Basic.olean
+lib/lean/Std/WP/Basic.olean.private
+lib/lean/Std/WP/Basic.olean.server
+lib/lean/Std/WP/Conjunctive.ilean
+lib/lean/Std/WP/Conjunctive.ir
+lib/lean/Std/WP/Conjunctive.ir.sig
+lib/lean/Std/WP/Conjunctive.olean
+lib/lean/Std/WP/Conjunctive.olean.private
+lib/lean/Std/WP/Conjunctive.olean.server
+lib/lean/Std/WP/EStack.ilean
+lib/lean/Std/WP/EStack.ir
+lib/lean/Std/WP/EStack.ir.sig
+lib/lean/Std/WP/EStack.olean
+lib/lean/Std/WP/EStack.olean.private
+lib/lean/Std/WP/EStack.olean.server
+lib/lean/Std/WP/Frame.ilean
+lib/lean/Std/WP/Frame.ir
+lib/lean/Std/WP/Frame.ir.sig
+lib/lean/Std/WP/Frame.olean
+lib/lean/Std/WP/Frame.olean.private
+lib/lean/Std/WP/Frame.olean.server
+lib/lean/Std/WP/Gadget/Assert.ilean
+lib/lean/Std/WP/Gadget/Assert.ir
+lib/lean/Std/WP/Gadget/Assert.ir.sig
+lib/lean/Std/WP/Gadget/Assert.olean
+lib/lean/Std/WP/Gadget/Assert.olean.private
+lib/lean/Std/WP/Gadget/Assert.olean.server
+lib/lean/Std/WP/Gadget/ForIn.ilean
+lib/lean/Std/WP/Gadget/ForIn.ir
+lib/lean/Std/WP/Gadget/ForIn.ir.sig
+lib/lean/Std/WP/Gadget/ForIn.olean
+lib/lean/Std/WP/Gadget/ForIn.olean.private
+lib/lean/Std/WP/Gadget/ForIn.olean.server
+lib/lean/Std/WP/Monad.ilean
+lib/lean/Std/WP/Monad.ir
+lib/lean/Std/WP/Monad.ir.sig
+lib/lean/Std/WP/Monad.olean
+lib/lean/Std/WP/Monad.olean.private
+lib/lean/Std/WP/Monad.olean.server
+lib/lean/Std/WP/Monad/Basic.ilean
+lib/lean/Std/WP/Monad/Basic.ir
+lib/lean/Std/WP/Monad/Basic.ir.sig
+lib/lean/Std/WP/Monad/Basic.olean
+lib/lean/Std/WP/Monad/Basic.olean.private
+lib/lean/Std/WP/Monad/Basic.olean.server
+lib/lean/Std/WP/Monad/Conjunctive.ilean
+lib/lean/Std/WP/Monad/Conjunctive.ir
+lib/lean/Std/WP/Monad/Conjunctive.ir.sig
+lib/lean/Std/WP/Monad/Conjunctive.olean
+lib/lean/Std/WP/Monad/Conjunctive.olean.private
+lib/lean/Std/WP/Monad/Conjunctive.olean.server
+lib/lean/Std/WP/Monad/Frame.ilean
+lib/lean/Std/WP/Monad/Frame.ir
+lib/lean/Std/WP/Monad/Frame.ir.sig
+lib/lean/Std/WP/Monad/Frame.olean
+lib/lean/Std/WP/Monad/Frame.olean.private
+lib/lean/Std/WP/Monad/Frame.olean.server
+lib/lean/Std/WP/Monad/Instances.ilean
+lib/lean/Std/WP/Monad/Instances.ir
+lib/lean/Std/WP/Monad/Instances.ir.sig
+lib/lean/Std/WP/Monad/Instances.olean
+lib/lean/Std/WP/Monad/Instances.olean.private
+lib/lean/Std/WP/Monad/Instances.olean.server
+lib/lean/Std/WP/Monad/Lemmas.ilean
+lib/lean/Std/WP/Monad/Lemmas.ir
+lib/lean/Std/WP/Monad/Lemmas.ir.sig
+lib/lean/Std/WP/Monad/Lemmas.olean
+lib/lean/Std/WP/Monad/Lemmas.olean.private
+lib/lean/Std/WP/Monad/Lemmas.olean.server
+lib/lean/Std/WP/Monad/Sound.ilean
+lib/lean/Std/WP/Monad/Sound.ir
+lib/lean/Std/WP/Monad/Sound.ir.sig
+lib/lean/Std/WP/Monad/Sound.olean
+lib/lean/Std/WP/Monad/Sound.olean.private
+lib/lean/Std/WP/Monad/Sound.olean.server
+lib/lean/Std/WP/Triple.ilean
+lib/lean/Std/WP/Triple.ir
+lib/lean/Std/WP/Triple.ir.sig
+lib/lean/Std/WP/Triple.olean
+lib/lean/Std/WP/Triple.olean.private
+lib/lean/Std/WP/Triple.olean.server
+lib/lean/Std/WP/Triple/Basic.ilean
+lib/lean/Std/WP/Triple/Basic.ir
+lib/lean/Std/WP/Triple/Basic.ir.sig
+lib/lean/Std/WP/Triple/Basic.olean
+lib/lean/Std/WP/Triple/Basic.olean.private
+lib/lean/Std/WP/Triple/Basic.olean.server
+lib/lean/Std/WP/Triple/Conjunctive.ilean
+lib/lean/Std/WP/Triple/Conjunctive.ir
+lib/lean/Std/WP/Triple/Conjunctive.ir.sig
+lib/lean/Std/WP/Triple/Conjunctive.olean
+lib/lean/Std/WP/Triple/Conjunctive.olean.private
+lib/lean/Std/WP/Triple/Conjunctive.olean.server
+lib/lean/Std/WP/Triple/Monad.ilean
+lib/lean/Std/WP/Triple/Monad.ir
+lib/lean/Std/WP/Triple/Monad.ir.sig
+lib/lean/Std/WP/Triple/Monad.olean
+lib/lean/Std/WP/Triple/Monad.olean.private
+lib/lean/Std/WP/Triple/Monad.olean.server
+lib/lean/Std/WP/Triple/SpecLemmas.ilean
+lib/lean/Std/WP/Triple/SpecLemmas.ir
+lib/lean/Std/WP/Triple/SpecLemmas.ir.sig
+lib/lean/Std/WP/Triple/SpecLemmas.olean
+lib/lean/Std/WP/Triple/SpecLemmas.olean.private
+lib/lean/Std/WP/Triple/SpecLemmas.olean.server
lib/lean/libInit.a
lib/lean/libInit_shared.so
lib/lean/libLake.a
lib/lean/libLake_shared.so
lib/lean/libLean.a
lib/lean/libLeanChecker.a
+lib/lean/libLeanExport.a
lib/lean/libLeanIR.a
lib/lean/libLeanc.a
lib/lean/libStd.a
@@ -15239,6 +15393,7 @@ src/lean/Init/Data/Dyadic/Basic.lean
src/lean/Init/Data/Dyadic/Instances.lean
src/lean/Init/Data/Dyadic/Inv.lean
src/lean/Init/Data/Dyadic/Round.lean
+src/lean/Init/Data/Erased.lean
src/lean/Init/Data/Fin.lean
src/lean/Init/Data/Fin/Basic.lean
src/lean/Init/Data/Fin/Bitwise.lean
@@ -15246,7 +15401,9 @@ src/lean/Init/Data/Fin/Fold.lean
src/lean/Init/Data/Fin/Iterate.lean
src/lean/Init/Data/Fin/Lemmas.lean
src/lean/Init/Data/Fin/Log2.lean
+src/lean/Init/Data/Fin/MinMax.lean
src/lean/Init/Data/Fin/OverflowAware.lean
+src/lean/Init/Data/Fin/Package.lean
src/lean/Init/Data/Float.lean
src/lean/Init/Data/Float/Float.lean
src/lean/Init/Data/Float/Float32.lean
@@ -15262,6 +15419,7 @@ src/lean/Init/Data/Float/Model/Unpacked/Operations.lean
src/lean/Init/Data/Float/Model/Unpacked/Operations/Add.lean
src/lean/Init/Data/Float/Model/Unpacked/Operations/Compare.lean
src/lean/Init/Data/Float/Model/Unpacked/Operations/Div.lean
+src/lean/Init/Data/Float/Model/Unpacked/Operations/Fma.lean
src/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.lean
src/lean/Init/Data/Float/Model/Unpacked/Operations/OfNat.lean
src/lean/Init/Data/Float/Model/Unpacked/Operations/OfScientific.lean
@@ -15302,6 +15460,7 @@ src/lean/Init/Data/Int/LemmasAux.lean
src/lean/Init/Data/Int/Linear.lean
src/lean/Init/Data/Int/OfNat.lean
src/lean/Init/Data/Int/Order.lean
+src/lean/Init/Data/Int/Package.lean
src/lean/Init/Data/Int/Pow.lean
src/lean/Init/Data/Int/Repr.lean
src/lean/Init/Data/Int/ToString.lean
@@ -15450,6 +15609,8 @@ src/lean/Init/Data/Nat/Log2.lean
src/lean/Init/Data/Nat/MinMax.lean
src/lean/Init/Data/Nat/Mod.lean
src/lean/Init/Data/Nat/Order.lean
+src/lean/Init/Data/Nat/Package.lean
+src/lean/Init/Data/Nat/PowMod.lean
src/lean/Init/Data/Nat/Power2.lean
src/lean/Init/Data/Nat/Power2/Basic.lean
src/lean/Init/Data/Nat/Power2/Bitwise.lean
@@ -15532,6 +15693,7 @@ src/lean/Init/Data/SInt/Float.lean
src/lean/Init/Data/SInt/Float32.lean
src/lean/Init/Data/SInt/IntToBitVec.lean
src/lean/Init/Data/SInt/Lemmas.lean
+src/lean/Init/Data/SInt/Package.lean
src/lean/Init/Data/Slice.lean
src/lean/Init/Data/Slice/Array.lean
src/lean/Init/Data/Slice/Array/Basic.lean
@@ -15636,6 +15798,7 @@ src/lean/Init/Data/UInt/Bitwise.lean
src/lean/Init/Data/UInt/IntToBitVec.lean
src/lean/Init/Data/UInt/Lemmas.lean
src/lean/Init/Data/UInt/Log2.lean
+src/lean/Init/Data/UInt/Package.lean
src/lean/Init/Data/ULift.lean
src/lean/Init/Data/Vector.lean
src/lean/Init/Data/Vector/Algebra.lean
@@ -15673,15 +15836,13 @@ src/lean/Init/Grind/Ext.lean
src/lean/Init/Grind/FieldNormNum.lean
src/lean/Init/Grind/Homo.lean
src/lean/Init/Grind/Homo/BitVec.lean
+src/lean/Init/Grind/Homo/Extra.lean
src/lean/Init/Grind/Homo/Fin.lean
src/lean/Init/Grind/Homo/ISize.lean
-src/lean/Init/Grind/Homo/Int.lean
src/lean/Init/Grind/Homo/Int16.lean
src/lean/Init/Grind/Homo/Int32.lean
src/lean/Init/Grind/Homo/Int64.lean
src/lean/Init/Grind/Homo/Int8.lean
-src/lean/Init/Grind/Homo/List.lean
-src/lean/Init/Grind/Homo/Nat.lean
src/lean/Init/Grind/Homo/UInt16.lean
src/lean/Init/Grind/Homo/UInt32.lean
src/lean/Init/Grind/Homo/UInt64.lean
@@ -15716,10 +15877,8 @@ src/lean/Init/Grind/Ring/CommSolver.lean
src/lean/Init/Grind/Ring/Envelope.lean
src/lean/Init/Grind/Ring/Field.lean
src/lean/Init/Grind/Ring/OfScientific.lean
-src/lean/Init/Grind/Ring/ToInt.lean
src/lean/Init/Grind/Tactics.lean
src/lean/Init/Grind/ToInt.lean
-src/lean/Init/Grind/ToIntLemmas.lean
src/lean/Init/Grind/Util.lean
src/lean/Init/GrindInstances.lean
src/lean/Init/GrindInstances/Nat.lean
@@ -15731,7 +15890,6 @@ src/lean/Init/GrindInstances/Ring/Nat.lean
src/lean/Init/GrindInstances/Ring/Rat.lean
src/lean/Init/GrindInstances/Ring/SInt.lean
src/lean/Init/GrindInstances/Ring/UInt.lean
-src/lean/Init/GrindInstances/ToInt.lean
src/lean/Init/Guard.lean
src/lean/Init/Hints.lean
src/lean/Init/Internal.lean
@@ -16091,6 +16249,7 @@ src/lean/Lean/Elab/InfoTree/Basic.lean
src/lean/Lean/Elab/InfoTree/InlayHints.lean
src/lean/Lean/Elab/InfoTree/Main.lean
src/lean/Lean/Elab/InfoTree/Types.lean
+src/lean/Lean/Elab/InfoTree/Util.lean
src/lean/Lean/Elab/InfoTrees.lean
src/lean/Lean/Elab/InheritDoc.lean
src/lean/Lean/Elab/LetRec.lean
@@ -16151,6 +16310,7 @@ src/lean/Lean/Elab/Quotation.lean
src/lean/Lean/Elab/Quotation/Precheck.lean
src/lean/Lean/Elab/Quotation/Util.lean
src/lean/Lean/Elab/RecAppSyntax.lean
+src/lean/Lean/Elab/Recall.lean
src/lean/Lean/Elab/RecommendedSpelling.lean
src/lean/Lean/Elab/SetOption.lean
src/lean/Lean/Elab/StructInst.lean
@@ -16190,23 +16350,6 @@ src/lean/Lean/Elab/Tactic/Do.lean
src/lean/Lean/Elab/Tactic/Do/Attr.lean
src/lean/Lean/Elab/Tactic/Do/ConjunctivePre.lean
src/lean/Lean/Elab/Tactic/Do/Contract.lean
-src/lean/Lean/Elab/Tactic/Do/Internal.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProc.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/FrameProcAttr.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/LatticeOp.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Util.lean
-src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.lean
src/lean/Lean/Elab/Tactic/Do/LetElim.lean
src/lean/Lean/Elab/Tactic/Do/ProofMode.lean
src/lean/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean
@@ -16253,6 +16396,8 @@ src/lean/Lean/Elab/Tactic/Grind/DSimprocDSL.lean
src/lean/Lean/Elab/Tactic/Grind/DSimprocDSLBuiltin.lean
src/lean/Lean/Elab/Tactic/Grind/Filter.lean
src/lean/Lean/Elab/Tactic/Grind/Have.lean
+src/lean/Lean/Elab/Tactic/Grind/LetToHave.lean
+src/lean/Lean/Elab/Tactic/Grind/LiftLet.lean
src/lean/Lean/Elab/Tactic/Grind/Lint.lean
src/lean/Lean/Elab/Tactic/Grind/LintExceptions.lean
src/lean/Lean/Elab/Tactic/Grind/Main.lean
@@ -16288,6 +16433,7 @@ src/lean/Lean/Elab/Tactic/Repeat.lean
src/lean/Lean/Elab/Tactic/Rewrite.lean
src/lean/Lean/Elab/Tactic/Rewrites.lean
src/lean/Lean/Elab/Tactic/Rfl.lean
+src/lean/Lean/Elab/Tactic/Rwa.lean
src/lean/Lean/Elab/Tactic/Show.lean
src/lean/Lean/Elab/Tactic/ShowTerm.lean
src/lean/Lean/Elab/Tactic/Simp.lean
@@ -16301,6 +16447,22 @@ src/lean/Lean/Elab/Tactic/Symm.lean
src/lean/Lean/Elab/Tactic/TreeTacAttr.lean
src/lean/Lean/Elab/Tactic/Try.lean
src/lean/Lean/Elab/Tactic/Unfold.lean
+src/lean/Lean/Elab/Tactic/VCGen.lean
+src/lean/Lean/Elab/Tactic/VCGen/BinderName.lean
+src/lean/Lean/Elab/Tactic/VCGen/Context.lean
+src/lean/Lean/Elab/Tactic/VCGen/Driver.lean
+src/lean/Lean/Elab/Tactic/VCGen/Entails.lean
+src/lean/Lean/Elab/Tactic/VCGen/FrameProc.lean
+src/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.lean
+src/lean/Lean/Elab/Tactic/VCGen/Frontend.lean
+src/lean/Lean/Elab/Tactic/VCGen/LatticeOp.lean
+src/lean/Lean/Elab/Tactic/VCGen/Reduce.lean
+src/lean/Lean/Elab/Tactic/VCGen/RuleCache.lean
+src/lean/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
+src/lean/Lean/Elab/Tactic/VCGen/Solve.lean
+src/lean/Lean/Elab/Tactic/VCGen/SpecDB.lean
+src/lean/Lean/Elab/Tactic/VCGen/Util.lean
+src/lean/Lean/Elab/Tactic/VCGen/WPApp.lean
src/lean/Lean/Elab/Task.lean
src/lean/Lean/Elab/Term.lean
src/lean/Lean/Elab/Term/TermElabM.lean
@@ -16323,6 +16485,7 @@ src/lean/Lean/LabelAttribute.lean
src/lean/Lean/Language/Basic.lean
src/lean/Lean/Language/Lean.lean
src/lean/Lean/Language/Lean/Types.lean
+src/lean/Lean/Language/Lean/Util.lean
src/lean/Lean/Language/Util.lean
src/lean/Lean/Level.lean
src/lean/Lean/LibrarySuggestions.lean
@@ -16517,6 +16680,8 @@ src/lean/Lean/Meta/Sym/InstantiateMVarsS.lean
src/lean/Lean/Meta/Sym/InstantiateS.lean
src/lean/Lean/Meta/Sym/Intro.lean
src/lean/Lean/Meta/Sym/IsClass.lean
+src/lean/Lean/Meta/Sym/LetToHave.lean
+src/lean/Lean/Meta/Sym/LiftLet.lean
src/lean/Lean/Meta/Sym/LitValues.lean
src/lean/Lean/Meta/Sym/LooseBVarsS.lean
src/lean/Lean/Meta/Sym/MaxFVar.lean
@@ -16674,8 +16839,6 @@ src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean
-src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean
-src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean
@@ -16715,6 +16878,8 @@ src/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Types.lean
src/lean/Lean/Meta/Tactic/Grind/Arith/Util.lean
src/lean/Lean/Meta/Tactic/Grind/Attr.lean
+src/lean/Lean/Meta/Tactic/Grind/BVDecide.lean
+src/lean/Lean/Meta/Tactic/Grind/BVDecide/Types.lean
src/lean/Lean/Meta/Tactic/Grind/Beta.lean
src/lean/Lean/Meta/Tactic/Grind/BitVec.lean
src/lean/Lean/Meta/Tactic/Grind/Cases.lean
@@ -16728,6 +16893,7 @@ src/lean/Lean/Meta/Tactic/Grind/CtorIdx.lean
src/lean/Lean/Meta/Tactic/Grind/Diseq.lean
src/lean/Lean/Meta/Tactic/Grind/EMatch.lean
src/lean/Lean/Meta/Tactic/Grind/EMatchAction.lean
+src/lean/Lean/Meta/Tactic/Grind/EMatchDiagnostics.lean
src/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
src/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean
src/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.lean
@@ -16739,6 +16905,7 @@ src/lean/Lean/Meta/Tactic/Grind/Filter.lean
src/lean/Lean/Meta/Tactic/Grind/Finish.lean
src/lean/Lean/Meta/Tactic/Grind/ForallProp.lean
src/lean/Lean/Meta/Tactic/Grind/Homo.lean
+src/lean/Lean/Meta/Tactic/Grind/Homomorphism.lean
src/lean/Lean/Meta/Tactic/Grind/Injection.lean
src/lean/Lean/Meta/Tactic/Grind/Injective.lean
src/lean/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -17009,6 +17176,10 @@ src/lean/Lean/Widget/TaggedText.lean
src/lean/Lean/Widget/Types.lean
src/lean/Lean/Widget/UserWidget.lean
src/lean/LeanChecker.lean
+src/lean/LeanExport.lean
+src/lean/LeanExport/Basic.lean
+src/lean/LeanExport/Json.lean
+src/lean/LeanExport/Parse.lean
src/lean/LeanIR.lean
src/lean/Leanc.lean
src/lean/Std.lean
@@ -17282,28 +17453,18 @@ src/lean/Std/Http/Server/Handler.lean
src/lean/Std/Http/Test/Helpers.lean
src/lean/Std/Http/Transport.lean
src/lean/Std/Internal.lean
-src/lean/Std/Internal/Do.lean
-src/lean/Std/Internal/Do/Assertion.lean
-src/lean/Std/Internal/Do/ExceptPost.lean
-src/lean/Std/Internal/Do/Gadget/ForIn.lean
-src/lean/Std/Internal/Do/Order/Basic.lean
-src/lean/Std/Internal/Do/Order/Heyting.lean
-src/lean/Std/Internal/Do/Order/Instances.lean
-src/lean/Std/Internal/Do/Order/Lemmas.lean
-src/lean/Std/Internal/Do/Order/PreservesSup.lean
-src/lean/Std/Internal/Do/PredTrans.lean
-src/lean/Std/Internal/Do/Triple.lean
-src/lean/Std/Internal/Do/Triple/Basic.lean
-src/lean/Std/Internal/Do/Triple/Gadget.lean
-src/lean/Std/Internal/Do/Triple/SpecLemmas.lean
-src/lean/Std/Internal/Do/WP.lean
-src/lean/Std/Internal/Do/WP/Basic.lean
-src/lean/Std/Internal/Do/WP/Conjunctive.lean
-src/lean/Std/Internal/Do/WP/Frame.lean
-src/lean/Std/Internal/Do/WP/Lemmas.lean
src/lean/Std/Internal/ForIn.lean
src/lean/Std/Internal/ForIn/Basic.lean
src/lean/Std/Internal/ForIn/Lemmas.lean
+src/lean/Std/Internal/Order/Basic.lean
+src/lean/Std/Internal/Order/FrameClosure.lean
+src/lean/Std/Internal/Order/Heyting.lean
+src/lean/Std/Internal/Order/Instances.lean
+src/lean/Std/Internal/Order/Lemmas.lean
+src/lean/Std/Internal/Order/OfProp.lean
+src/lean/Std/Internal/Order/PredTrans.lean
+src/lean/Std/Internal/Order/PreservesSup.lean
+src/lean/Std/Internal/Order/PropLattice.lean
src/lean/Std/Internal/Parsec.lean
src/lean/Std/Internal/Parsec/Basic.lean
src/lean/Std/Internal/Parsec/ByteArray.lean
@@ -17340,9 +17501,15 @@ src/lean/Std/Sat/AIG/RelabelNat.lean
src/lean/Std/Sat/CNF.lean
src/lean/Std/Sat/CNF/Basic.lean
src/lean/Std/Sat/CNF/Dimacs.lean
+src/lean/Std/Sat/CNF/Entails.lean
src/lean/Std/Sat/CNF/Literal.lean
+src/lean/Std/Sat/CNF/Negation.lean
+src/lean/Std/Sat/CNF/Redundancy.lean
src/lean/Std/Sat/CNF/Relabel.lean
src/lean/Std/Sat/CNF/RelabelFin.lean
+src/lean/Std/Sat/CNF/Sat.lean
+src/lean/Std/Sat/CNF/SpecLemmas.lean
+src/lean/Std/Sat/CNF/Unit.lean
src/lean/Std/Sync.lean
src/lean/Std/Sync/Barrier.lean
src/lean/Std/Sync/Basic.lean
@@ -17423,26 +17590,15 @@ src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
src/lean/Std/Tactic/BVDecide/LRAT.lean
src/lean/Std/Tactic/BVDecide/LRAT/Actions.lean
src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.lean
src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.lean
src/lean/Std/Tactic/BVDecide/LRAT/Parser.lean
src/lean/Std/Tactic/BVDecide/Normalize.lean
src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -17500,6 +17656,26 @@ src/lean/Std/Time/Zoned/Database/Windows.lean
src/lean/Std/Time/Zoned/RecurringRule.lean
src/lean/Std/Time/Zoned/TimeZone.lean
src/lean/Std/Time/Zoned/ZoneRules.lean
+src/lean/Std/WP.lean
+src/lean/Std/WP/Assertion.lean
+src/lean/Std/WP/Basic.lean
+src/lean/Std/WP/Conjunctive.lean
+src/lean/Std/WP/EStack.lean
+src/lean/Std/WP/Frame.lean
+src/lean/Std/WP/Gadget/Assert.lean
+src/lean/Std/WP/Gadget/ForIn.lean
+src/lean/Std/WP/Monad.lean
+src/lean/Std/WP/Monad/Basic.lean
+src/lean/Std/WP/Monad/Conjunctive.lean
+src/lean/Std/WP/Monad/Frame.lean
+src/lean/Std/WP/Monad/Instances.lean
+src/lean/Std/WP/Monad/Lemmas.lean
+src/lean/Std/WP/Monad/Sound.lean
+src/lean/Std/WP/Triple.lean
+src/lean/Std/WP/Triple/Basic.lean
+src/lean/Std/WP/Triple/Conjunctive.lean
+src/lean/Std/WP/Triple/Monad.lean
+src/lean/Std/WP/Triple/SpecLemmas.lean
src/lean/cmake/Modules/README.md
src/lean/lake/Lake.lean
src/lean/lake/Lake/All.lean
@@ -17538,6 +17714,7 @@ src/lean/lake/Lake/CLI.lean
src/lean/lake/Lake/CLI/Actions.lean
src/lean/lake/Lake/CLI/Build.lean
src/lean/lake/Lake/CLI/BuiltinLint.lean
+src/lean/lake/Lake/CLI/Check.lean
src/lean/lake/Lake/CLI/Error.lean
src/lean/lake/Lake/CLI/Help.lean
src/lean/lake/Lake/CLI/Init.lean
@@ -17547,6 +17724,9 @@ src/lean/lake/Lake/CLI/Shake.lean
src/lean/lake/Lake/CLI/Translate.lean
src/lean/lake/Lake/CLI/Translate/Lean.lean
src/lean/lake/Lake/CLI/Translate/Toml.lean
+src/lean/lake/Lake/Check/Axioms.lean
+src/lean/lake/Lake/Check/Compare.lean
+src/lean/lake/Lake/Check/Util.lean
src/lean/lake/Lake/Config.lean
src/lean/lake/Lake/Config/Artifact.lean
src/lean/lake/Lake/Config/Cache.lean
diff --git a/lean4/TODO b/lean4/TODO
deleted file mode 100644
index da40973f20..0000000000
--- a/lean4/TODO
+++ /dev/null
@@ -1 +0,0 @@
-Fails because it wants to use git to check out a lean4lean repository.
diff --git a/lean4/distinfo b/lean4/distinfo
index 5adeb807bf..6af95f5241 100644
--- a/lean4/distinfo
+++ b/lean4/distinfo
@@ -3,11 +3,11 @@ $NetBSD: distinfo,v 1.9 2026/09/26 11:04:54 wiz Exp $
BLAKE2s (lean4-4.35.0.tar.gz) = c65f1e087e298a9c0ec08d0a58481ff56f9f42ee58c34dcea8e011161817f6a0
SHA512 (lean4-4.35.0.tar.gz) = 474f724a1c927470bc5e6b6e658505fb73b34c8a788ca27aada2f1fa8ae82b9e488d719acdebcc255244fb46c442590e5fd68b0e07a2d1814f8aa683a77e43b2
Size (lean4-4.35.0.tar.gz) = 90233735 bytes
-SHA1 (patch-src_CMakeLists.txt) = f859b5e9d25c3cbb3187b60c8513176a760eb159
+SHA1 (patch-src_CMakeLists.txt) = 7151dbd094d203a58689979c48862647dfb791d5
SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
SHA1 (patch-src_include_lean_lean.h) = 017a9c5b5ac185a122a831f6fe4a64e94d9caad9
SHA1 (patch-src_lake_Lake_Build_Common.lean) = d629442adea33b122932170b0ed13397760716d4
SHA1 (patch-src_runtime_process.cpp) = 2a064f747f0448be92e6426e1ba91e34e9d5ca60
-SHA1 (patch-stage0_src_CMakeLists.txt) = c8dad10cbb58a2d127da11e83012ef269f280df2
+SHA1 (patch-stage0_src_CMakeLists.txt) = fd61fca506b91fb32a3eee165498659fb3f49bd1
SHA1 (patch-stage0_src_include_lean_lean.h) = b138c9a082107a667ee3df0623c2ab0e6b2a546f
SHA1 (patch-stage0_src_runtime_process.cpp) = afc46a9ee553a370da3a29ba1e907c6351a5eb1c
diff --git a/lean4/patches/patch-src_CMakeLists.txt b/lean4/patches/patch-src_CMakeLists.txt
index 7937c24fc3..25cef1daa9 100644
--- a/lean4/patches/patch-src_CMakeLists.txt
+++ b/lean4/patches/patch-src_CMakeLists.txt
@@ -3,6 +3,9 @@ $NetBSD: patch-src_CMakeLists.txt,v 1.2 2026/07/24 21:26:20 wiz Exp $
Treat NetBSD like Linux.
https://github.com/leanprover/lean4/pull/14543
+Do not build projects using ExternalProject - this wants to download
+during the build. Package separately?
+
--- src/CMakeLists.txt.orig 2026-10-12 15:51:15.000000000 +0000
+++ src/CMakeLists.txt
@@ -547,7 +547,7 @@ set(LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LIN
@@ -23,3 +26,87 @@ https://github.com/leanprover/lean4/pull/14543
if(BSYMBOLIC)
string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
+@@ -1030,23 +1030,6 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+ VERBATIM
+ )
+
+- # NOTE: uses toolchain from contained `lean-toolchain` so bumps are necessary only on kernel
+- # interface changes. Not in `ALL` as it's expensive; release CI builds it explicitly.
+- ExternalProject_Add(
+- lean4lean
+- PREFIX lean4lean
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/Kha/lean4lean
+- GIT_TAG lean4-bundle-4.35
+- PATCH_COMMAND bash ${LEAN_SOURCE_DIR}/../script/lean4lean-minimal-init.sh
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND lake build lean4lean
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy .lake/build/bin/lean4lean${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+-
+ # `cargo` links with whatever `cc` is on `PATH`. In a standalone build, link the Rust checkers through `leanc`
+ # instead so that they bind to the bundled glibc and the default ELF interpreter like every other shipped binary.
+ set(CARGO_LINK_WITH_LEANC OFF)
+@@ -1055,59 +1038,6 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+ set(CARGO_LINK_WITH_LEANC ON)
+ string(TOUPPER "${CMAKE_SYSTEM_PROCESSOR}_unknown_linux_gnu" CARGO_RUST_TARGET)
+ set(CARGO_BUILD_ENV ${CMAKE_COMMAND} -E env "CARGO_TARGET_${CARGO_RUST_TARGET}_LINKER=${CMAKE_BINARY_DIR}/bin/leanc")
+- endif()
+-
+- # Not in `ALL` as it's expensive; release CI builds it explicitly.
+- ExternalProject_Add(
+- nanoda
+- PREFIX nanoda
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/ammkrn/nanoda_lib
+- GIT_TAG 3a2407216ee84a75f9e1aead6803d0578be06ae7
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND ${CARGO_BUILD_ENV} cargo build --release --locked
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy target/release/nanoda_bin${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+- if(CARGO_LINK_WITH_LEANC)
+- add_dependencies(nanoda leanc)
+- endif()
+-
+- # Not in `ALL` as it's expensive; release CI builds it explicitly.
+- ExternalProject_Add(
+- con-leche
+- PREFIX con-leche
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/leanprover/con-leche
+- GIT_TAG 67f04630d88718e81aa4d07ab64501f68f105398
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND lake build con-leche
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy .lake/build/bin/con-leche${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+-
+- # Not in `ALL` as it's expensive; release CI builds it explicitly. Its only submodule is the
+- # Aeneas verifier, which the binary does not need.
+- ExternalProject_Add(
+- con-ron
+- PREFIX con-ron
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/leanprover/con-ron
+- GIT_TAG dd8d8218892c871276b1e569d3decbb368bba1b6
+- GIT_SUBMODULES ""
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND ${CARGO_BUILD_ENV} cargo build --release --locked
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy target/release/con-ron${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+- if(CARGO_LINK_WITH_LEANC)
+- add_dependencies(con-ron leanc)
+ endif()
+
+ # Not `ALL` as it's big; release CI builds it explicitly.
diff --git a/lean4/patches/patch-stage0_src_CMakeLists.txt b/lean4/patches/patch-stage0_src_CMakeLists.txt
index d1e2a0053c..5ffbed2ef7 100644
--- a/lean4/patches/patch-stage0_src_CMakeLists.txt
+++ b/lean4/patches/patch-stage0_src_CMakeLists.txt
@@ -3,6 +3,9 @@ $NetBSD: patch-stage0_src_CMakeLists.txt,v 1.2 2026/07/24 21:26:20 wiz Exp $
Treat NetBSD like Linux.
https://github.com/leanprover/lean4/pull/14543
+Do not build projects using ExternalProject - this wants to download
+during the build. Package separately?
+
--- stage0/src/CMakeLists.txt.orig 2026-10-12 15:51:15.000000000 +0000
+++ stage0/src/CMakeLists.txt
@@ -547,7 +547,7 @@ set(LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LIN
@@ -23,3 +26,87 @@ https://github.com/leanprover/lean4/pull/14543
if(BSYMBOLIC)
string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
+@@ -1030,23 +1030,6 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+ VERBATIM
+ )
+
+- # NOTE: uses toolchain from contained `lean-toolchain` so bumps are necessary only on kernel
+- # interface changes. Not in `ALL` as it's expensive; release CI builds it explicitly.
+- ExternalProject_Add(
+- lean4lean
+- PREFIX lean4lean
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/Kha/lean4lean
+- GIT_TAG lean4-bundle-4.35
+- PATCH_COMMAND bash ${LEAN_SOURCE_DIR}/../script/lean4lean-minimal-init.sh
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND lake build lean4lean
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy .lake/build/bin/lean4lean${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+-
+ # `cargo` links with whatever `cc` is on `PATH`. In a standalone build, link the Rust checkers through `leanc`
+ # instead so that they bind to the bundled glibc and the default ELF interpreter like every other shipped binary.
+ set(CARGO_LINK_WITH_LEANC OFF)
+@@ -1055,59 +1038,6 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+ set(CARGO_LINK_WITH_LEANC ON)
+ string(TOUPPER "${CMAKE_SYSTEM_PROCESSOR}_unknown_linux_gnu" CARGO_RUST_TARGET)
+ set(CARGO_BUILD_ENV ${CMAKE_COMMAND} -E env "CARGO_TARGET_${CARGO_RUST_TARGET}_LINKER=${CMAKE_BINARY_DIR}/bin/leanc")
+- endif()
+-
+- # Not in `ALL` as it's expensive; release CI builds it explicitly.
+- ExternalProject_Add(
+- nanoda
+- PREFIX nanoda
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/ammkrn/nanoda_lib
+- GIT_TAG 4c544ed4099c8227f07d5de77ad1e69fb0740a27
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND ${CARGO_BUILD_ENV} cargo build --release --locked
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy target/release/nanoda_bin${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+- if(CARGO_LINK_WITH_LEANC)
+- add_dependencies(nanoda leanc)
+- endif()
+-
+- # Not in `ALL` as it's expensive; release CI builds it explicitly.
+- ExternalProject_Add(
+- con-leche
+- PREFIX con-leche
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/leanprover/con-leche
+- GIT_TAG b46cb0e6138d975e657857526839a3c7d8a1df20
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND lake build con-leche
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy .lake/build/bin/con-leche${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+-
+- # Not in `ALL` as it's expensive; release CI builds it explicitly. Its only submodule is the
+- # Aeneas verifier, which the binary does not need.
+- ExternalProject_Add(
+- con-ron
+- PREFIX con-ron
+- EXCLUDE_FROM_ALL ON
+- GIT_REPOSITORY https://github.com/leanprover/con-ron
+- GIT_TAG cb54c9a4e5f604a678b0230f96b8358b9fd73c82
+- GIT_SUBMODULES ""
+- CONFIGURE_COMMAND ""
+- BUILD_COMMAND ${CARGO_BUILD_ENV} cargo build --release --locked
+- BUILD_IN_SOURCE ON
+- INSTALL_COMMAND
+- ${CMAKE_COMMAND} -E copy target/release/con-ron${CMAKE_EXECUTABLE_SUFFIX}
+- ${CMAKE_BINARY_DIR}/bin
+- )
+- if(CARGO_LINK_WITH_LEANC)
+- add_dependencies(con-ron leanc)
+ endif()
+
+ # Not `ALL` as it's big; release CI builds it explicitly.
Home |
Main Index |
Thread Index |
Old Index