Lake build fails on Windows when issuing long command line

[bernborgess]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [ ] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

lake build is failing to build in Windows, in a project using mathlib. As the Zulip Topic details, this might be an issue with ERROR_INVALID_PARAMETER, as lake is calling CreateProcess with a 56856-character string as the lpCommandLine argument, and that's invalid because the maximum length for that parameter is 32767 characters. @bustercopley was able to produce an exe by writing the arguments to a file args.txt and invoking leanc as leanc.exe @args.txt, what lake should be doing automatically.

Context

The error was discussed about on this topic: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/could.20not.20rename.20packages.20directory

Steps to Reproduce

1. Clone the repository at the issue branch

   git clone -b WindowsIssue https://github.com/bernborgess/lean-cutting-planes.git

2. Execute the setup commands, which are working:

   cd lean-cutting-planes
   lake update
   lake exe cache get

3. Trigger the build and check for errors:

   lake build

Expected behavior: The build completes successfully, albeit with sorry warnings

 $ lake build
[698/1402] Building LeanCuttingPlanes.Rules.Division
warning: ././././LeanCuttingPlanes/Rules/Division.lean:14:8-14:16: declaration uses 'sorry'
[699/1402] Building LeanCuttingPlanes.Rules.Saturation
warning: ././././LeanCuttingPlanes/Rules/Saturation.lean:10:8-10:18: declaration uses 'sorry'

Actual behavior: Build fails with error

PS D:\ic\lean-cutting-planes> lake build
[421/1402] Building Mathlib.Tactic.Widget.SelectInsertParams
[447/1402] Building Mathlib.Algebra.GroupWithZero.Units.Basi
[483/1402] Building Mathlib.Order.Interval.Set.UnorderedInte[491/1402] Building Mathlib.Order.Interval.Set.OrderEmbeddin
[512/1402] Building Mathlib.Algebra.CovariantAndContravarian[515/1402] Building Mathlib.Algebra.Order.Monoid.Canonical.D[521/1402] Building Mathlib.Algebra.GroupWithZero.Units.Equi[530/1402] Building Mathlib.Algebra.Order.GroupWithZero.Cano[542/1402] Building Mathlib.Algebra.GroupPower.CovariantClas
[593/1402] Building Mathlib.Algebra.BigOperators.Multiset.Ba
[668/1402] Building Mathlib.Algebra.Order.Interval.Set.Monoi
[680/1402] Building Mathlib.Algebra.GroupWithZero.Divisibili[685/1402] Building Mathlib.Algebra.BigOperators.Multiset.Le
[698/1402] Building LeanCuttingPlanes.Rules.Division        
warning: .\.\.\.\LeanCuttingPlanes\Rules\Division.lean:14:8-14:16: declaration uses 'sorry'
[699/1402] Building LeanCuttingPlanes.Rules.Saturation      
warning: .\.\.\.\LeanCuttingPlanes\Rules\Saturation.lean:10:8-10:18: declaration uses 'sorry'
[1122/1402] Compiling Mathlib.Tactic.Widget.SelectInsertPara[1148/1402] Compiling Mathlib.Algebra.GroupWithZero.Units.Ba[1184/1402] Compiling Mathlib.Order.Interval.Set.UnorderedIn[1192/1402] Compiling Mathlib.Order.Interval.Set.OrderEmbedd[1199/1402] Compiling Mathlib.Order.Interval.Set.OrdConnecte[1213/1402] Compiling Mathlib.Algebra.CovariantAndContravari[1216/1402] Compiling Mathlib.Algebra.Order.Monoid.Canonical[1222/1402] Compiling Mathlib.Algebra.GroupWithZero.Units.Eq[1231/1402] Compiling Mathlib.Algebra.Order.GroupWithZero.Ca[1243/1402] Compiling Mathlib.Algebra.GroupPower.CovariantCl[1293/1402] Compiling Mathlib.Algebra.BigOperators.List.Basi[1294/1402] Compiling Mathlib.Algebra.BigOperators.Multiset.[1369/1402] Compiling Mathlib.Algebra.Order.Interval.Set.Mon[1381/1402] Compiling Mathlib.Algebra.GroupWithZero.Divisibi[1382/1402] Compiling Mathlib.Algebra.Ring.Divisibility.Basi[1385/1402] Compiling Mathlib.Algebra.BigOperators.List.Lemm[1386/1402] Compiling Mathlib.Algebra.BigOperators.Multiset.[1402/1402] Linking lean-cutting-planes.exe
trace: .> c:\Users\bernb\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe -o .\.\.lake\build\bin\lean-cutting-planes.exe .\.\.lake\build\ir\Main.c.o.noexport .\.\.lake\build\ir\LeanCuttingPlanes\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Mathport\Rename.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Nat\Notation.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Attr.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Position.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Deprecated.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Alias.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Int\Order.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Int\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Init\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\String\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Array\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\MemoFix.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Expr\ReplaceRec.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\EnvExtension.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\OpenPrivate.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Meta\Simp.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\NameMapAttribute.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Lint\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Lint\Misc.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Util\LibraryNote.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Lint\Simp.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Lint\TypeClass.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Lint\Frontend.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Lint.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Init.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Logic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Meta.c.o.noexport 
.\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Elab\Tactic\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Relation\Trans.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Eqns.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Expr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Simps\NotationClass.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Array\Match.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\String\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Name.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Nat\Gcd.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Int\DivMod.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Float.c.o.noexport 
.\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Rat\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Expr\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Simps\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ToAdditive.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\ZeroOne.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Lemma.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\TypeStar.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\AssertExists.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Mathport\Attributes.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ProjectionNotation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Logic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Cases.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Semiconj\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Algebra\Classes.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Commute\Defs.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Check.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Nanos.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Util\UnionFind.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Init\Attach.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Array\Init\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Array\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Array\Merge.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Util\UnorderedArraySet.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\SeqFocus.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Classes\Order.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\UInt.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Char.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Control\ForInStep\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Control\ForInStep\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\String\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\String.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\Expr.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\PersistentHashMap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\DiscrTree.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\PersistentHashSet.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Util\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Rule\Name.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tracing.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RulePattern.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Index\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Options\Public.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Options\Internal.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Options.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Percent.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Util\Tactic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\MonadBacktrack.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\SavedState.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Util\EqualUpToIds.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\Clear.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\Inaccessible.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\HashSet.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\PermuteGoals.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Script.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Rule\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\InstantiateMVars.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Index.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Rule.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleSet\Member.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleSet\Name.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleSet\Filter.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleSet.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend\Extension\Init.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend\Extension.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\ElabM.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac\ElabRuleTerm.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Apply.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac\Cases.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Cases.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Constructors.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\NormSimp.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Tactic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Default.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Forward.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder\Unfold.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Builder.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend\RuleExpr.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend\Attribute.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac\Apply.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\UnusedNames.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\AssertHypotheses.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac\Forward.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac\Preprocess.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac\Tactic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\RuleTac.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\Expansion\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\Expansion\Simp.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Constants.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\UnsafeQueue.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\Data.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\Traversal.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\RunMetaM.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\TreeM.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\AddRapp.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\State.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\Check.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\Tracing.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\ExtractProof.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\ExtractScript.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree\Free.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Tree.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\Queue\Class.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Stats\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\SearchM.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\RuleSelection.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\Expansion\Norm.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\Expansion.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Exception.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\ExpandSafePrefix.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\BinomialHeap\Basic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\Queue.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Search\Main.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules\Assumption.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules\ApplyHyps.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules\DestructProducts.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules\Ext.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules\Intros.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules\Split.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules\Subst.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Stats\Extension.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Stats\Report.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend\Command.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend\Tactic.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Frontend.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\BuiltinRules.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop\Main.c.o.noexport .\.\.lake/packages\aesop\.lake\build\ir\Aesop.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Nat\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Nat\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\WF.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\CompileInductive.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Nat\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Ordering\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Core.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\SplitIfs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Order\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Nat\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Classes\BEq.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Classes\Cast.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Classes\RatCast.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Classes\SatisfiesM.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Misc.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Control\ForInStep.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Control\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\MLList\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Control\Nondet\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Util\ProofWanted.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Array\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Array\Monadic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Array.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\AssocList.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\BinomialHeap\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\BinomialHeap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\BitVec\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\BitVec.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Bool.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\ByteArray.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\DList.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Fin\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Fin\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Fin.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\HashMap\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\HashMap\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\HashMap\WF.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\HashMap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Int\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Int.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\LazyList.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Count.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\EraseIdx.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Pairwise.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List\Perm.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\List.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\MLList\Heartbeats.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\System\IO.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\MLList\IO.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\MLList.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Nat.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Option\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Option.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\PairingHeap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\RBMap\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\RBMap\WF.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\RBMap\Alter.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\RBMap\Depth.c.o.noexport 
.\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\RBMap\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\RBMap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Range\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Range.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Rat\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Rat.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Sum\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Sum\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\Sum.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\UnionFind\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\UnionFind\Lemmas.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Data\UnionFind.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\TagAttribute.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\AttributeExtra.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Delaborator.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Except.c.o.noexport 
.\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\HashMap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\IO\Process.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Json.c.o.noexport 
.\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Meta\Simp.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\NameMap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\SMap.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Syntax.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Util\EnvSearch.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Lean\Util\Path.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Unreachable.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Linter\UnreachableTactic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Linter\UnnecessarySeqFocus.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Linter.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\StdDeprecations.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Basic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Case.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Classical.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Congr.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Exact.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Instances.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\NoMatch.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\PrintDependents.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\PrintPrefix.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\ShowUnused.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\SqueezeScope.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Tactic\Where.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Test\Internal\DummyLabelAttr.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Util\Cache.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Util\CheckTactic.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Util\ExtendedBinder.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries\Util\Pickle.c.o.noexport .\.\.lake/packages\batteries\.lake\build\ir\Batteries.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\PPWithUniv.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ExtendDoc.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\AdaptationNote.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Attr\Register.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Function.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Nonempty.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Set.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Function\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Nontrivial\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\GCongr\ForwardAttr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\GCongr\Core.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Conv.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\PushNeg.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\IsEmpty.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Meta\CongrTheorems.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Congr!.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Convert.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Int\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\SimpRw.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Inhabit.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Prod\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Name.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\MkIffOfInductiveProp.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Sum\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Unique.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Spread.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Pi\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\FunLike\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Hom\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Hom\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\FunLike\Embedding.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\FunLike\Equiv.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Bool\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Option\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Sigma\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Subtype.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Sigma\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Quot.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Relator.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Elab\Term.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\PrettyPrinter\Delaborator.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\WithWeakNamespace.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ScopedNS.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Mathport\Notation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Quot.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Coe.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Bool\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Substs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Equiv\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Function\Conjugate.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Lift.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Contrapose.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\GeneralizeProofs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Equiv\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Equiv\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Cast\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Int\Cast\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Int\Cast\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\InjSurj.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Semiconj\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Commute\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Defs.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\ForLean\ReduceEval.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\ForLean\ToExpr.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\Typ.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\Macro.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\Delab.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\MetaM.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\ForLean\Do.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\SortLocalDecls.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\Match.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq\AssertInstancesCommute.c.o.noexport .\.\.lake/packages\Qq\.lake\build\ir\Qq.c.o.noexport .\.\.lake/packages\importGraph\.lake\build\ir\ImportGraph\RequiredModules.c.o.noexport .\.\.lake/packages\importGraph\.lake\build\ir\ImportGraph\Imports.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ApplyCongr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Meta\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ApplyAt.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ApplyWith.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ByContra.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\CasesM.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Check.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\Tactic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Choose.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ClearExclamation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ClearExcept.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Clear_.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\TermCongr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Congrm.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Constructor.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\DefEqTransformations.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ToLevel.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\DeriveToExpr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Existsi.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ExtractGoal.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ExtractLets.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\FailIfNoProgress.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Find.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\GuardGoalNums.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\GuardHypNums.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\HelpCmd.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\HigherOrder.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Hint.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\InferParam.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\IrreducibleDef.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Lint.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\NthRewrite.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Observe.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Propose.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\RSuffices.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Recover.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Relation\Rfl.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Rename.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\RenameBVar.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Says.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Set.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\SimpIntro.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\SuccessIfFailWithMsg.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\SudoSetOption.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\SwapVar.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Tauto.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\WhatsNew.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ToExpr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Trace.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\TypeCheck.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\UnsetOption.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Use.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Variable.c.o.noexport .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Compat.c.o.noexport .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Component\Basic.c.o.noexport .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Component\MakeEditLink.c.o.noexport .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Util.c.o.noexport .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Data\Html.c.o.noexport .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Cancellable.c.o.noexport .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Component\OfRpcMethod.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Widget\SelectInsertParamsClass.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Widget\SelectPanelUtils.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Widget\Calc.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Widget\Congrm.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Widget\Conv.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\WLOG.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\CountHeartbeats.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Common.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupPower\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Nontrivial\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Attr\Core.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Nontriviality\Core.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Nontriviality.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Opposites.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Opposite.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Units\Hom.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\NeZero.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Hom.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\NeZero.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Order\LinearOrder.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Notation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Synonym.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\OrderSynonym.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Units\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Prod.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Function\Iterate.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Int\Order.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Compare.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Max.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Relation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\RelClasses.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Monotone\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\ULift.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Lattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\MinMax.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\FBinop.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\SProd.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\BoundedOrder.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Disjoint.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\PropInstances.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Heyting\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\BooleanAlgebra.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\SymmDiff.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\Delaborators.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Subsingleton.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Set\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Option\NAry.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Control\Combinators.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Option\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\WithBot.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Image.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Prod.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Function.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Directed.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Set\Image.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\NAry.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Bounds\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Set\UnorderedInterval.c.o.noexport 
.\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Control\EquivFunctor.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Equiv\Option.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Prod\PProd.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Embedding\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\RelIso\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\Monotonicity\Attr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Hom\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Set\OrderEmbedding.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Pairwise.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Pairwise\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Equiv\Set.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Hom\Set.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Antichain.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\SetNotation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Set\OrdConnected.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Antisymmetrization.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Cover.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Function\Support.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Hom\Instances.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Pi\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Function\Indicator.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Hom\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Embedding.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finite\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\TypeTags.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Nat.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\CovariantAndContravariant.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\Canonical\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Sub\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Group\Nat.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\WithOne\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\InjSurj.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Units\Equiv.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Units\Equiv.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\WithZero.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Group\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Group\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\OrderDual.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\TypeTags.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\ZeroLEOne.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\GroupWithZero\Canonical.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\MinMax.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\NatCast.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Ring\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Ring\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Sub\Canonical.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Ring\Canonical.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Nat.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Ring\Nat.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\CharZero\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Int.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Int.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupPower\CovariantClass.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Group\OrderIso.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Group\Lattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Group\Abs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Divisibility\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Group\Int.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Ring\Int.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fin\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Attr.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Control\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Control\Functor.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\List\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\List\Instances.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\List\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Forall2.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Lex.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Infix.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Chain.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Enum.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Data\Fin\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Nodup.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Pairwise.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Zip.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Range.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Count.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Dedup.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\InsertNth.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Lattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Join.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Permutation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Factorial\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Perm.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\GetD.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\List.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Quot.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Range.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Nodup.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Dedup.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\FinsetOps.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Semiconj.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\InjSurj.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Bracket.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Commute.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\ProdSigma.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Rotate.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\List\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\Multiset\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\GroupTheory\GroupAction\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Bind.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Union.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Image.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fin\OrderHom.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\WellFounded.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Pi\Lex.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fin\Tuple\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\OfFn.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\FinRange.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Piecewise.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Card.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Duplicate.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Sort.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\NodupEquivFin.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Card.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Monoid\WithTop.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Fold.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Fold.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Option.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Pi.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Pi.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Prod.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Lattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Bool\Set.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Set.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Control\ULift.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\ULift.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\CompleteLattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\CompleteBooleanAlgebra.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\GaloisConnection.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Lattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Hom\Bounded.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Hom\Lattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Lattice.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Choose\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\List\Sublists.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Powerset.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Powerset.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Powerset.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Prod.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Sigma.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Sigma.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Sigma.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Multiset\Sum.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Sum.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Embedding\Set.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Sum.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Pi.c.o.noexport 
.\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Vector.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Control\Applicative.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Control\Traversable\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Vector\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Setoid\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Tactic\ApplyFun.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Sym\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Vector.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finite\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Lean\Expr\ExtraRecognizers.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Functor.c.o.noexport 
.\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\Finite.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Finset\Preimage.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fin\VecNotation.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Option.c.o.noexport 
.\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\Option.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\BigOperators.c.o.noexport 
.\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Cast\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Cast\NeZero.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Cast\Order.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Finset\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Finset\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\Interval\Multiset.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Interval\Set\Monoid.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Interval\Finset.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Interval.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fin\Interval.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fintype\Fin.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Logic\Equiv\Fin.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Semiconj\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Init\Classical.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Semiconj.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Commute\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Commute.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Divisibility\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\GroupWithZero\Divisibility.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Divisibility\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Int\Units.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\List\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\Multiset\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Rat\Init.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Field\Defs.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Order\Ring\CharZero.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Ring\Hom\Basic.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Nat\Cast\Commute.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Int\Cast\Lemmas.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\Ring.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\BigOperators\Fin.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Fin\Tuple\Reflection.c.o.noexport .\.\.lake\build\ir\LeanCuttingPlanes\Data\PBO.c.o.noexport .\.\.lake\build\ir\LeanCuttingPlanes\Rules\Addition.c.o.noexport .\.\.lake\build\ir\LeanCuttingPlanes\Rules\Multiplication.c.o.noexport .\.\.lake\build\ir\LeanCuttingPlanes\Rules\Division.c.o.noexport .\.\.lake\build\ir\LeanCuttingPlanes\Rules\Saturation.c.o.noexport .\.\.lake\build\ir\LeanCuttingPlanes.c.o.noexport
error: failed to execute 'c:\Users\bernb\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe': unspecified system_category error (error code: 87)
Some build steps logged failures:
- Linking lean-cutting-planes.exe
error: build failed

Versions

Lean.versionString: "4.8.0-rc1" OS version: Windows 10 Home Single Language 22H2

Impact

General compilation in Windows with Mathlib