Report #7 — adler2 2.0.1: Adler-32 computation core verified with Aeneas and Lean

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

5 verified claims · 0 findings

Recorded by the author; proofs.rs has not re-run it. How to read a report

keiichiw · 2026-10-17 05:11 UTC

Revision v2 · v1

Overview

Verified API contracts

This report covers the Adler-32 computation core extracted with default Cargo
features for macOS arm64. The five mapped theorems prove successful execution
and functional correctness in the extracted Lean model:

Adler32::new returns the initial state (a, b) = (1, 0).
Adler32::checksum returns 65536 * b + a for every state.
Adler32::from_checksum decodes every u32 into
a = checksum % 65536 and b = checksum / 65536.
Adler32::write_slice updates the state exactly as specified by the scalar
Adler-32 recurrence, for every representable initial state and byte slice.
adler32_slice returns the checksum of that recurrence starting from (1, 0).

In Rust, write_slice mutates the state and returns (). The extracted Lean
function represents this mutation by returning the updated state.

Meaning of update correctness

An initial state consists of two 16-bit unsigned values: a and b may each
range from 0 through 65535. The contracts cover all such states, including
those restored from arbitrary u32 checksums.

The specification first reduces both state halves modulo 65521, then processes
each byte x in order:

a := (a + x) mod 65521
b := (b + a) mod 65521

The proof covers the actual extracted optimized compute body, including its loops,
machine arithmetic, and indexing. It proves a successful result in the model,
not merely a property conditional on execution succeeding. There is no
normalized-seed assumption or input-length bound beyond slice representability.

Empty updates also normalize the state. For example, restoring 0xffffffff
and writing an empty slice produces state (14, 14), with checksum 0x000e000e.
Encoding and decoding alone do not perform this normalization.

Supplementary proofs

The local theorem inventory also includes proofs that:

Encoding and decoding round-trip every state and every u32 checksum.
Split updates and an update over their concatenation both succeed and return
the same complete state.
Saving the intermediate checksum, restoring it, and continuing the update
produces that same state.

These are supplementary audited theorems, not additional API mappings. The split
and resumption laws take slices xs, ys, and whole whose byte sequences satisfy
whole = xs ++ ys. Thus the concatenated input must itself be representable as
a slice; these laws do not establish the success of allocating that slice.

Source and evidence

The model is extracted from unchanged upstream sources pinned by a Git submodule.
Source checks compare src/ with the checksummed release archive and check the
outer Cargo manifest's features and dependencies against upstream.

Local verification workflow. scripts/verify.sh checks source identity,
regenerates and compares the Lean model, rebuilds the proofs, and checks input
fingerprints before and after verification. Its audit starts from the 46 named
theorem roots in verification/theorems.json and follows their proof dependencies.
Those roots include the five API contracts, supplementary laws, and implementation
lemmas. The number 46 is not a count of verified APIs or of every auxiliary theorem.
Native tests are separate evidence, not the basis of the universal contracts above.

Saved verification evidence. The accepted local run dated 2026-10-16, recorded
in verification/results.md, completed this workflow and separately checked the
five API mappings. That run did not execute cargo proofs run; its evidence is
distinct from subsequent recorder experiments.

proofs.rs recording. The Aeneas adapter builds the configured Lean modules
and transitively audits the five mapped theorem roots. It does not rerun
Charon/Aeneas extraction or independently establish the correspondence between
Rust and the Lean model. Fresh extraction, source identity, and the supplementary
theorem audit belong to the separate local verification workflow above.

Findings (0)

No findings reported.

APIs (5)

Functions

pub fn adler32_slice(data: &[u8]) -> u32

Claim #5

Associated functions

`impl Adler32`

pub const fn from_checksum(sum: u32) -> Self

Claim #2

pub fn new() -> Self

Claim #3

Methods

`impl Adler32`

pub fn checksum(self: &Self) -> u32

Claim #1

pub fn write_slice(self: &mut Self, bytes: &[u8])

Claim #4

Evidence

https://github.com/keiichiw/crate-proofs/tree/5c4e0f729b5bd557451157346250211069968474

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/keiichiw/crate-proofs report-7-source-1
git -C report-7-source-1 checkout --detach 5c4e0f729b5bd557451157346250211069968474
git -C report-7-source-1 submodule update --init --recursive --checkout
cd report-7-source-1/adler2/2.0.1/proofs

lake build +Proofs.Codec +Proofs.PublicUpdate +Proofs.Smoke

printf '%s' 'import Aeneas
import Proofs.Codec
import Proofs.PublicUpdate
import Proofs.Smoke
set_option pp.all true
set_option pp.universes true
set_option pp.explicit true
set_option pp.fullNames true
set_option pp.notation false
set_option pp.proofs true
set_option pp.deepTerms true
set_option pp.maxSteps 10000000
-- proofs.rs adapter for Lean 4.35.0 / Aeneas be86ab0f.
-- Uses Lean'\''s environment, Meta telescope and pretty-printer, never source parsing.
open Lean Meta Elab Command
namespace ProofsProbe
meta def moduleOf (env : Environment) (n : Name) : String :=
  match env.getModuleIdxFor? n with
  | some idx => env.header.moduleNames[idx.toNat]!.toString
  | none => ""
meta def pretty (e : Expr) : MetaM String := do
  let s := (← ppExpr e).pretty
  if s.contains '\''⋯'\'' then
    throwError "Lean display contains an omission marker (or literal ⋯); refusing an incomplete proposition"
  if s.utf8ByteSize > 1000000 then throwError "Proposition exceeds 1,000,000-byte recording limit"
  return s
-- The full statement stays explicit; the inspection view uses Lean notation.
meta def readable (e : Expr) : MetaM String :=
  withOptions (fun o =>
    let o := o.setBool `pp.all false
    let o := o.setBool `pp.explicit false
    let o := o.setBool `pp.universes false
    o.setBool `pp.notation true) (pretty e)
-- Only a constant'\''s own tag grants a link; names in plain text are never guessed.
partial def segments (code : Widget.CodeWithInfos) (ref : Option Name := none) : Array Json :=
  match code with
  | .text text => #[Json.mkObj (([("text", toJson text)]) ++
      (ref.toList.map fun n => ("ref", toJson n.toString)))]
  | .append parts => parts.foldl (fun acc part => acc ++ segments part ref) #[]
  | .tag info part =>
    let ref := match info.info.val.info with
      | .ofTermInfo ti => ti.expr.constName?
      | _ => none
    segments part ref
meta def readableFields (key : String) (e : Expr) : MetaM (List (String × Json)) := do
  let text ← readable e
  let base := [(key, toJson text)]
  try
    let code ← withOptions (fun o =>
      let o := o.setBool `pp.all false
      let o := o.setBool `pp.explicit false
      let o := o.setBool `pp.universes false
      let o := o.setBool `pp.notation true
      o.setBool `pp.tagAppFns true) (Widget.ppExprTagged e)
    let parts := segments code
    let joined := String.join (parts.toList.map fun j =>
      (j.getObjValAs? String "text").toOption.getD "")
    if joined != text || parts.size > 10000 || joined.utf8ByteSize > 1000000 then
      return base
    return base ++ [(key ++ "_segments", toJson parts)]
  catch _ => return base
meta def inspect (n : Name) (ty : Expr) (manual : Bool) : MetaM (Option Json) := do
  let env ← getEnv
  forallTelescope ty fun xs conclusion => do
    let programExpr ← try
      let normalized ← Aeneas.Utils.normalizeLetBindings conclusion
      let (expr, _) ← Aeneas.Step.getStepSpecFunArgsExpr normalized
      pure (some expr)
    catch _ => pure none
    if programExpr.isNone && !manual then return none
    let full ← pretty ty
    let program ← match programExpr with
      | some expr => pure (toJson (← readable expr))
      | none => pure Json.null
    let head := toJson (programExpr.bind (·.getAppFn.constName?) |>.map Name.toString)
    let mut binders := #[]
    for x in xs do
      let d ← x.fvarId!.getDecl
      let prop ← isProp d.type
      binders := binders.push (Json.mkObj ((← readableFields "type" d.type) ++ [
        ("name", toJson d.userName.toString),
        ("kind", toJson (if d.binderInfo.isInstImplicit then "instance" else if prop then "hypothesis" else "variable")),
        ("binder", toJson (if d.binderInfo.isInstImplicit then "instance" else if d.binderInfo.isExplicit then "explicit" else "implicit"))]))
    if binders.size > 1000 then throwError "More than 1000 binders"
    let some ranges ← findDeclarationRanges? n | throwError "Missing theorem source range: {n}"
    let axioms ← Lean.collectAxioms n
    let constants := ty.getUsedConstants
    let mut definitions := #[]
    for nm in constants.extract 0 100 do
      let ranges ← findDeclarationRanges? nm
      definitions := definitions.push (Json.mkObj [
        ("name", toJson nm.toString), ("module", toJson (moduleOf env nm)),
        ("source", match ranges with
          | some r => Json.mkObj [("first_line", toJson r.range.pos.line), ("last_line", toJson r.range.endPos.line)]
          | none => Json.null)])
    return some (Json.mkObj ((← readableFields "conclusion" conclusion) ++ [
      ("version", toJson (1 : Nat)), ("theorem", toJson n.toString),
      ("module", toJson (moduleOf env n)), ("statement", toJson full),
      ("binders", toJson binders),
      ("program", program), ("program_head", head),
      ("axioms", toJson (axioms.map Name.toString)),
      ("first_line", toJson ranges.range.pos.line), ("last_line", toJson ranges.range.endPos.line),
      ("definitions", toJson definitions), ("definitions_truncated", toJson (decide (constants.size > 100))),
      ("translation_rerun", toJson false)]))
end ProofsProbe

run_cmd do
  let manual : Array Name := #[`adler2.new_spec, `adler2.checksum_spec, `adler2.from_checksum_spec, `adler2.write_slice_spec, `adler2.adler32_slice_spec]
  let localModules : Array String := #[]
  let roots : Array Name := #[]
  let env ← getEnv
  let mut closure : Array Name := #[]
  let mut pending := roots.toList
  while !pending.isEmpty do
    let m := pending.head!
    pending := pending.tail!
    if !closure.contains m then
      closure := closure.push m
      if let some idx := env.header.moduleNames.findIdx? (· == m) then
        pending := (env.header.moduleData[idx]!.imports.toList.map (·.module)) ++ pending
  let scope := closure.filter (fun m => localModules.contains m.toString)
  for n in manual do
    match env.find? n with
    | some (.thmInfo _) => pure ()
    | _ => throwError "Expected a theorem: {n}"
  for (n, ci) in env.constants.toList do
    let explicit := manual.contains n
    if explicit || scope.contains (ProofsProbe.moduleOf env n).toName then
      if let .thmInfo th := ci then
        let result ← liftTermElabM <| ProofsProbe.inspect n th.type explicit
        if let some value := result then
          liftIO <| IO.println ("proofs.rs:formal:" ++ value.compress)

run_cmd do
  let theorem_name := `adler2.checksum_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: adler2.checksum_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in adler2.checksum_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:adler2.checksum_spec"

run_cmd do
  let theorem_name := `adler2.from_checksum_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: adler2.from_checksum_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in adler2.from_checksum_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:adler2.from_checksum_spec"

run_cmd do
  let theorem_name := `adler2.new_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: adler2.new_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in adler2.new_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:adler2.new_spec"

run_cmd do
  let theorem_name := `adler2.write_slice_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: adler2.write_slice_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in adler2.write_slice_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:adler2.write_slice_spec"

run_cmd do
  let theorem_name := `adler2.adler32_slice_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: adler2.adler32_slice_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in adler2.adler32_slice_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:adler2.adler32_slice_spec"
' | lake env lean --stdin

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 5 checks passed · 0 failed

2026-10-20T06:41:02.924098+00:00 · 570.3 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem adler2.checksum_spec; axioms limited to propext, Classical.choice, Quot.sound `adler2.checksum_spec`	Passed	Claim #1
Lean checked theorem adler2.from_checksum_spec; axioms limited to propext, Classical.choice, Quot.sound `adler2.from_checksum_spec`	Passed	Claim #2
Lean checked theorem adler2.new_spec; axioms limited to propext, Classical.choice, Quot.sound `adler2.new_spec`	Passed	Claim #3
Lean checked theorem adler2.write_slice_spec; axioms limited to propext, Classical.choice, Quot.sound `adler2.write_slice_spec`	Passed	Claim #4
Lean checked theorem adler2.adler32_slice_spec; axioms limited to propext, Classical.choice, Quot.sound `adler2.adler32_slice_spec`	Passed	Claim #5

Execution details

Started: 2026-10-20T06:41:02.924098+00:00
Finished: 2026-10-20T06:50:33.270925+00:00
Platform: macos aarch64
Rust compiler: rustc 1.91.1 (ed61e7d7e 2025-11-07) binary: rustc commit-hash: ed61e7d7e242494fb7057f2657300d9e77bb4fcb commit-date: 2025-11-07 host: aarch64-apple-darwin release: 1.91.1 LLVM version: 21.1.2
Working directory: adler2/2.0.1/proofs
Environment overrides: None recorded
Git repository: https://github.com/keiichiw/crate-proofs
Git commit: 5c4e0f729b5bd557451157346250211069968474

Diagnostics & logs

=== stdout ===
⚠ [2/11] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [4/67] Built AeneasMeta.Simp.RegisterCommand (662ms)
✔ [5/67] Built Aeneas.Data.Coinductive.Effect (669ms)
✔ [8/73] Built Aeneas.Tactic.Solver.Grind.Attribute (775ms)
✔ [9/74] Built AeneasMeta.Simp.RegisterCommand:c.o (500ms)
✔ [10/74] Built AeneasMeta.BvEnumToBitVec (1.1s)
✔ [11/76] Built AeneasMeta.Simp.RegisterCommand:dynlib (199ms)
✔ [12/78] Built AeneasMeta.BvEnumToBitVec:c.o (362ms)
✔ [13/78] Built Qq.Typ (568ms)
✔ [14/83] Built AeneasMeta.BvEnumToBitVec:dynlib (100ms)
✔ [15/83] Built Qq.ForLean.ReduceEval (731ms)
✔ [16/83] Built Qq.ForLean.ToExpr (670ms)
✔ [17/83] Built AeneasMeta.OptionConfig (1.8s)
✔ [18/83] Built Qq.ForLean.Do (533ms)
✔ [19/83] Built Qq.SortLocalDecls (522ms)
✔ [20/83] Built Aeneas.Std.Global (2.1s)
✔ [21/83] Built AeneasMeta.UtilsCore (2.1s)
✔ [24/91] Built AeneasMeta.UtilsCore:c.o (198ms)
✔ [25/92] Built AeneasMeta.UtilsCore:dynlib (179ms)
✔ [26/92] Built Aeneas.Tactic.Solver.Grind.Init (1.5s)
✔ [27/92] Built Batteries.Util.LibraryNote (594ms)
✔ [28/92] Built AeneasMeta.OptionConfig:c.o (1.1s)
✔ [29/92] Built Batteries.CodeAction.Deprecated (726ms)
✔ [32/95] Built Batteries.Tactic.Lint.Basic (718ms)
✔ [33/98] Built AeneasMeta.OptionConfig:dynlib (254ms)
✔ [34/101] Built Aeneas.Data.Coinductive.CoInd (3.1s)
✔ [35/102] Built ImportGraph.Lean.MessageData (544ms)
✔ [36/105] Built ImportGraph.Lean.Syntax (612ms)
✔ [37/105] Built ImportGraph.Lean.EnvExtension (516ms)
✔ [38/106] Built Batteries.Tactic.Lint.Misc (871ms)
✔ [39/106] Built ImportGraph.Shake.Core (740ms)
✔ [40/111] Built Batteries.Tactic.HelpCmd (1.4s)
✔ [41/112] Built Batteries.Tactic.Alias (1.4s)
✔ [42/116] Built Aeneas.Data.Coinductive.ITree (1.2s)
✔ [43/116] Built ImportGraph.Lean.Json (820ms)
✔ [44/116] Built ImportGraph.Util.Modules (720ms)
✔ [45/117] Built ImportGraph.Shake.EnvExtension (696ms)
✔ [46/119] Built Qq.Macro (3.0s)
✔ [47/120] Built ImportGraph.Imports.ImportGraph (478ms)
✔ [48/120] Built ImportGraph.Graph.TransitiveClosure (402ms)
✔ [49/120] Built ImportGraph.Lean.Environment (526ms)
✔ [50/120] Built ImportGraph.Imports.Pretty (1.4s)
✔ [51/120] Built ImportGraph.Shake.Basic (895ms)
✔ [52/122] Built ImportGraph.Widget.Collapsible (667ms)
✔ [53/122] Built ImportGraph.WorkspaceModel.Base (776ms)
✔ [54/122] Built ImportGraph.Widget.Copy (907ms)
✔ [55/125] Built ImportGraph.Widget.GoToModule (866ms)
✔ [56/125] Built Qq.Commands (1.1s)
✔ [57/125] Built ImportGraph.Tools.ImportDiff (851ms)
✔ [58/132] Built Qq.Delab (1.1s)
✔ [59/132] Built ImportGraph.Imports.RequiredModules (921ms)
✔ [60/132] Built ImportGraph.Imports.Redundant (509ms)
✔ [61/133] Built ImportGraph.Shake.Algebra (863ms)
✔ [62/134] Built ImportGraph.Imports.FromSource (584ms)
✔ [63/148] Built Batteries.Util.ProofWanted (2.6s)
✔ [64/148] Built ImportGraph.WorkspaceModel.Summary.Core (722ms)
✔ [65/152] Built ImportGraph.WorkspaceModel.Model (953ms)
✔ [66/154] Built Qq.MetaM (917ms)
✔ [67/154] Built ImportGraph.Tools.RedundantImports (774ms)
✔ [68/155] Built ImportGraph.Tools.MinImports (783ms)
✔ [69/155] Built Batteries.Lean.Position (470ms)
✔ [70/156] Built ImportGraph.WorkspaceModel.Summary.Cache (543ms)
✔ [71/156] Built Mathlib.Tactic.Linter.DirectoryDependency (1.1s)
✔ [72/162] Built Batteries.Tactic.Lint.TypeClass (607ms)
✔ [73/163] Built ImportGraph.WorkspaceModel.Summary.Get (504ms)
✔ [74/167] Built Qq.Simp (738ms)
✔ [75/167] Built Qq.MatchImpl (739ms)
✔ [76/167] Built ImportGraph.Shake.DeclNeeds (2.6s)
✔ [77/176] Built AeneasMeta.Utils (5.4s)
✔ [78/176] Built Qq.AssertInstancesCommute (959ms)
✔ [79/176] Built Batteries.Tactic.Lint.Simp (1.2s)
✔ [80/176] Built Batteries.Tactic.Unreachable (569ms)
✔ [81/179] Built ImportGraph.WorkspaceModel.Summary (380ms)
✔ [82/181] Built Batteries.Tactic.Lint.Frontend (1.4s)
✔ [83/181] Built Mathlib.Tactic.Linter.Header (1.2s)
✔ [84/181] Built Batteries.Lean.Meta.Inaccessible (483ms)
✔ [85/181] Built Aeneas.Data.Coinductive.ITreeWP.EffectWP (530ms)
✔ [86/181] Built Batteries.Tactic.Lint (640ms)
✔ [87/181] Built ImportGraph.WorkspaceModel.Build (896ms)
✔ [88/181] Built Mathlib.Tactic.TypeStar (686ms)
✔ [89/181] Built Batteries.Logic (824ms)
✔ [90/181] Built ImportGraph.Shake.Environment (1.5s)
✔ [91/181] Built Mathlib.Util.CodeActions.BinderPlicity (829ms)
✔ [92/181] Built Aeneas.Tactic.Step.Trace (1.2s)
✔ [93/181] Built Mathlib.Lean.Elab.Tactic.Meta (611ms)
✔ [94/181] Built Mathlib.Util.ParseCommand (716ms)
✔ [95/181] Built Mathlib.Tactic.Linter.PrivateModule (719ms)
✔ [96/181] Built Mathlib.Tactic.Linter.TacticDocumentation (712ms)
✔ [97/181] Built Mathlib.Tactic.Linter.UnusedTacticExtension (858ms)
✔ [98/181] Built Mathlib.Tactic.DeclarationNames (642ms)
✔ [99/181] Built Mathlib.Tactic.Linter.OldObtain (785ms)
✔ [100/181] Built Mathlib.Tactic.MinImports (1.1s)
✔ [101/181] Built Mathlib.Tactic.Linter.Multigoal (925ms)
✔ [102/181] Built Mathlib.Tactic.Linter.Whitespace (1.2s)
✔ [103/181] Built Mathlib.Tactic.Linter.InternalConstructor (624ms)
✔ [104/181] Built Qq.Match (2.7s)
✔ [105/181] Built Mathlib.Tactic.Linter.HashCommandLinter (845ms)
✔ [106/181] Built Mathlib.Tactic.Linter.HaveILetI (866ms)
✔ [107/181] Built Mathlib.Lean.Environment (566ms)
✔ [108/181] Built Mathlib.Tactic.Linter.EmptyLine (945ms)
✔ [109/181] Built Mathlib.Tactic.Linter.DocString (1.1s)
✔ [110/182] Built Mathlib.Tactic.Lemma (521ms)
✔ [111/182] Built Mathlib.Tactic.Linter.AuxLemma (630ms)
✔ [112/182] Built Mathlib.Tactic.Linter.DeprecatedSyntaxLinter (1.0s)
✔ [113/182] Built Mathlib.Lean.Expr.Basic (1.1s)
✔ [114/182] Built Mathlib.Tactic.Linter.DocPrime (1.4s)
✔ [115/182] Built Mathlib.Tactic.Linter.FlexibleLinter (1.6s)
✔ [116/182] Built Mathlib.Lean.Linter (635ms)
✔ [117/182] Built Mathlib.Tactic.AdaptationNote (835ms)
✔ [118/182] Built Mathlib.Util.CodeActions (634ms)
✔ [119/184] Built Mathlib.Lean.ContextInfo (773ms)
✔ [120/184] Built ImportGraph.Tools.NormImports (918ms)
✔ [121/213] Built Qq (512ms)
✔ [122/213] Built ImportGraph.Shake.Workspace (1.2s)
✔ [123/213] Built Mathlib.Tactic.Linter.UnusedTactic (941ms)
✔ [124/218] Built Mathlib.Lean.Elab.InfoTree (599ms)
✔ [125/218] Built Mathlib.Tactic.Linter.Lint (828ms)
✔ [126/238] Built Mathlib.Tactic.ExtractGoal (1.1s)
✔ [127/250] Built Batteries.Lean.NameMapAttribute (574ms)
✔ [128/251] Built Mathlib.Tactic.Linter.Style (1.4s)
✔ [129/251] Built Mathlib.Tactic.TacticAnalysis (994ms)
✔ [130/260] Built Batteries.Lean.Expr (615ms)
✔ [131/260] Built Batteries.Lean.Syntax (350ms)
✔ [132/260] Built Batteries.Util.ExtendedBinder (709ms)
✔ [133/260] Built Mathlib.Tactic.Linter.UnusedInstancesInType (972ms)
✔ [134/260] Built Batteries.Tactic.Trans (1.3s)
✔ [135/260] Built Batteries.Tactic.Init (962ms)
✔ [136/260] Built Batteries.Linter.UnreachableTactic (616ms)
✔ [137/260] Built ImportGraph.Tools.FindHome (1.3s)
✔ [140/267] Built AeneasMeta.Utils:c.o (6.1s)
✔ [141/273] Built AeneasMeta.Utils:dynlib (210ms)
✔ [142/273] Built ImportGraph.Tools (663ms)
✔ [143/273] Built Aesop.Script.Tactic (694ms)
✔ [144/273] Built Batteries.Control.Lemmas (490ms)
✔ [145/275] Built Mathlib.Tactic.Linter.OverlappingInstances (1.2s)
✔ [146/275] Built Aesop.Script.GoalWithMVars (634ms)
✔ [147/275] Built Aesop.Nanos (555ms)
✔ [148/281] Built Mathlib.Tactic.TacticAnalysis.Declarations (1.7s)
✔ [149/281] Built Aesop.Index.DiscrTreeConfig (560ms)
✔ [150/284] Built Batteries.Data.Array.Merge (785ms)
✔ [151/286] Built Batteries.Tactic.PermuteGoals (891ms)
✔ [152/286] Built Batteries.Lean.MonadBacktrack (583ms)
✔ [153/291] Built Batteries.Control.AlternativeMonad (700ms)
✔ [154/291] Built Aesop.Check (574ms)
✔ [155/296] Built Mathlib.Tactic.Linter.DeclType (769ms)
✔ [156/296] Built Aesop.Options.Public (645ms)
✔ [157/300] Built AeneasMeta.Extensions (1.5s)
✔ [158/300] Built Aesop.Util.UnorderedArraySet (660ms)
✔ [159/300] Built Aesop.Rule.Name (872ms)
✔ [160/300] Built Aesop.Forward.LevelIndex (452ms)
✔ [161/301] Built Batteries.Lean.Meta.Basic (675ms)
✔ [162/301] Built Aesop.Script.OptimizeSyntax (759ms)
✔ [163/301] Built Aesop.Forward.PremiseIndex (472ms)
✔ [164/302] Built AeneasMeta.Async.Async (1.9s)
✔ [165/302] Built AeneasMeta.Extensions:c.o (316ms)
✔ [166/302] Built Aesop.Options.Internal (461ms)
✔ [167/302] Built AeneasMeta.Simp.Simp (1.8s)
✔ [168/302] Built Aesop.Percent (598ms)
✔ [169/303] Built AeneasMeta.Extensions:dynlib (210ms)
✔ [170/303] Built Mathlib.Init (961ms)
✔ [171/303] Built Aesop.Forward.SlotIndex (537ms)
✔ [172/303] Built Batteries.Lean.Meta.SavedState (601ms)
✔ [173/303] Built AeneasMeta.Async.Async:c.o (485ms)
✔ [174/303] Built Aesop.Script.TacticState (618ms)
✔ [175/303] Built AeneasMeta.Async.Async:dynlib (135ms)
✔ [176/303] Built Aesop.Util.UnionFind (542ms)
✔ [177/303] Built Aesop.Util.Basic (1.4s)
✔ [178/303] Built AeneasMeta.Simp.Simp:c.o (1.1s)
✔ [179/303] Built Mathlib.Lean.Elab.Term (1.0s)
✔ [180/303] Built Mathlib.Util.WithWeakNamespace (931ms)
✔ [181/303] Built Mathlib.Tactic.Eqns (945ms)
✔ [182/303] Built Mathlib.Tactic.Core (1.5s)
✔ [183/303] Built Mathlib.Tactic.SimpRw (1.2s)
✔ [184/303] Built Aesop.Util.EqualUpToIds (2.2s)
✔ [185/303] Built Mathlib.Tactic.Inhabit (930ms)
✔ [186/303] Built Mathlib.Tactic.Simps.NotationClass (1.3s)
✔ [187/303] Built Mathlib.Tactic.Use (1.7s)
✔ [188/303] Built Mathlib.Lean.PrettyPrinter.Delaborator (989ms)
✔ [189/303] Built Mathlib.Tactic.ExtendDoc (1.1s)
✔ [190/303] Built Mathlib.Basic.Nonempty (874ms)
✔ [191/303] Built Mathlib.Basic.IsEmpty.Defs (1.0s)
✔ [192/303] Built Mathlib.Tactic.OfNat (940ms)
✔ [193/303] Built Mathlib.Basic.ExistsUnique (1.3s)
✔ [194/303] Built Mathlib.Data.Int.Notation (1.0s)
✔ [195/303] Built Mathlib.Data.Nat.Notation (899ms)
✔ [196/303] Built Mathlib.Tactic.Attr.Register (1.3s)
✔ [197/303] Built AeneasMeta.Saturate.Attribute (3.2s)
✔ [198/303] Built Mathlib.Tactic.Push.Attr (1.3s)
✔ [199/303] Built Mathlib.Data.Nat.BinaryRec (1.1s)
✔ [200/303] Built Mathlib.Lean.Meta (1.0s)
✔ [201/303] Built Mathlib.Tactic.CrossRefAttribute (1.8s)
✔ [202/303] Built AeneasMeta.Simp.Simp:dynlib (152ms)
✔ [203/303] Built Mathlib.Data.String.Defs (956ms)
✔ [204/303] Built Mathlib.Tactic.Translate.Attributes (1.1s)
✔ [205/303] Built Mathlib.Util.AddRelatedDecl (1.5s)
✔ [206/303] Built Mathlib.Lean.Name (1.0s)
✔ [207/303] Built Mathlib.Tactic.Translate.UnfoldBoundary (1.7s)
✔ [208/303] Built Mathlib.Lean.Meta.Simp (1.2s)
✔ [209/306] Built Mathlib.Tactic.Simproc.ExistsAndEq (1.7s)
✔ [210/307] Built Aesop.Tracing (1.0s)
✔ [211/307] Built Aesop.Forward.Substitution (1.0s)
✔ [212/307] Built Aesop.Script.Util (693ms)
✔ [213/307] Built Mathlib.Tactic.SplitIfs (1.1s)
✔ [214/313] Built Mathlib.Tactic.Translate.Reorder (2.4s)
✔ [215/313] Built Mathlib.Basic.Nontrivial.Defs (845ms)
✔ [216/313] Built Mathlib.Logic.Function.Defs (1.3s)
✔ [217/313] Built Batteries.Lean.TagAttribute (502ms)
✔ [218/316] Built Mathlib.Tactic.ScopedNS (1.9s)
✔ [219/316] Built Aesop.RulePattern.Cache (561ms)
✔ [220/320] Built AeneasMeta.Saturate.Attribute:c.o (2.2s)
✔ [221/320] Built Mathlib.Tactic.Translate.GuessName (1.3s)
✔ [222/320] Built Aesop.Index.Basic (713ms)
✔ [223/320] Built Mathlib.Tactic.MkIffOfInductiveProp (1.5s)
✔ [224/320] Built AeneasMeta.Simp.SimpAllAssumptions (1.0s)
✔ [225/320] Built AeneasMeta.Saturate.Attribute:dynlib (209ms)
✔ [226/320] Built Batteries.Lean.AttributeExtra (678ms)
✔ [227/320] Built Batteries.Tactic.SeqFocus (979ms)
✔ [228/320] Built Aesop.Script.Step (1.4s)
✔ [229/320] Built Aesop.Stats.Basic (1.4s)
✔ [230/320] Built Aesop.RuleTac.RuleTerm (620ms)
✔ [231/322] Built Mathlib.Basic.Logic.Basic (2.1s)
✔ [232/322] Built Mathlib.Logic.Relator (1.4s)
✔ [233/322] Built Aesop.Script.CtorNames (707ms)
✔ [234/322] Built AeneasMeta.Simp.SimpAllAssumptions:c.o (1.1s)
✔ [235/322] Built Aesop.BaseM (729ms)
✔ [236/324] Built AeneasMeta.Simp.SimpAllAssumptions:dynlib (171ms)
✔ [237/324] Built Aesop.Script.UScript (740ms)
✔ [238/324] Built Aesop.Script.SScript (908ms)
✔ [239/324] Built Batteries.Linter.UnnecessarySeqFocus (1.1s)
✔ [240/325] Built Aesop.ElabM (595ms)
✔ [241/325] Built Mathlib.Tactic.SetNotationForOrder (1.8s)
✔ [242/325] Built Mathlib.Tactic.Simps.Basic (3.9s)
✔ [243/325] Built Aesop.Util.Tactic.Ext (707ms)
✔ [244/325] Built Aesop.Script.Check (673ms)
✔ [245/325] Built Aesop.RuleTac.GoalDiff (1.0s)
✔ [246/325] Built Aesop.Script.ScriptM (749ms)
✔ [247/328] Built Mathlib.Tactic.Translate.Expr (2.3s)
✔ [248/329] Built Aesop.RulePattern (1.4s)
✔ [249/329] Built Batteries.Linter (630ms)
✔ [250/329] Built AeneasMeta.Simp (1.5s)
✔ [251/329] Built Aesop.Util.Tactic (603ms)
✔ [252/332] Built AeneasMeta.Simp:c.o (147ms)
✔ [253/332] Built Aesop.RuleTac.ElabRuleTerm (875ms)
✔ [254/334] Built AeneasMeta.Simp:dynlib (157ms)
✔ [255/334] Built Aesop.Script.UScriptToSScript (1.1s)
✔ [256/334] Built Aesop.RuleTac.Basic (803ms)
✔ [257/334] Built Aesop.Util.Unfold (882ms)
✔ [258/338] Built Mathlib.Tactic.Simps (1.1s)
✔ [259/338] Built Batteries.Tactic.Basic (605ms)
✔ [260/338] Built Aesop.RuleTac.Forward.Basic (760ms)
✔ [261/339] Built Batteries.Lean.Meta.UnusedNames (672ms)
✔ [262/339] Built Aesop.Constants (444ms)
✔ [263/340] Built Aesop.Script.StructureStatic (909ms)
✔ [264/344] Built Aesop.Util.OrderedHashSet (459ms)
✔ [265/346] Built Aesop.Util.Tactic.Unfold (806ms)
✔ [266/347] Built Aesop.EMap (861ms)
✔ [267/349] Built Aesop.Script.StructureDynamic (1.4s)
✔ [268/349] Built Batteries.Classes.Order (928ms)
✔ [269/349] Built Batteries.Lean.Meta.Expr (444ms)
✔ [270/351] Built Batteries.Lean.PersistentHashMap (529ms)
✔ [271/359] Built Mathlib.Util.Notation3 (5.5s)
✔ [272/359] Built Batteries.Lean.Meta.InstantiateMVars (533ms)
✔ [273/359] Built Batteries.Lean.PersistentHashSet (471ms)
✔ [274/366] Built AeneasMeta.Saturate.Tactic (4.8s)
✔ [275/367] Built Aesop.RuleSet.Name (458ms)
✔ [276/369] Built AeneasMeta.Async.TestTactics (2.1s)
✔ [277/369] Built Aesop.Script.Main (945ms)
✔ [278/369] Built Batteries.Data.UInt (944ms)
✔ [279/369] Built Batteries.Lean.Meta.DiscrTree (610ms)
✔ [280/369] Built Batteries.Lean.HashSet (545ms)
✔ [281/374] Built Aesop.RuleSet.Filter (452ms)
✔ [282/383] Built AeneasMeta.Async.TestTactics:c.o (389ms)
✔ [283/383] Built Aesop.RuleTac.Tactic (782ms)
✔ [284/383] Built Aesop.Search.Expansion.Basic (631ms)
✔ [285/383] Built Aesop.Search.Expansion.Simp (550ms)
✔ [286/400] Built AeneasMeta.Async.TestTactics:dynlib (171ms)
✔ [287/401] Built Aesop.Script.SpecificTactics (1.7s)
✔ [288/401] Built Aesop.Exception (497ms)
✔ [289/401] Built Batteries.Control.ForInStep.Basic (484ms)
✔ [290/402] Built Aesop.Index.RulePattern (972ms)
✔ [291/404] Built Aesop.Stats.Extension (618ms)
✔ [292/407] Built Aesop.Stats.File (984ms)
✔ [293/421] Built Aesop.RuleTac.Preprocess (1.1s)
✔ [294/434] Built Aesop.RuleTac.Cases (1.2s)
✔ [295/443] Built Aesop.RuleTac.Apply (1.2s)
✔ [296/443] Built Aesop.Frontend.Basic (903ms)
✔ [297/446] Built Aesop.Stats.Report (1.0s)
✔ [298/446] Built Mathlib.Tactic.Translate.Core (5.5s)
✔ [299/446] Built Batteries.Data.Array.Basic (2.8s)
✔ [300/446] Built Mathlib.Tactic.Spread (1.2s)
✔ [301/446] Built Mathlib.Tactic.Attr.Core (1.1s)
✔ [302/451] Built Mathlib.Tactic.Conv (1.7s)
✔ [303/451] Built Mathlib.Tactic.Lift (1.4s)
✔ [304/454] Built Mathlib.Tactic.Translate.TagUnfoldBoundary (1.5s)
✔ [305/454] Built Mathlib.Tactic.Subsingleton (1.5s)
✔ [306/454] Built Aesop.Forward.RuleInfo (1.4s)
✔ [307/454] Built Mathlib.Tactic.Translate.ToAdditive (1.7s)
✔ [308/454] Built Mathlib.Util.AtLocation (1.4s)
✔ [309/458] Built Aesop.Rule.Forward (905ms)
✔ [310/458] Built Mathlib.Tactic.DepRewrite (3.8s)
✔ [311/459] Built Mathlib.Util.CompileInductive (1.0s)
✔ [312/462] Built Mathlib.Tactic.ToAdditive (1.4s)
✔ [313/462] Built Mathlib.Lean.Meta.CongrTheorems (2.0s)
✔ [314/463] Built Mathlib.Tactic.Translate.ToDual (2.1s)
✔ [315/463] Built Batteries.Data.BinomialHeap.Basic (5.4s)
✔ [316/463] Built Aesop.Forward.Match.Types (872ms)
✔ [317/468] Built Mathlib.Tactic.Relation.Rfl (1.3s)
✔ [318/468] Built Mathlib.Control.Combinators (1.2s)
✔ [319/468] Built Mathlib.Data.Option.Defs (1.3s)
✔ [320/468] Built Mathlib.Algebra.Regular.Defs (1.4s)
✔ [321/468] Built Mathlib.Data.Int.Init (2.1s)
✔ [322/468] Built Mathlib.Tactic.Push (2.8s)
✔ [323/468] Built Mathlib.Algebra.Notation.Defs (1.9s)
✔ [324/468] Built Aesop.RuleTac.Descr (881ms)
✔ [325/468] Built Aesop.Index.Forward (1.2s)
✔ [326/468] Built Mathlib.Tactic.ToDual (1.6s)
✔ [327/468] Built Aesop.Rule.Basic (903ms)
✔ [328/468] Built Mathlib.Tactic.Coe (1.5s)
✔ [329/468] Built Mathlib.Tactic.Contrapose (1.7s)
✔ [330/472] Built Mathlib.Algebra.Notation.Pi.Defs (1.9s)
✔ [331/472] Built Mathlib.Tactic.TermCongr (3.8s)
✔ [332/473] Built Mathlib.Algebra.Group.Semigroup (2.2s)
✔ [333/473] Built Mathlib.Data.Set.Defs (2.1s)
✔ [334/473] Built Mathlib.Order.Defs.Prop (1.4s)
✔ [335/473] Built Aesop.Rule (1.0s)
✔ [336/473] Built Aesop.Index (1.4s)
✔ [337/475] Built Mathlib.Tactic.CongrExclamation (3.3s)
✔ [338/475] Built Mathlib.Data.Ordering.Basic (1.4s)
✔ [339/476] Built Aesop.RuleSet.Member (886ms)
✔ [340/478] Built Aesop.Forward.Match (1.4s)
✔ [341/478] Built Mathlib.Order.Defs.PartialOrder (2.1s)
✔ [342/478] Built Mathlib.Order.Notation (1.0s)
✔ [343/478] Built Aesop.Tree.UnsafeQueue (972ms)
✔ [344/478] Built AeneasMeta.Saturate.Tactic:c.o (13s)
✔ [345/478] Built Mathlib.Order.Defs.Unbundled (1.0s)
✔ [346/478] Built Batteries.Data.Except (646ms)
✔ [347/478] Built Mathlib.Tactic.FastInstance (2.2s)
✔ [348/478] Built AeneasMeta.Saturate.Tactic:dynlib (162ms)
✔ [349/478] Built Aesop.Builder.Basic (1.0s)
✔ [350/480] Built Aesop.Tree.Data.ForwardRuleMatches (889ms)
✔ [351/480] Built Batteries.Tactic.Exact (739ms)
✔ [352/480] Built Mathlib.Algebra.Group.Monoid (3.2s)
✔ [353/480] Built Mathlib.Tactic.GCongr.ForwardAttr (1.5s)
✔ [354/480] Built Batteries.Lean.Except (815ms)
✔ [355/480] Built Mathlib.Order.Defs.LinearOrder (2.2s)
✔ [356/480] Built Aesop.Builder.Unfold (919ms)
✔ [357/480] Built Aesop.RuleTac.Forward (2.0s)
✔ [358/480] Built Aesop.Builder.Apply (761ms)
✔ [359/480] Built Mathlib.Tactic.Convert (2.9s)
✔ [360/480] Built Aesop.Builder.Tactic (783ms)
✔ [361/480] Built Aesop.Builder.Forward (1.4s)
✔ [362/487] Built Aesop.Builder.NormSimp (807ms)
✔ [363/487] Built Aesop.Builder.Constructors (996ms)
✔ [364/487] Built Aesop.Builder.Cases (1.2s)
✔ [365/487] Built Mathlib.Logic.Function.Basic (2.5s)
✔ [366/487] Built Batteries.Data.MLList.Basic (1.1s)
✔ [367/489] Built Mathlib.Logic.Relation (2.8s)
✔ [368/489] Built Aesop.RuleTac (590ms)
✔ [369/489] Built AeneasMeta.Saturate (2.1s)
✔ [370/489] Built Aesop.Builder.Default (700ms)
✔ [371/489] Built Mathlib.Algebra.Group.DivInvMonoid (2.0s)
✔ [372/489] Built Mathlib.Tactic.PPWithUniv (1.2s)
✔ [373/490] Built Aesop.Forward.State (4.9s)
✔ [374/490] Built Mathlib.Data.Sigma.Basic (1.5s)
✔ [375/490] Built Mathlib.Algebra.Notation.Pi.Basic (1.7s)
✔ [376/491] Built AeneasMeta.Saturate:c.o (207ms)
✔ [377/491] Built Aesop.RuleSet (3.1s)
✔ [378/491] Built Mathlib.Data.Sum.Basic (1.5s)
✔ [379/491] Built Mathlib.Basic.Unique (1.5s)
✔ [380/491] Built Batteries.Control.Nondet.Basic (955ms)
✔ [381/493] Built AeneasMeta.Saturate:dynlib (185ms)
✔ [382/493] Built Mathlib.Logic.Function.Conjugate (1.5s)
✔ [383/493] Built Mathlib.Data.Subtype (1.6s)
✔ [384/493] Built Mathlib.Logic.Function.ULift (1.1s)
✔ [385/493] Built Mathlib.Tactic.ByCases (1.1s)
✔ [386/493] Built Mathlib.Algebra.Group.Defs (1.6s)
✔ [387/493] Built Aesop.Forward.State.Initial (812ms)
✔ [388/493] Built Aesop.Frontend.Extension.Init (816ms)
✔ [389/493] Built Mathlib.Tactic.Basic (1.5s)
✔ [390/494] Built Aesop.Tree.Data (1.6s)
✔ [391/494] Built Aesop.Forward.State.ApplyGoalDiff (1.0s)
✔ [392/494] Built Mathlib.Tactic.GCongr.Core (4.6s)
✔ [393/494] Built Aesop.Frontend.RuleExpr (2.3s)
✔ [394/494] Built Mathlib.Basic.FunLike.Basic (1.1s)
✔ [395/495] Built Mathlib.Logic.Function.Iterate (1.2s)
✔ [396/495] Built Mathlib.Data.Quot (1.9s)
✔ [397/495] Built Aesop.Frontend.Extension (1.1s)
✔ [398/495] Built Mathlib.Tactic.Basify.Attr (1.6s)
✔ [399/495] Built Mathlib.Algebra.Group.Semiconj.Defs (1.4s)
✔ [400/495] Built Aesop.Tree.TreeM (755ms)
✔ [401/495] Built Aesop.Tree.Traversal (762ms)
✔ [402/495] Built Mathlib.Tactic.Hint (1.5s)
✔ [403/495] Built Aesop.Search.Queue.Class (770ms)
✔ [404/495] Built Aesop.Tree.RunMetaM (925ms)
✔ [405/495] Built Mathlib.Algebra.Group.Pi.Basic (2.3s)
✔ [406/495] Built Mathlib.Data.Bool.Basic (1.4s)
✔ [407/495] Built Aesop.Saturate (2.9s)
✔ [408/495] Built Mathlib.Algebra.Group.InjSurj (2.8s)
✔ [409/495] Built Mathlib.Basic.FunLike.Embedding (1.1s)
✔ [410/495] Built Aesop.Tree.Free (823ms)
✔ [411/495] Built Mathlib.Data.Prod.Basic (1.4s)
✔ [412/495] Built Aesop.Frontend.Tactic (1.4s)
✔ [413/495] Built Aesop.Frontend.Attribute (1.4s)
✔ [414/495] Built Mathlib.Logic.Pairwise (1.4s)
✔ [415/495] Built Aesop.Frontend.Command (1.5s)
✔ [416/495] Built Mathlib.Algebra.Group.Commute.Defs (1.6s)
✔ [417/495] Built Aesop.Tree.Stats (748ms)
✔ [418/499] Built Aesop.Tree.State (846ms)
✔ [419/499] Built Aesop.Forward.State.UpdateGoal (780ms)
✔ [420/499] Built Aesop.Tree.ExtractScript (1.3s)
✔ [421/499] Built Mathlib.Tactic.GCongr (1.1s)
✔ [422/499] Built Aesop.Tree.AddRapp (1.4s)
✔ [423/499] Built Aesop.Tree.ExtractProof (1.1s)
✔ [424/499] Built Aesop.Search.SearchM (802ms)
✔ [425/499] Built Aesop.Search.Queue (864ms)
✔ [426/499] Built Aesop.Tree.Tracing (1.2s)
✔ [427/499] Built Aesop.Frontend.Saturate (1.1s)
✔ [428/499] Built Mathlib.Basic.FunLike.Equiv (1.1s)
✔ [429/499] Built Aesop.BuiltinRules.Rfl (875ms)
✔ [430/499] Built Aesop.BuiltinRules.Split (957ms)
✔ [431/499] Built Aesop.BuiltinRules.Subst (1.1s)
✔ [432/499] Built Aesop.BuiltinRules.Intros (934ms)
✔ [433/500] Built Aesop.BuiltinRules.Ext (813ms)
✔ [434/500] Built Mathlib.Algebra.Notation.Prod (1.5s)
✔ [435/500] Built Aesop.BuiltinRules.ApplyHyps (880ms)
✔ [436/500] Built Aesop.BuiltinRules.DestructProducts (1.1s)
✔ [437/500] Built Aesop.BuiltinRules.Assumption (988ms)
✔ [438/500] Built Mathlib.Algebra.Group.Hom.Defs (4.8s)
✔ [439/500] Built Aesop.Search.RuleSelection (737ms)
✔ [440/504] Built Aesop.Tree.Check (1.3s)
✔ [441/505] Built Aesop.Frontend (851ms)
✔ [442/511] Built Aesop.BuiltinRules (945ms)
✔ [443/511] Built Batteries.Data.Nat.Basic (582ms)
✔ [444/511] Built Mathlib.Data.Int.Order.Basic (1.3s)
✔ [445/513] Built Batteries.Data.Nat.Lemmas (663ms)
✔ [446/520] Built Mathlib.Tactic.Finiteness.Attr (1.2s)
✔ [447/522] Built Aesop.Search.Expansion.Norm (1.0s)
✔ [448/522] Built Mathlib.Tactic.ToExpr (1.2s)
✔ [449/522] Built Mathlib.Data.Set.CoeSort (1.0s)
✔ [450/522] Built Mathlib.Algebra.Group.Units.Defs (3.5s)
✔ [451/522] Built Mathlib.Logic.Equiv.Defs (2.9s)
✔ [452/522] Built Mathlib.Tactic.GRewrite.Core (3.5s)
✔ [454/522] Built Mathlib.Basic.IsEmpty.Basic (1.2s)
✔ [455/522] Built Mathlib.Order.Basic (3.8s)
✔ [456/522] Built Mathlib.Data.Nat.Init (1.8s)
✔ [458/522] Built Mathlib.Tactic.Choose (1.6s)
✔ [459/523] Built Aesop.Search.Expansion (1.6s)
✔ [460/523] Built Mathlib.Control.EquivFunctor (1.3s)
✔ [461/524] Built Mathlib.Tactic.FBinop (1.8s)
✔ [462/524] Built Mathlib.Algebra.Opposites (1.9s)
✔ [463/527] Built Mathlib.Tactic.GRewrite.Elab (1.7s)
✔ [464/528] Built Plausible.Random (675ms)
✔ [465/529] Built Aesop.Search.ExpandSafePrefix (1.1s)
✔ [466/529] Built Mathlib.Order.OrderDual (1.8s)
✔ [467/529] Built Mathlib.Order.ULift (1.5s)
✔ [468/531] Built Mathlib.Logic.Equiv.Prod (2.5s)
✔ [469/531] Built Mathlib.Data.Nat.Basic (1.4s)
✔ [470/531] Built Plausible.Shrinkable (613ms)
✔ [471/531] Built Mathlib.Basic.SProd (1.1s)
✔ [472/533] Built Mathlib.Tactic.GRewrite (1.1s)
✔ [473/533] Built Plausible.Gen (963ms)
✔ [474/536] Built Mathlib.Algebra.Group.Equiv.Defs (3.5s)
✔ [475/537] Built Plausible.Attr (604ms)
✔ [476/537] Built Mathlib.Order.Compare (1.4s)
✔ [477/539] Built Plausible.Arbitrary (747ms)
✔ [478/540] Built Aesop.Search.Main (1.9s)
✔ [479/540] Built Mathlib.Order.Max (1.9s)
✔ [480/540] Built Mathlib.Order.RelClasses (2.2s)
✔ [481/545] Built Mathlib.Logic.Equiv.Sum (2.1s)
✔ [482/545] Built Batteries.Tactic.Case (1.3s)
✔ [483/545] Built Mathlib.Order.Defs.Lattice (2.1s)
✔ [484/545] Built Plausible.ArbitraryFueled (695ms)
✔ [485/545] Built Plausible.DeriveShrinkable (1.9s)
✔ [486/545] Built Batteries.CodeAction.Attr (1.1s)
✔ [487/545] Built Plausible.Sampleable (845ms)
✔ [490/546] Built Aesop.Main (1.1s)
✔ [491/547] Built Batteries.Tactic.GeneralizeProofs (2.3s)
✔ [492/550] Built Plausible.Functions (906ms)
✔ [493/550] Built Batteries.CodeAction.Basic (996ms)
✔ [494/555] Built Mathlib.Order.BoundedOrder.Basic (2.3s)
✔ [495/555] Built Plausible.DeriveArbitrary (1.8s)
✔ [496/555] Built LeanSearchClient.Basic (825ms)
✔ [497/555] Built Aesop (1.1s)
✔ [498/556] Built Batteries.CodeAction.Misc (2.2s)
✔ [499/556] Built Plausible.Testable (2.0s)
✔ [500/557] Built Mathlib.Tactic.ApplyCongr (1.4s)
✔ [501/557] Built Batteries.Data.List.Basic (2.8s)
✔ [502/558] Built Mathlib.Data.Set.Operations (2.3s)
✔ [503/558] Built Mathlib.Lean.Meta.Basic (1.2s)
✔ [504/559] Built Mathlib.Tactic.ApplyWith (1.4s)
✔ [505/559] Built Mathlib.Tactic.ByContra (1.3s)
✔ [506/559] Built Mathlib.Tactic.CasesM (1.5s)
✔ [507/559] Built Plausible.Tactic (901ms)
✔ [508/559] Built LeanSearchClient.Syntax (1.8s)
✔ [509/560] Built Mathlib.Data.Option.Basic (1.6s)
✔ [510/560] Built Mathlib.Tactic.ClearExclamation (995ms)
✔ [511/560] Built Mathlib.Tactic.Check (1.5s)
✔ [512/561] Built Batteries.CodeAction.Match (1.1s)
✔ [513/561] Built Mathlib.Tactic.ClearExcept (1.1s)
✔ [514/562] Built Plausible (756ms)
✔ [515/562] Built Mathlib.Tactic.Clear_ (1.0s)
✔ [516/564] Built Mathlib.Tactic.ApplyAt (1.2s)
✔ [517/576] Built Batteries.CodeAction (729ms)
✔ [518/576] Built LeanSearchClient.LoogleSyntax (1.4s)
✔ [522/576] Built Mathlib.Lean.GoalsLocation (1.1s)
✔ [524/576] Built Mathlib.Lean.Meta.KAbstractPositions (921ms)
✔ [527/576] Built Mathlib.Order.Monotone.Defs (2.1s)
✔ [530/584] Built Mathlib.Logic.Equiv.Option (1.8s)
✔ [531/594] Built Mathlib.Lean.FoldEnvironment (1.2s)
✔ [532/599] Built LeanSearchClient (689ms)
✔ [533/599] Built Mathlib.Lean.Meta.RefinedDiscrTree.Basic (1.4s)
✔ [534/599] Built Mathlib.Tactic.NthRewrite (937ms)
✔ [535/599] Built ProofWidgets.Compat (577ms)
✔ [536/602] Built ProofWidgets.Util (711ms)
✔ [537/602] Built Mathlib.Control.Basic (1.4s)
✔ [538/602] Built Mathlib.Tactic.CongrM (1.3s)
✔ [539/603] Built Mathlib.Tactic.Constructor (1.3s)
✔ [540/604] Built Mathlib.Algebra.Group.Basic (5.1s)
✔ [541/604] Built Mathlib.Lean.Meta.RefinedDiscrTree.Encode (1.7s)
✔ [542/605] Built ProofWidgets.Component.Basic (1.4s)
✔ [543/605] Built Mathlib.Order.Monotone.Basic (2.5s)
✔ [544/605] Built ProofWidgets.Cancellable (914ms)
✔ [545/605] Built Mathlib.Lean.Meta.RefinedDiscrTree.Initialize (2.1s)
✔ [546/605] Built Mathlib.Lean.MessageData.Trace (1.1s)
✔ [547/606] Built Mathlib.Tactic.DeprecateTo (1.6s)
✔ [548/606] Built Mathlib.Logic.Equiv.Basic (3.6s)
✔ [549/606] Built Mathlib.Tactic.DefEqTransformations (1.8s)
✔ [550/606] Built Mathlib.Algebra.Group.SelfInv (1.6s)
✔ [551/606] Built Mathlib.Tactic.DSimpPercent (1.1s)
✔ [552/606] Built Mathlib.Algebra.Group.Semiconj.Basic (1.6s)
✔ [553/607] Built Mathlib.Lean.Meta.RefinedDiscrTree.Lookup (1.5s)
✔ [554/607] Built ProofWidgets.Component.MakeEditLink (791ms)
✔ [555/607] Built ProofWidgets.Component.Panel.Basic (962ms)
✔ [556/609] Built Mathlib.Algebra.Group.Units.Basic (2.7s)
✔ [557/609] Built Mathlib.Tactic.ErwQuestion (1.4s)
✔ [558/610] Built Mathlib.Algebra.Group.Hom.Basic (2.6s)
✔ [559/610] Built Mathlib.Tactic.ExistsI (988ms)
✔ [560/610] Built Batteries.Util.Cache (697ms)
✔ [561/611] Built Mathlib.Tactic.DefEqAbuse (1.6s)
✔ [562/613] Built Mathlib.Lean.Meta.RefinedDiscrTree (1.1s)
✔ [563/613] Built ProofWidgets.Data.Html (2.4s)
✔ [564/615] Built Mathlib.Tactic.FailIfNoProgress (1.4s)
✔ [565/615] Built Mathlib.Algebra.Group.Commute.Basic (1.7s)
✔ [566/621] Built Mathlib.Tactic.Find (1.3s)
✔ [567/621] Built Mathlib.Tactic.FunProp.Decl (1.4s)
✔ [568/621] Built Mathlib.Tactic.FunProp.Mor (1.3s)
✔ [569/622] Built ProofWidgets.Component.OfRpcMethod (1.0s)
✔ [570/623] Built Mathlib.Algebra.Group.Units.Hom (2.2s)
✔ [571/624] Built Mathlib.Order.Lattice (3.7s)
✔ [572/624] Built ProofWidgets.Component.RefreshComponent (1.5s)
✔ [573/624] Built Mathlib.Algebra.Group.Equiv.Basic (2.5s)
✔ [574/624] Built ProofWidgets.Component.FilterDetails (850ms)
✔ [575/624] Built Mathlib.Tactic.FunProp.ToBatteries (1.7s)
✔ [576/626] Built Mathlib.Tactic.InferParam (898ms)
✔ [577/626] Built Mathlib.Tactic.GuardGoalNums (980ms)
✔ [578/627] Built Mathlib.Algebra.Group.Torsion (1.5s)
✔ [579/627] Built Mathlib.Tactic.GrindAttrs (1.2s)
✔ [580/628] Built Mathlib.Tactic.GuardHypNums (1.1s)
✔ [581/629] Built Mathlib.Tactic.HigherOrder (1.3s)
✔ [582/631] Built Mathlib.Tactic.FunProp.FunctionData (1.4s)
✔ [583/631] Built Mathlib.Order.BoundedOrder.Lattice (1.7s)
✔ [584/632] Built Mathlib.Util.TermReduce (1.3s)
✔ [585/632] Built Mathlib.Tactic.Linter.HaveLetLinter (1.4s)
✔ [586/633] Built Mathlib.Algebra.Group.Units.Equiv (2.0s)
✔ [587/633] Built Mathlib.Tactic.Linter.MinImports (1.4s)
✔ [588/634] Built Mathlib.Tactic.ClickSuggestions.Util (2.7s)
✔ [589/634] Built Mathlib.Tactic.Linter.PPRoundtrip (1.3s)
✔ [590/634] Built Mathlib.Tactic.Linter.UpstreamableDecl (1.3s)
✔ [591/635] Built Mathlib.Tactic.FunProp.Types (1.7s)
✔ [592/635] Built Mathlib.Algebra.Group.Opposite (2.7s)
✔ [593/635] Built Mathlib.Algebra.Group.TypeTags.Basic (2.7s)
✔ [594/635] Built Mathlib.Tactic.RSuffices (975ms)
✔ [595/635] Built Mathlib.Tactic.Observe (1.3s)
✔ [596/637] Built Mathlib.Tactic.IrreducibleDef (1.6s)
✔ [597/638] Built Mathlib.Tactic.ClickSuggestions.SectionState (1.4s)
✔ [598/639] Built Mathlib.Tactic.Linter (1.0s)
✔ [599/639] Built Mathlib.Tactic.ClickSuggestions.Unfold (1.4s)
✔ [600/639] Built Mathlib.Tactic.Recover (1.2s)
✔ [601/639] Built Mathlib.Tactic.Rename (1.1s)
✔ [602/639] Built Mathlib.Order.Disjoint (2.7s)
✔ [603/639] Built Mathlib.Tactic.FunProp.Theorems (1.7s)
✔ [604/639] Built Mathlib.Util.Tactic (1.1s)
✔ [605/639] Built Mathlib.Algebra.Group.TypeTags.Hom (1.8s)
✔ [606/639] Built Mathlib.Tactic.Says (1.4s)
✔ [607/642] Built Mathlib.Tactic.ClickSuggestions.Apply (1.6s)
✔ [608/642] Built Mathlib.Tactic.ClickSuggestions.ApplyAt (1.6s)
✔ [609/642] Built Mathlib.Order.PropInstances (1.4s)
✔ [610/642] Built Mathlib.Tactic.Set (1.4s)
✔ [611/644] Built Mathlib.Tactic.ClickSuggestions.GRewrite (1.0s)
✔ [612/644] Built Mathlib.Tactic.ClickSuggestions.Rewrite (1.9s)
✔ [613/645] Built Mathlib.Tactic.FunProp.Attr (1.0s)
✔ [614/645] Built Mathlib.Tactic.RenameBVar (1.1s)
✔ [615/646] Built Mathlib.Lean.Elab.Tactic.Basic (1.1s)
✔ [616/647] Built Mathlib.Tactic.Substs (1.0s)
✔ [617/647] Built Mathlib.Algebra.Group.Prod (4.2s)
✔ [618/649] Built Mathlib.Algebra.Group.Equiv.TypeTags (2.0s)
✔ [619/649] Built Mathlib.Tactic.SimpIntro (1.5s)
✔ [620/650] Built Mathlib.Tactic.SuccessIfFailWithMsg (1.2s)
✔ [621/651] Built Mathlib.Tactic.ClickSuggestions.FindPremises (1.8s)
✔ [622/651] Built Mathlib.Tactic.SudoSetOption (1.3s)
✔ [623/652] Built Mathlib.Tactic.FunProp.Core (3.3s)
✔ [624/652] Built Mathlib.Tactic.SwapVar (1.2s)
✔ [625/656] Built Mathlib.Tactic.Setm (1.5s)
✔ [626/656] Built Mathlib.Tactic.ToLevel (1.1s)
✔ [627/659] Built Mathlib.Tactic.ToFun (1.4s)
✔ [628/662] Built Mathlib.Data.Set.Basic (2.9s)
✔ [629/662] Built Mathlib.Tactic.Trace (1.0s)
✔ [630/665] Built Mathlib.Tactic.UnsetOption (1.0s)
✔ [631/665] Built Mathlib.Tactic.Tauto (2.2s)
✔ [632/665] Built Mathlib.Tactic.Widget.SelectInsertParamsClass (1.1s)
✔ [633/665] Built Mathlib.Tactic.ClickSuggestions.TryPremises (1.0s)
✔ [634/665] Built Mathlib.Tactic.FunProp.Elab (1.5s)
✔ [635/668] Built Mathlib.Tactic.WLOG (1.4s)
✔ [636/670] Built Mathlib.Util.PrintSorries (1.3s)
✔ [637/671] Built Mathlib.Util.TransImports (1.1s)
✔ [638/680] Built Mathlib.Tactic.Variable (2.0s)
✔ [639/682] Built Mathlib.Util.CountHeartbeats (1.8s)
✔ [640/690] Built Mathlib.Util.WhatsNew (1.3s)
✔ [641/691] Built AeneasMeta.Async.Test (59s)
✔ [642/691] Built Mathlib.Tactic.FunProp (1.1s)
✔ [643/691] Built Mathlib.Tactic.Widget.SelectPanelUtils (1.5s)
✔ [644/694] Built Batteries.Tactic.Congr (1.0s)
✔ [645/694] Built AeneasMeta.Async.Test:c.o (379ms)
✔ [646/694] Built Mathlib.Control.ULift (1.1s)
✔ [647/694] Built Mathlib.Tactic.ClickSuggestions (1.9s)
✔ [648/694] Built Mathlib.Data.Set.Disjoint (1.7s)
✔ [649/694] Built Mathlib.Data.Set.Inclusion (1.5s)
✔ [650/694] Built Mathlib.Data.Prod.PProd (999ms)
✔ [651/694] Built Mathlib.Tactic.Monotonicity.Attr (1.0s)
✔ [652/694] Built AeneasMeta.Async.Test:dynlib (266ms)
✔ [653/694] Built Mathlib.Order.GaloisConnection.Defs (1.8s)
✔ [654/696] Built Mathlib.Order.BoundedOrder.Monotone (1.4s)
✔ [655/698] Built Mathlib.Tactic.Widget.CongrM (1.1s)
✔ [656/698] Built Mathlib.Util.PPOptions (1.0s)
✔ [657/703] Built Mathlib.Tactic.Widget.Conv (1.0s)
✔ [658/703] Built Mathlib.Data.ULift (1.6s)
✔ [659/712] Built Mathlib.Tactic.Widget.Calc (1.0s)
✔ [660/719] Built Mathlib.Tactic.Widget.LibraryRewrite (2.6s)
✔ [661/719] Built Mathlib.Algebra.Order.ZeroLEOne (1.5s)
✔ [662/719] Built Mathlib.Logic.Embedding.Basic (2.2s)
✔ [663/720] Built Mathlib.Order.Interval.Set.Defs (1.6s)
✔ [664/721] Built AeneasMeta.Async (2.2s)
✔ [665/721] Built Mathlib.Data.Set.Insert (2.6s)
✔ [666/721] Built Mathlib.Order.Bounds.Defs (1.2s)
✔ [667/722] Built AeneasMeta.Async:c.o (162ms)
✔ [668/722] Built Mathlib.Basic.Nontrivial.Basic (1.3s)
✔ [669/722] Built Mathlib.Data.Option.NAry (1.1s)
✔ [670/722] Built AeneasMeta.Async:dynlib (209ms)
✔ [671/722] Built Mathlib.Order.TypeTags (1.3s)
✔ [672/722] Built Mathlib.Control.Monad.Basic (1.1s)
✔ [673/722] Built Mathlib.Dynamics.FixedPoints.Defs (1.2s)
✔ [674/724] Built Mathlib.Algebra.Order.IsBotOne (1.5s)
✔ [675/726] Built Mathlib.Tactic.Common (1.8s)
✔ [676/726] Built Mathlib.Util.Delaborators (2.7s)
✔ [677/729] Built Mathlib.Data.Bool.Set (1.5s)
✔ [678/731] Built Mathlib.Data.Set.Subsingleton (1.9s)
✔ [679/731] Built Batteries.Control.ForInStep.Lemmas (469ms)
✔ [680/731] Built Mathlib.Tactic.SetLike (1.2s)
✔ [681/731] Built Batteries.Data.List.Pairwise (529ms)
✔ [682/735] Built Mathlib.Order.Heyting.Basic (5.2s)
✔ [683/735] Built Mathlib.Order.Iterate (1.8s)
✔ [684/735] Built Mathlib.Order.RelIso.Basic (3.7s)
✔ [685/738] Built Mathlib.Order.SetNotation (2.9s)
✔ [686/755] Built AeneasMeta (2.5s)
✔ [687/755] Built Mathlib.Data.List.TFAE (1.1s)
✔ [688/755] Built AeneasMeta:c.o (165ms)
✔ [689/757] Built AeneasMeta:shared (263ms)
✔ [690/757] Built Mathlib.Lean.Expr.ExtraRecognizers (1.3s)
✔ [691/757] Built Mathlib.Basic.SetLike.Basic (2.1s)
✔ [692/757] Built Mathlib.Data.Part (2.7s)
✔ [693/757] Built Aeneas.Tactic.Step.Simp (1.9s)
✔ [694/760] Built Mathlib.Order.BooleanAlgebra.Defs (2.2s)
✔ [695/762] Built Mathlib.Algebra.Group.End (4.5s)
✔ [696/763] Built Aeneas.Tactic.Elab.TraitDefault.Init (1.9s)
✔ [697/765] Built Aeneas.Std.Spec (2.3s)
✔ [698/774] Built Mathlib.Data.Set.Notation (1.4s)
✔ [699/774] Built Mathlib.Util.AtomM (1.1s)
✔ [700/774] Built Mathlib.Algebra.Group.Int.Defs (963ms)
✔ [701/776] Built Batteries.Data.List.Lemmas (4.5s)
✔ [702/776] Built Aeneas.Tactic.Step.DspecInduction (3.1s)
✔ [703/779] Built Mathlib.Logic.OpClass (1.1s)
✔ [704/779] Built Mathlib.Util.AtomM.Recurse (1.3s)
✔ [705/782] Built Mathlib.Data.Int.Basic (1.5s)
✔ [706/785] Built Batteries.Classes.RatCast (533ms)
✔ [707/785] Built Mathlib.Algebra.Group.Equiv.Opposite (2.5s)
✔ [708/788] Built Mathlib.Algebra.Order.Monoid.Unbundled.Defs (2.2s)
✔ [709/788] Built Mathlib.Order.BooleanAlgebra.Basic (3.5s)
✔ [710/788] Built Aeneas.Extract.Extract (4.3s)
✔ [711/788] Built Mathlib.Order.WithBot (8.2s)
✔ [712/788] Built Mathlib.Order.Hom.Basic (6.2s)
✔ [713/788] Built Mathlib.Algebra.Group.IsCommutative (1.3s)
✔ [714/788] Built Mathlib.Data.Rat.Init (1.1s)
✔ [715/788] Built Mathlib.Data.Nat.Cast.Defs (1.4s)
✔ [716/788] Built Mathlib.Data.List.Pairwise (2.4s)
✔ [717/788] Built Mathlib.Order.MinMax (2.3s)
✔ [718/788] Built Mathlib.Algebra.GroupWithZero.Defs (1.5s)
✔ [719/792] Built Mathlib.Algebra.Group.Even (2.0s)
✔ [720/794] Built Aeneas.Extract (1.3s)
✔ [721/794] Built Aeneas.Std.Core.Result (1.9s)
✔ [722/794] Built Mathlib.Data.Int.Cast.Defs (1.3s)
✔ [723/794] Built Mathlib.Order.BooleanAlgebra.Set (2.7s)
✔ [724/794] Built Mathlib.Order.Part (1.0s)
✔ [725/794] Built Mathlib.Order.SymmDiff (2.9s)
✔ [726/794] Built Mathlib.Order.Antisymmetrization (2.3s)
✔ [727/794] Built Mathlib.Data.Rat.Defs (2.1s)
✔ [728/802] Built Mathlib.Algebra.Notation.Bracket (1.2s)
✔ [729/802] Built Mathlib.Order.Lex (1.5s)
✔ [730/806] Built Mathlib.Algebra.CharZero.Defs (1.1s)
✔ [731/811] Built Mathlib.Data.Int.Cast.Basic (1.4s)
✔ [732/811] Built Mathlib.Algebra.NeZero (1.2s)
✔ [733/811] Built Mathlib.Data.Set.SymmDiff (1.6s)
✔ [734/811] Built Aeneas.Std.Primitives (2.6s)
✔ [735/811] Built Mathlib.Algebra.Ring.Defs (3.1s)
✔ [736/817] Built Mathlib.Algebra.Group.Semiconj.Units (1.6s)
✔ [737/817] Built Mathlib.Algebra.Group.Invertible.Defs (1.4s)
✔ [738/817] Built Mathlib.Algebra.Order.Monoid.Unbundled.Basic (4.5s)
✔ [739/817] Built Mathlib.Algebra.GroupWithZero.NeZero (1.2s)
✔ [740/817] Built Mathlib.Tactic.TFAE (2.7s)
✔ [741/817] Built Mathlib.Algebra.Group.Hom.Instances (3.1s)
✔ [742/817] Built Mathlib.Algebra.Ring.Semiconj (1.2s)
✔ [743/817] Built Mathlib.Order.Interval.Set.Basic (4.2s)
✔ [744/817] Built Mathlib.Algebra.Order.Group.Synonym (3.5s)
✔ [745/817] Built Aeneas.Std.Core.Ops (2.2s)
✔ [746/817] Built Mathlib.Algebra.Ring.Int.Defs (1.8s)
✔ [747/817] Built Mathlib.Algebra.Ring.GrindInstances (1.8s)
✔ [748/818] Built Mathlib.Algebra.Field.Defs (1.7s)
✔ [749/821] Built Aeneas.Std.Delab (2.4s)
✔ [750/823] Built Mathlib.Tactic.Nontriviality.Core (1.8s)
✔ [751/823] Built Mathlib.Data.Set.Image (3.0s)
✔ [752/823] Built Mathlib.Algebra.GroupWithZero.InjSurj (1.7s)
✔ [753/823] Built Mathlib.Algebra.Group.Commute.Units (2.1s)
✔ [754/823] Built Mathlib.Algebra.Order.Sub.Defs (1.0s)
✔ [755/823] Built Mathlib.Algebra.GroupWithZero.Basic (2.0s)
✔ [756/823] Built Mathlib.Algebra.Order.Ring.Synonym (1.9s)
✔ [757/823] Built Mathlib.Algebra.Ring.Basic (1.0s)
✔ [758/823] Built Mathlib.Tactic.Bound.Init (1.4s)
✔ [759/823] Built Mathlib.Tactic.Nontriviality (1.6s)
✔ [760/823] Built Mathlib.Algebra.Order.GroupWithZero.Defs (2.4s)
✔ [761/825] Built Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual (1.5s)
✔ [762/825] Built Mathlib.Data.Set.Restrict (1.8s)
✔ [763/825] Built Mathlib.Data.Nat.Set (1.5s)
✔ [764/827] Built Mathlib.Order.Directed (2.1s)
✔ [765/827] Built Mathlib.Algebra.Group.Invertible.Basic (1.0s)
✔ [766/834] Built Mathlib.Tactic.Bound.Attribute (1.9s)
✔ [767/837] Built Mathlib.Algebra.GroupWithZero.Hom (2.6s)
✔ [768/837] Built Mathlib.Algebra.Group.Nat.Defs (1.5s)
✔ [769/837] Built Mathlib.Data.Set.Prod (3.7s)
✔ [770/837] Built Mathlib.Algebra.GroupWithZero.Units.Basic (2.8s)
✔ [771/837] Built Mathlib.Data.Nat.Cast.Pi (1.2s)
✔ [772/837] Built Mathlib.Data.Nat.Cast.NeZero (1.4s)
✔ [773/840] Built Mathlib.Algebra.Divisibility.Basic (2.9s)
✔ [774/840] Built Mathlib.Algebra.Order.Group.Unbundled.Basic (4.1s)
✔ [775/840] Built Mathlib.Algebra.Order.Monoid.Unbundled.Pow (3.0s)
✔ [776/840] Built Mathlib.Algebra.GroupWithZero.Nat (1.3s)
✔ [777/840] Built Mathlib.Algebra.Ring.InjSurj (4.9s)
✔ [778/840] Built Mathlib.Algebra.Group.Nat.Hom (1.6s)
✔ [779/844] Built Mathlib.Data.Set.NAry (1.8s)
✔ [780/847] Built Mathlib.Algebra.GroupWithZero.Invertible (1.6s)
✔ [781/850] Built Mathlib.Algebra.Ring.Rat (2.1s)
✔ [782/850] Built Mathlib.Algebra.GroupWithZero.Semiconj (1.8s)
✔ [783/857] Built Mathlib.Algebra.Divisibility.Hom (2.1s)
✔ [784/857] Built Mathlib.Algebra.Ring.Nat (1.5s)
✔ [785/858] Built Mathlib.Algebra.Ring.Hom.Defs (3.4s)
✔ [786/858] Built Mathlib.Data.Nat.Sqrt (1.4s)
✔ [787/858] Built Mathlib.Data.Set.Function (3.6s)
✔ [788/858] Built Mathlib.Algebra.Order.Group.OrderIso (2.5s)
✔ [789/859] Built Mathlib.Order.Bounds.Basic (5.6s)
✔ [790/859] Built Mathlib.Data.PNat.Notation (1.1s)
✔ [791/860] Built Mathlib.Algebra.Ring.Invertible (1.9s)
✔ [792/860] Built Mathlib.Algebra.GroupWithZero.Commute (1.5s)
✔ [793/860] Built Mathlib.Data.Nat.Find (1.5s)
✔ [794/860] Built Mathlib.Algebra.Divisibility.Units (2.1s)
✔ [795/860] Built Mathlib.Tactic.HaveI (1.1s)
✔ [796/864] Built Mathlib.Data.Nat.Cast.Basic (2.0s)
✔ [797/864] Built Mathlib.Algebra.Ring.Units (1.7s)
✔ [798/864] Built Mathlib.Data.Int.Sqrt (1.8s)
✔ [799/867] Built Mathlib.Algebra.Group.Nat.Even (1.9s)
✔ [800/867] Built Mathlib.Lean.Expr.Rat (1.0s)
✔ [801/867] Built Mathlib.Algebra.Order.Group.Lattice (1.9s)
✔ [802/867] Built Mathlib.Data.Set.Pairwise.Basic (2.1s)
✔ [803/867] Built Mathlib.Order.WellFounded (2.3s)
✔ [804/867] Built Mathlib.Util.Qq (1.4s)
✔ [805/869] Built Mathlib.Data.PNat.Defs (1.7s)
✔ [806/869] Built Mathlib.Order.Nat (1.7s)
✔ [807/869] Built Mathlib.Algebra.GroupWithZero.Units.Lemmas (1.0s)
✔ [808/869] Built Mathlib.Order.CompleteLattice.Defs (2.7s)
✔ [809/869] Built Mathlib.Logic.Equiv.Set (3.2s)
✔ [810/869] Built Mathlib.Order.Bounds.Image (2.9s)
✔ [811/870] Built Mathlib.Algebra.GroupWithZero.Divisibility (2.3s)
✔ [812/874] Built Mathlib.Algebra.Order.GroupWithZero.Basic (4.7s)
✔ [813/874] Built Mathlib.Tactic.TryThis (1.3s)
✔ [814/874] Built Mathlib.Algebra.Ring.Commute (2.1s)
✔ [815/874] Built Mathlib.Data.Nat.Cast.Order.Basic (2.4s)
✔ [816/874] Built Mathlib.Data.Ineq (595ms)
✔ [817/877] Built Mathlib.Tactic.NormNum.Result (2.9s)
✔ [818/877] Built Mathlib.Algebra.Group.Int.Even (2.3s)
✔ [819/877] Built Mathlib.Order.ScottContinuity (2.2s)
✔ [820/879] Built Mathlib.Algebra.Order.Monoid.Defs (1.7s)
✔ [821/879] Built Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE (1.7s)
✔ [822/881] Built Mathlib.Data.Nat.Cast.Commute (1.7s)
✔ [823/883] Built Mathlib.Algebra.Order.Group.Unbundled.Abs (3.3s)
✔ [824/884] Built Mathlib.Order.Hom.Set (3.3s)
✔ [825/884] Built Mathlib.Algebra.GroupWithZero.Regular (1.3s)
✔ [826/885] Built Mathlib.Algebra.Group.WithOne.Defs (2.3s)
✔ [827/885] Built Mathlib.Algebra.Order.Nonneg.Basic (2.7s)
✔ [828/885] Built Mathlib.Algebra.GroupWithZero.Equiv (1.5s)
✔ [829/885] Built Mathlib.Tactic.NormNum.Core (2.4s)
✔ [830/885] Built Mathlib.Algebra.Field.Basic (3.2s)
✔ [831/885] Built Mathlib.Algebra.Order.Monoid.Canonical.Defs (1.9s)
✔ [832/885] Built Mathlib.Algebra.Order.Group.Unbundled.Int (1.6s)
✔ [833/888] Built Mathlib.Algebra.Regular.Basic (1.8s)
✔ [834/888] Built Mathlib.Algebra.Ring.Parity (2.9s)
✔ [835/888] Built Mathlib.Algebra.Order.Group.Int (1.7s)
✔ [836/888] Built Mathlib.Algebra.Order.Group.Defs (2.1s)
✔ [837/888] Built Mathlib.Order.Preorder.Chain (2.4s)
✔ [838/891] Built Mathlib.Algebra.Group.WithOne.Map (2.2s)
✔ [839/891] Built Mathlib.Algebra.Order.Group.Nat (1.6s)
✔ [840/891] Built Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (4.4s)
✔ [841/891] Built Mathlib.Algebra.Order.Monoid.Units (1.7s)
✔ [842/892] Built Mathlib.Algebra.Order.Monoid.OrderDual (1.5s)
✔ [843/896] Built Mathlib.Algebra.GroupWithZero.WithZero (3.5s)
✔ [844/896] Built Mathlib.Algebra.Ring.Int.Parity (2.6s)
✔ [845/902] Built Mathlib.Data.Int.Cast.Lemmas (2.5s)
✔ [846/902] Built Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags (1.8s)
✔ [847/902] Built Mathlib.Algebra.Order.Monoid.WithTop (1.8s)
✔ [848/902] Built Mathlib.Algebra.Order.Group.Units (1.7s)
✔ [849/902] Built Mathlib.Order.CompleteLattice.Basic (5.7s)
✔ [850/902] Built Mathlib.Algebra.Order.Monoid.NatCast (1.8s)
✔ [851/904] Built Mathlib.Algebra.Order.Ring.Unbundled.Rat (4.3s)
✔ [852/904] Built Mathlib.Tactic.NormNum.Basic (5.3s)
✔ [853/907] Built Mathlib.Util.SynthesizeUsing (1.1s)
✔ [854/907] Built Mathlib.Order.OmegaCompletePartialOrder (3.7s)
✔ [855/908] Built Mathlib.Algebra.Order.Monoid.TypeTags (1.6s)
✔ [856/912] Built Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (2.1s)
✔ [857/912] Built Mathlib.Algebra.Order.Sub.Unbundled.Basic (1.9s)
✔ [858/912] Built Mathlib.Data.Rat.Lemmas (2.2s)
✔ [859/912] Built Mathlib.Algebra.Order.AddGroupWithTop (2.2s)
✔ [860/914] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (1.1s)
✔ [861/916] Built Mathlib.Lean.Meta.Tactic.Rewrite (998ms)
✔ [862/916] Built Mathlib.Order.CompleteLattice.Lemmas (2.2s)
✔ [863/916] Built Mathlib.Data.Tree.Basic (1.5s)
✔ [864/916] Built Mathlib.Data.NNRat.Defs (2.7s)
✔ [865/919] Built Mathlib.Algebra.Order.Sub.Basic (1.8s)
✔ [866/922] Built Mathlib.Order.GaloisConnection.Basic (3.2s)
✔ [867/922] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm (1.3s)
✔ [868/923] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss (1.4s)
✔ [869/923] Built Mathlib.Tactic.Zify (1.7s)
✔ [870/923] Built Mathlib.Util.ElabWithoutMVars (1.2s)
✔ [871/925] Built Mathlib.Tactic.NormNum.Pow (3.6s)
✔ [872/929] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector (1.0s)
✔ [873/932] Built Mathlib.Algebra.Order.Ring.Unbundled.Basic (3.4s)
✔ [874/932] Built Mathlib.Order.ConditionallyCompleteLattice.Defs (1.9s)
✔ [875/932] Built Mathlib.Algebra.Field.Rat (2.1s)
✔ [876/932] Built Mathlib.Order.ConditionallyCompletePartialOrder.Defs (1.7s)
✔ [877/937] Built Mathlib.Order.Hom.Order (2.0s)
✔ [878/937] Built Mathlib.Data.Set.Order (1.7s)
✔ [879/941] Built Mathlib.Order.Antichain (2.2s)
✔ [880/946] Built Mathlib.Algebra.Order.Ring.Defs (1.0s)
✔ [881/947] Built Mathlib.Order.ConditionallyCompletePartialOrder.Basic (1.9s)
✔ [882/947] Built Mathlib.Algebra.Order.GroupWithZero.Canonical (5.5s)
✔ [883/947] Built Mathlib.Order.Interval.Set.Image (2.0s)
✔ [884/947] Built Mathlib.Order.LatticeIntervals (2.8s)
✔ [885/947] Built Mathlib.Algebra.Order.Monoid.Basic (1.9s)
✔ [886/947] Built Mathlib.Data.Rat.Cast.Defs (2.8s)
✔ [887/950] Built Mathlib.Order.Interval.Set.LinearOrder (3.9s)
✔ [888/950] Built Mathlib.Algebra.Order.Ring.Rat (2.0s)
✔ [889/953] Built Mathlib.Algebra.Order.Group.Abs (2.9s)
✔ [890/954] Built Mathlib.Order.CompleteBooleanAlgebra (6.1s)
✔ [891/954] Built Mathlib.Algebra.Order.Positive.Ring (2.0s)
✔ [892/954] Built Mathlib.Algebra.Order.Ring.InjSurj (1.5s)
✔ [893/956] Built Mathlib.Algebra.Order.Ring.Canonical (2.2s)
✔ [894/956] Built Mathlib.Algebra.Order.Ring.Nat (1.0s)
✔ [895/958] Built Mathlib.Data.Int.GCD (2.3s)
✔ [896/958] Built Mathlib.Tactic.CancelDenoms.Core (2.9s)
✔ [897/964] Built Mathlib.Algebra.Notation (1.4s)
✔ [898/965] Built Mathlib.Data.Rat.Cast.CharZero (2.1s)
✔ [899/965] Built Mathlib.Algebra.Order.Hom.Basic (1.6s)
✔ [900/965] Built Mathlib.Data.Set.BooleanAlgebra (1.6s)
✔ [901/965] Built Mathlib.Algebra.Order.Ring.Basic (2.2s)
✔ [902/966] Built Mathlib.Order.Interval.Set.UnorderedInterval (2.9s)
✔ [903/966] Built Mathlib.Data.Int.Cast.Field (1.7s)
✔ [904/966] Built Mathlib.Data.Int.Cast.Pi (1.1s)
✔ [905/966] Built Mathlib.Algebra.Order.Field.Canonical (2.2s)
✔ [906/970] Built Mathlib.Algebra.Notation.Support (2.5s)
✔ [907/970] Built Mathlib.Data.Nat.Cast.Order.Ring (2.2s)
✔ [908/971] Built Mathlib.Algebra.Order.Ring.Int (2.3s)
✔ [909/971] Built Aeneas.Tactic.Simp.SimpScalar.Init (1.5s)
✔ [910/972] Built Aeneas.Tactic.Simp.SimpBoolProp.Init (1.6s)
✔ [911/972] Built Mathlib.Algebra.Order.Group.PosPart (2.0s)
✔ [912/972] Built Mathlib.Data.Nat.Factorial.Basic (2.7s)
✔ [913/972] Built Aeneas.Tactic.Solver.ScalarTac.Init (2.1s)
✔ [914/974] Built Mathlib.Order.Interval.Set.OrderEmbedding (2.1s)
✔ [915/974] Built Mathlib.Data.Set.Lattice.Indexed (2.4s)
✔ [916/974] Built Aeneas.Tactic.Conv.Bvify.Init (1.5s)
✔ [917/975] Built Mathlib.Data.Int.CharZero (1.9s)
✔ [918/975] Built Mathlib.Tactic.NormNum.Inv (3.0s)
✔ [919/975] Built Aeneas.Data.Nat (1.3s)
✔ [920/975] Built Mathlib.Tactic.NormNum.Abs (2.0s)
✔ [921/975] Built Mathlib.Algebra.Order.Invertible (1.8s)
✔ [922/975] Built Aeneas.Data.Int (1.4s)
✔ [923/975] Built Mathlib.Algebra.Order.Ring.Cast (2.1s)
✔ [924/975] Built Mathlib.Tactic.Linarith.Lemmas (2.1s)
✔ [925/976] Built Aeneas.Tactic.Simp.SimpLists.Init (1.5s)
✔ [926/980] Built Aeneas.Tactic.Simp.SimpBoolProp.SimpBoolProp (2.1s)
✔ [927/986] Built Mathlib.Order.Interval.Set.OrdConnected (2.3s)
✔ [928/986] Built Mathlib.Algebra.Group.Nat.Units (1.2s)
✔ [929/988] Built Batteries.Data.Fin.Basic (829ms)
✔ [930/991] Built Mathlib.Algebra.Group.Irreducible.Defs (1.5s)
✔ [931/991] Built Mathlib.Data.Set.Lattice.Bounded (2.7s)
✔ [932/991] Built Aeneas.Std.Scalar.Elab (2.6s)
✔ [933/991] Built Mathlib.Tactic.NormNum.Eq (2.6s)
✔ [934/992] Built Mathlib.Data.Int.DivMod (1.1s)
✔ [935/992] Built Mathlib.Tactic.Linarith.Datatypes (2.7s)
✔ [936/995] Built Mathlib.Order.ConditionallyCompleteLattice.Basic (4.2s)
✔ [937/995] Built Mathlib.Algebra.GroupWithZero.Opposite (1.5s)
✔ [938/995] Built Mathlib.Algebra.Group.ULift (1.9s)
✔ [939/995] Built Mathlib.Algebra.Prime.Defs (1.9s)
✔ [940/995] Built Mathlib.Order.BourbakiWitt (2.0s)
✔ [941/997] Built Mathlib.Tactic.Positivity.Core (4.9s)
✔ [942/997] Built Mathlib.Algebra.Group.ModEq (1.9s)
✔ [943/997] Built Mathlib.Data.Fin.Basic (2.6s)
✔ [944/997] Built Mathlib.Tactic.NormNum.Ineq (3.5s)
✔ [945/998] Built Mathlib.Tactic.Linarith.Preprocessing (3.2s)
✔ [946/998] Built Mathlib.Tactic.Linarith.Parsing (2.5s)
✔ [947/998] Built Mathlib.Algebra.Ring.Equiv (4.6s)
✔ [948/998] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm (2.9s)
✔ [949/998] Built Mathlib.Order.CompleteLatticeIntervals (3.0s)
✔ [950/998] Built Mathlib.Data.Nat.GCD.Basic (2.4s)
✔ [951/1000] Built Mathlib.Data.Nat.Prime.Defs (2.3s)
✔ [952/1000] Built Mathlib.Data.Nat.Cast.Prod (1.5s)
✔ [953/1000] Built Mathlib.Algebra.Ring.Opposite (3.3s)
✔ [954/1000] Built Mathlib.Order.FixedPoints (2.6s)
✔ [955/1000] Built Mathlib.Tactic.Ring.Common (9.2s)
✔ [956/1000] Built Mathlib.Algebra.GroupWithZero.Units.Equiv (1.6s)
✔ [957/1000] Built Mathlib.Tactic.NormNum.DivMod (2.6s)
✔ [958/1000] Built Mathlib.Algebra.Order.Nonneg.Lattice (2.2s)
✔ [959/1001] Built Mathlib.Algebra.Ring.ULift (2.5s)
✔ [960/1005] Built Mathlib.Data.Fin.SuccPred (3.5s)
✔ [961/1005] Built Mathlib.Algebra.Group.Int.Units (1.5s)
✔ [962/1005] Built Mathlib.Tactic.Linarith.Verification (3.1s)
✔ [963/1005] Built Aeneas.Data.Coinductive.ITreeWP.FunctionalWP (1.9s)
✔ [964/1005] Built Mathlib.Data.Nat.ModEq (2.9s)
✔ [965/1005] Built Mathlib.Algebra.CharP.Defs (2.3s)
✔ [966/1005] Built Mathlib.Algebra.Ring.Int.Units (1.4s)
✔ [967/1015] Built Mathlib.Algebra.Order.Sub.WithTop (1.6s)
✔ [968/1015] Built Mathlib.Data.Fin.Rev (1.7s)
✔ [969/1015] Built Mathlib.Algebra.Order.Nonneg.Ring (2.3s)
✔ [970/1015] Built Mathlib.Data.ENat.Defs (1.2s)
✔ [971/1019] Built Aeneas.Data.Coinductive.ITreeWP.DWLP (1.9s)
✔ [972/1019] Built Aeneas.Data.Coinductive.ITreeWP.DWP (1.9s)
✔ [973/1020] Built Mathlib.Data.Int.ModEq (2.2s)
✔ [974/1021] Built Mathlib.Tactic.Ring.Basic (4.5s)
✔ [975/1021] Built Mathlib.Order.Interval.Set.WithBotTop (2.0s)
✔ [976/1026] Built Mathlib.Algebra.Group.Fin.Basic (2.2s)
✔ [977/1026] Built Mathlib.Data.ENat.Basic (2.1s)
✔ [978/1026] Built Mathlib.Data.List.Monad (1.2s)
✔ [979/1026] Built Aeneas.Data.Coinductive.ITreeWP.Taxonomy (682ms)
✔ [980/1026] Built Mathlib.Control.Functor (1.5s)
✔ [981/1026] Built Mathlib.Algebra.Order.Nonneg.Field (2.0s)
✔ [982/1026] Built Batteries.Data.List.Perm (1.3s)
✔ [983/1026] Built Mathlib.Algebra.Order.Ring.WithTop (5.2s)
✔ [984/1027] Built Mathlib.Tactic.Positivity.Basic (9.4s)
✔ [985/1027] Built Aeneas.Data.Coinductive.ITreeWP.Tests (843ms)
✔ [986/1027] Built Mathlib.Data.List.Forall2 (2.1s)
✔ [987/1027] Built Mathlib.Data.List.InsertIdx (2.1s)
✔ [988/1028] Built Mathlib.Algebra.CharP.Basic (2.3s)
✔ [989/1032] Built Aeneas.Data.Coinductive.ITreeWP (456ms)
✔ [990/1035] Built Mathlib.Data.List.Defs (2.0s)
✔ [991/1035] Built Mathlib.Algebra.Order.Field.Rat (2.1s)
✔ [992/1036] Built Mathlib.Tactic.Ring.RingNF (3.2s)
✔ [993/1036] Built Mathlib.Tactic.Linarith.Frontend (3.7s)
✔ [994/1045] Built Mathlib.Data.List.Count (1.0s)
✔ [995/1052] Built Mathlib.Tactic.NormNum.OfScientific (2.5s)
✔ [996/1061] Built Mathlib.Data.ENat.Monoid (2.8s)
✔ [997/1063] Built Mathlib.Order.Cover (4.6s)
✔ [998/1068] Built Mathlib.Data.Set.List (1.6s)
✔ [999/1075] Built Mathlib.Data.List.Perm.Basic (2.2s)
✔ [1000/1083] Built Mathlib.Data.Finset.Attr (1.2s)
✔ [1001/1088] Built Mathlib.Data.List.Induction (1.4s)
✔ [1002/1091] Built Batteries.Data.Fin.Lemmas (1.2s)
✔ [1003/1092] Built Mathlib.Basic.Finite.Defs (1.7s)
✔ [1004/1092] Built Mathlib.Data.Rat.Cast.Order (3.9s)
✔ [1005/1092] Built Mathlib.Data.List.TakeDrop (3.2s)
✔ [1006/1092] Built Mathlib.Logic.Small.Defs (1.6s)
✔ [1007/1097] Built Mathlib.Data.List.Basic (4.2s)
✔ [1008/1097] Built Mathlib.Data.Fin.Embedding (2.6s)
✔ [1009/1097] Built Mathlib.Algebra.BigOperators.Group.List.Defs (1.6s)
✔ [1010/1098] Built Aeneas.Std.WP (4.0s)
✔ [1011/1098] Built Mathlib.Data.List.Flatten (1.6s)
✔ [1012/1098] Built Mathlib.Basic.Countable.Defs (1.1s)
✔ [1013/1098] Built Mathlib.Basic.UnivLE (1.1s)
✔ [1014/1098] Built Mathlib.Data.List.ProdSigma (1.6s)
✔ [1015/1098] Built Mathlib.Logic.Small.Basic (1.6s)
✔ [1016/1103] Built Mathlib.Tactic.NormNum (2.0s)
✔ [1017/1103] Built Mathlib.Data.List.Lex (1.8s)
✔ [1018/1103] Built Mathlib.Algebra.Order.Hom.Monoid (4.7s)
✔ [1019/1103] Built Mathlib.Order.SuccPred.Basic (5.4s)
✔ [1020/1103] Built Mathlib.Order.Fin.Basic (2.7s)
✔ [1021/1103] Built Mathlib.Data.List.Infix (2.1s)
✔ [1022/1103] Built Mathlib.Data.List.Perm.Subperm (1.9s)
✔ [1023/1103] Built Mathlib.Data.List.Lattice (2.5s)
✔ [1024/1103] Built Mathlib.Basic.Countable.Small (1.7s)
✔ [1025/1105] Built Mathlib.Algebra.BigOperators.Group.List.Basic (3.0s)
✔ [1026/1107] Built Mathlib.Tactic.Linarith (2.2s)
✔ [1027/1109] Built Mathlib.Data.List.Nodup (3.3s)
✔ [1028/1109] Built Aeneas.Tactic.Step.PrepareIntroOutputs (2.8s)
✔ [1029/1109] Built Mathlib.Order.SuccPred.WithBot (2.1s)
✔ [1030/1109] Built Mathlib.Data.List.Chain (3.0s)
✔ [1031/1109] Built Mathlib.Algebra.Order.Hom.MonoidWithZero (3.1s)
✔ [1032/1109] Built Mathlib.Data.Multiset.Defs (2.4s)
✔ [1033/1112] Built Mathlib.Order.SuccPred.Archimedean (3.1s)
✔ [1034/1112] Built Mathlib.Data.List.Enum (2.1s)
✔ [1035/1112] Built Aeneas.Command.Decompose (5.1s)
✔ [1036/1112] Built Mathlib.Data.List.Dedup (2.2s)
✔ [1037/1112] Built Mathlib.Data.List.Perm.Lattice (2.2s)
✔ [1038/1112] Built Aeneas.Tactic.Solver.ScalarTac.Core (3.4s)
✔ [1039/1112] Built Mathlib.Data.Fin.Tuple.Basic (4.3s)
✔ [1040/1115] Built Mathlib.Data.List.Duplicate (2.3s)
✔ [1041/1115] Built Mathlib.Data.List.Rotate (2.7s)
✔ [1042/1115] Built Mathlib.Data.List.Range (1.0s)
✔ [1043/1115] Built Aeneas.Tactic.Step.SpecInfo (2.2s)
✔ [1044/1115] Built Mathlib.Data.Nat.Choose.Basic (2.6s)
✔ [1045/1115] Built Mathlib.Data.Finset.Defs (2.2s)
✔ [1046/1116] Built Mathlib.Data.Multiset.ZeroCons (2.0s)
✔ [1047/1116] Built Mathlib.Algebra.Order.Hom.Ring (3.4s)
✔ [1048/1117] Built Mathlib.Data.List.OfFn (2.1s)
✔ [1049/1117] Built Mathlib.Data.List.OffDiag (2.4s)
✔ [1050/1120] Built Mathlib.Data.Set.Piecewise (1.8s)
✔ [1051/1120] Built Mathlib.Data.List.FinRange (2.2s)
✔ [1052/1121] Built Mathlib.Algebra.BigOperators.Group.List.Lemmas (2.2s)
✔ [1053/1127] Built Mathlib.Data.Finset.Empty (2.0s)
✔ [1054/1129] Built Mathlib.Data.Multiset.Count (1.0s)
✔ [1055/1131] Built Mathlib.Data.Multiset.Basic (2.0s)
✔ [1056/1131] Built Mathlib.Order.SuccPred.Limit (4.6s)
✔ [1057/1136] Built Aeneas.Tactic.Solver.ScalarTac.ScalarTac (5.5s)
✔ [1058/1138] Built Mathlib.Data.List.Sort (3.3s)
✔ [1059/1140] Built Mathlib.Order.Hom.Bounded (3.7s)
✔ [1060/1142] Built Mathlib.Data.Set.Sigma (3.1s)
✔ [1061/1143] Built Mathlib.Order.Hom.Lattice (3.9s)
✔ [1062/1143] Built Mathlib.Data.Multiset.AddSub (2.9s)
✔ [1063/1143] Built Mathlib.Logic.Embedding.Set (2.7s)
✔ [1064/1147] Built Mathlib.Logic.Function.DependsOn (1.0s)
✔ [1065/1147] Built Mathlib.Data.Set.Lattice.Image (3.8s)
✔ [1066/1151] Built Mathlib.Control.Applicative (1.7s)
✔ [1067/1151] Built Mathlib.Algebra.Order.SuccPred (3.7s)
✔ [1068/1155] Built Mathlib.Control.Traversable.Basic (1.9s)
✔ [1069/1155] Built Aeneas.Tactic.Step.Init (6.9s)
✔ [1070/1155] Built Mathlib.Data.List.NodupEquivFin (2.9s)
✔ [1071/1155] Built Mathlib.Data.Vector.Defs (2.4s)
✔ [1072/1156] Built Mathlib.Order.Setoid.Basic (2.4s)
✔ [1073/1159] Built Mathlib.Data.Multiset.Replicate (2.1s)
✔ [1074/1159] Built Mathlib.Tactic.ApplyFun (2.1s)
✔ [1075/1159] Built Mathlib.Data.List.Sublists (2.1s)
✔ [1076/1161] Built Mathlib.Data.List.Zip (2.1s)
✔ [1077/1161] Built Mathlib.Order.SuccPred.Nat (2.2s)
✔ [1078/1165] Built Mathlib.Data.Set.Lattice.Disjoint (1.9s)
✔ [1079/1165] Built Mathlib.Data.Nat.Bits (1.3s)
✔ [1080/1169] Built Aeneas.Std.Core.Cmp (2.5s)
✔ [1081/1169] Built Mathlib.Order.Hom.BoundedLattice (4.2s)
✔ [1082/1169] Built Mathlib.Data.Nat.Pairing (1.7s)
✔ [1083/1169] Built Aeneas.Std.Core.Core (2.7s)
✔ [1084/1169] Built Mathlib.Data.Nat.Order.Lemmas (1.5s)
✔ [1085/1169] Built Mathlib.Data.Multiset.MapFold (2.7s)
✔ [1086/1169] Built Mathlib.Data.PNat.Equiv (1.4s)
✔ [1087/1170] Built Mathlib.Data.Vector.Basic (3.2s)
✔ [1088/1170] Built Mathlib.Order.SuccPred.ENat (2.3s)
✔ [1089/1171] Built Mathlib.Data.Set.Pairwise.Lattice (2.2s)
✔ [1090/1171] Built Mathlib.Logic.Small.Set (1.7s)
✔ [1091/1173] Built Mathlib.Logic.Equiv.Nat (1.6s)
✔ [1092/1173] Built Mathlib.Data.List.MinMax (3.8s)
✔ [1093/1175] Built Mathlib.Data.Finset.Attach (1.7s)
✔ [1094/1175] Built Mathlib.Order.Minimal (3.6s)
✔ [1095/1175] Built Mathlib.Order.RelIso.Set (1.5s)
✔ [1096/1179] Built Aeneas.Std.Alloc.Alloc (2.6s)
✔ [1097/1179] Built Mathlib.Data.Multiset.Filter (2.2s)
✔ [1098/1179] Built Aeneas.Std.Core.Convert (2.8s)
✔ [1099/1179] Built Mathlib.Data.ENat.Pow (2.2s)
✔ [1100/1179] Built Mathlib.Order.Prod.Lex.Basic (2.8s)
✔ [1101/1179] Built Mathlib.Logic.Encodable.Basic (2.7s)
✔ [1102/1179] Built Mathlib.Basic.Countable.Basic (2.3s)
✔ [1103/1188] Built Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (2.5s)
✔ [1104/1188] Built Mathlib.Data.Finset.Erase (2.3s)
✔ [1105/1192] Built Mathlib.Data.Finset.Filter (2.5s)
✔ [1106/1192] Built Mathlib.Algebra.BigOperators.Group.Multiset.Defs (2.7s)
✔ [1107/1192] Built Mathlib.Data.Multiset.UnionInter (2.7s)
✔ [1108/1192] Built Mathlib.Order.Sum.Order (4.9s)
✔ [1109/1192] Built Mathlib.SetTheory.Cardinal.Defs (2.1s)
✔ [1110/1192] Built Mathlib.Order.CompleteLattice.Chain (1.7s)
✔ [1111/1192] Built Mathlib.Order.UpperLower.Basic (4.6s)
✔ [1112/1192] Built Mathlib.Algebra.Ring.CompTypeclasses (1.9s)
✔ [1113/1193] Built Mathlib.Algebra.GroupWithZero.Prod (2.1s)
✔ [1114/1196] Built Aeneas.Std.Alloc.Boxed (2.9s)
✔ [1115/1199] Built Mathlib.Data.Int.Cast.Prod (1.6s)
✔ [1116/1200] Built Aeneas.Std.Scalar.Core (8.8s)
✔ [1117/1210] Built Mathlib.Data.Multiset.Range (1.8s)
✔ [1118/1210] Built Mathlib.Data.Multiset.Dedup (2.1s)
✔ [1119/1210] Built Mathlib.Order.Zorn (1.7s)
✔ [1120/1210] Built Mathlib.Data.Fintype.Defs (2.8s)
✔ [1121/1210] Built Mathlib.Order.Hom.Lex (2.7s)
✔ [1122/1215] Built Mathlib.Order.ConditionallyCompleteLattice.Indexed (4.7s)
✔ [1123/1215] Built Mathlib.Algebra.Group.Subsemigroup.Defs (2.7s)
✔ [1124/1215] Built Mathlib.Algebra.Group.Action.Defs (2.0s)
✔ [1125/1215] Built Mathlib.Data.Finset.Dedup (1.0s)
✔ [1126/1215] Built Mathlib.Data.Multiset.FinsetOps (2.0s)
✔ [1127/1215] Built Mathlib.Data.Multiset.Fold (1.8s)
✔ [1128/1215] Built Mathlib.Algebra.Group.Conj (2.8s)
✔ [1129/1215] Built Mathlib.Algebra.Ring.Prod (3.5s)
✔ [1130/1215] Built Mathlib.Algebra.Order.Group.Multiset (2.1s)
✔ [1131/1215] Built Mathlib.SetTheory.Cardinal.SchroederBernstein (2.3s)
✔ [1132/1217] Built Mathlib.Algebra.Group.Action.Faithful (1.4s)
✔ [1133/1217] Built Mathlib.Algebra.Group.Pi.Lemmas (3.0s)
✔ [1134/1217] Built Mathlib.Algebra.Group.Subsemigroup.Basic (2.1s)
✔ [1135/1217] Built Mathlib.Order.SuccPred.CompleteLinearOrder (2.7s)
✔ [1136/1219] Built Mathlib.Algebra.Group.Action.Opposite (2.0s)
✔ [1137/1219] Built Mathlib.Order.InitialSeg (3.5s)
✔ [1138/1219] Built Mathlib.Data.Multiset.Lattice (2.0s)
✔ [1139/1219] Built Mathlib.Algebra.Group.Submonoid.Defs (3.4s)
✔ [1140/1221] Built Mathlib.Data.Finset.Lattice.Basic (2.3s)
✔ [1141/1221] Built Mathlib.Data.Multiset.Sum (1.0s)
✔ [1142/1222] Built Mathlib.Algebra.BigOperators.Group.Multiset.Basic (2.6s)
✔ [1143/1223] Built Mathlib.Data.Finset.Insert (3.4s)
✔ [1144/1223] Built Mathlib.Algebra.Group.Action.Units (1.9s)
✔ [1145/1223] Built Mathlib.Algebra.Group.Center (4.0s)
✔ [1146/1223] Built Mathlib.Data.Sym.Basic (3.0s)
✔ [1147/1223] Built Mathlib.Algebra.Group.Submonoid.MulAction (1.9s)
✔ [1148/1223] Built Mathlib.Logic.Function.CompTypeclasses (1.1s)
✔ [1149/1223] Built Mathlib.Algebra.Group.Pointwise.Set.Scalar (2.7s)
✔ [1150/1223] Built Mathlib.Algebra.GroupWithZero.Action.Defs (2.5s)
✔ [1151/1223] Built Mathlib.Algebra.Group.Submonoid.Basic (2.6s)
✔ [1152/1223] Built Mathlib.Data.Multiset.Bind (2.4s)
✔ [1153/1223] Built Mathlib.Data.Finset.Range (2.1s)
✔ [1154/1223] Built Mathlib.Data.Finset.SDiff (2.4s)
✔ [1155/1226] Built Mathlib.Data.Finset.Lattice.Lemmas (2.2s)
✔ [1156/1231] Built Mathlib.GroupTheory.Subsemigroup.Center (1.7s)
✔ [1157/1231] Built Mathlib.Algebra.Regular.SMul (2.1s)
✔ [1158/1231] Built Mathlib.Data.Finset.Disjoint (2.4s)
✔ [1159/1232] Built Mathlib.Algebra.Group.Action.Basic (2.3s)
✔ [1160/1232] Built Mathlib.Algebra.Group.Hom.CompTypeclasses (1.5s)
✔ [1161/1234] Built Mathlib.Algebra.Group.Submonoid.DistribMulAction (1.4s)
✔ [1162/1234] Built Mathlib.Algebra.Group.Subgroup.Defs (4.4s)
✔ [1163/1235] Built Mathlib.Algebra.Module.Defs (1.8s)
✔ [1164/1239] Built Mathlib.Algebra.Group.Action.TypeTags (1.5s)
✔ [1165/1239] Built Mathlib.Data.Multiset.Powerset (2.2s)
✔ [1166/1246] Built Mathlib.Algebra.GroupWithZero.Action.Units (1.7s)
✔ [1167/1248] Built Mathlib.Data.Multiset.Pi (2.2s)
✔ [1168/1256] Built Mathlib.Algebra.Group.Support (1.7s)
✔ [1169/1258] Built Mathlib.Algebra.Group.Commute.Hom (1.5s)
✔ [1170/1263] Built Mathlib.Data.Finset.Basic (3.3s)
✔ [1171/1263] Built Mathlib.Algebra.Group.Action.Pretransitive (1.0s)
✔ [1172/1263] Built Mathlib.Algebra.Order.Group.Action (2.0s)
✔ [1173/1264] Built Mathlib.Data.Finset.Image (3.7s)
✔ [1174/1266] Built Mathlib.Algebra.Ring.Divisibility.Basic (2.3s)
✔ [1175/1266] Built Mathlib.Algebra.Group.Irreducible.Lemmas (1.8s)
✔ [1176/1266] Built Mathlib.GroupTheory.GroupAction.Defs (3.9s)
✔ [1177/1266] Built Mathlib.Data.PNat.Basic (2.4s)
✔ [1178/1267] Built Mathlib.Algebra.Group.Action.Hom (1.7s)
✔ [1179/1267] Built Mathlib.Data.List.Permutation (2.2s)
✔ [1180/1267] Built Mathlib.Dynamics.FixedPoints.Basic (2.1s)
✔ [1181/1267] Built Mathlib.Data.Finset.BooleanAlgebra (2.3s)
✔ [1182/1267] Built Mathlib.Algebra.Group.Submonoid.Operations (6.9s)
✔ [1183/1267] Built Mathlib.Data.Fintype.OfMap (2.1s)
✔ [1184/1267] Built Mathlib.Data.Finset.Fold (2.3s)
✔ [1185/1267] Built Mathlib.Data.Finset.SymmDiff (2.0s)
✔ [1186/1268] Built Mathlib.Algebra.GroupWithZero.Action.End (1.5s)
✔ [1187/1275] Built Mathlib.Algebra.Prime.Lemmas (2.2s)
✔ [1188/1275] Built Mathlib.Algebra.Group.Embedding (1.6s)
✔ [1189/1275] Built Mathlib.Algebra.Order.Ring.Abs (2.7s)
✔ [1190/1277] Built Mathlib.Data.Finset.Piecewise (2.4s)
✔ [1191/1278] Built Mathlib.Algebra.Group.Pointwise.Set.Basic (8.4s)
✔ [1192/1278] Built Mathlib.Algebra.Ring.Action.Basic (1.8s)
✔ [1193/1283] Built Mathlib.GroupTheory.Submonoid.Center (3.3s)
✔ [1194/1284] Built Mathlib.Data.Fintype.Sets (2.9s)
✔ [1195/1284] Built Mathlib.Data.Finset.Union (3.4s)
✔ [1196/1284] Built Mathlib.Data.Finset.Card (5.2s)
✔ [1197/1287] Built Mathlib.Algebra.Notation.Indicator (2.5s)
✔ [1198/1287] Built Mathlib.Algebra.GroupWithZero.Associated (3.4s)
✔ [1199/1287] Built Mathlib.Order.Hom.WithTopBot (3.9s)
✔ [1200/1287] Built Mathlib.Algebra.Group.Subgroup.Lattice (5.2s)
✔ [1201/1287] Built Mathlib.Algebra.Group.Pointwise.Set.Lattice (2.8s)
✔ [1202/1288] Built Mathlib.Algebra.Group.Subsemigroup.MulOpposite (2.2s)
✔ [1203/1288] Built Mathlib.Data.Fintype.Basic (2.6s)
✔ [1204/1288] Built Mathlib.Algebra.Group.Idempotent (1.3s)
✔ [1205/1288] Built Mathlib.Data.Finset.Pi (2.4s)
✔ [1206/1288] Built Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (3.1s)
✔ [1207/1288] Built Mathlib.Data.Finset.Option (2.2s)
✔ [1208/1288] Built Mathlib.Data.Finset.Sum (2.6s)
✔ [1209/1288] Built Mathlib.Data.Finset.Prod (2.8s)
✔ [1210/1289] Built Mathlib.Algebra.BigOperators.Group.Finset.Defs (5.0s)
✔ [1211/1289] Built Mathlib.Data.Nat.Prime.Basic (2.5s)
✔ [1212/1289] Built Mathlib.Algebra.Ring.Associated (1.0s)
✔ [1213/1289] Built Mathlib.Algebra.FreeMonoid.Basic (3.9s)
✔ [1214/1293] Built Mathlib.Algebra.Group.Submonoid.MulOpposite (2.3s)
✔ [1215/1293] Built Mathlib.Algebra.Order.BigOperators.Group.List (2.6s)
✔ [1216/1293] Built Mathlib.Algebra.Group.Submonoid.Finite (2.1s)
✔ [1217/1294] Built Mathlib.Data.Fintype.Card (2.5s)
✔ [1218/1294] Built Mathlib.Order.Sigma.Lex (1.2s)
✔ [1219/1295] Built Mathlib.Algebra.Group.TransferInstance (2.4s)
✔ [1220/1295] Built Mathlib.Order.CompleteLattice.Finset (2.8s)
✔ [1221/1300] Built Mathlib.Algebra.CharP.Two (2.3s)
✔ [1222/1300] Built Mathlib.Algebra.Group.Subgroup.Map (4.0s)
✔ [1223/1300] Built Mathlib.Data.Fintype.EquivFin (2.4s)
✔ [1224/1306] Built Mathlib.Algebra.Group.Subgroup.MulOpposite (2.5s)
✔ [1225/1306] Built Mathlib.Algebra.Group.Commutator (1.3s)
✔ [1226/1306] Built Mathlib.Algebra.Group.Action.End (2.5s)
✔ [1227/1306] Built Mathlib.GroupTheory.GroupAction.Hom (10s)
✔ [1228/1306] Built Mathlib.GroupTheory.Subsemigroup.Centralizer (2.1s)
✔ [1229/1306] Built Mathlib.Data.Finset.Lattice.Fold (5.4s)
✔ [1230/1306] Built Mathlib.Algebra.Group.Subgroup.ZPowers.Basic (2.7s)
✔ [1231/1306] Built Mathlib.Data.Fintype.Prod (2.0s)
✔ [1232/1306] Built Mathlib.Data.Fintype.Option (1.8s)
✔ [1233/1306] Built Mathlib.Data.Fintype.Sum (2.1s)
✔ [1234/1306] Built Mathlib.Algebra.GCDMonoid.Basic (5.8s)
✔ [1235/1306] Built Mathlib.Basic.Denumerable (2.6s)
✔ [1236/1306] Built Mathlib.Algebra.BigOperators.Group.Finset.Basic (6.9s)
✔ [1237/1306] Built Mathlib.Algebra.Group.Action.Prod (2.1s)
✔ [1238/1306] Built Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic (1.8s)
✔ [1239/1306] Built Mathlib.Algebra.Group.Submonoid.Membership (4.5s)
✔ [1240/1306] Built Mathlib.Data.ZMod.Defs (2.8s)
✔ [1241/1306] Built Mathlib.GroupTheory.Submonoid.Centralizer (1.0s)
✔ [1242/1310] Built Mathlib.Data.Set.Finite.Basic (3.5s)
✔ [1243/1310] Built Mathlib.Algebra.Group.Subgroup.Ker (5.5s)
✔ [1244/1310] Built Mathlib.Data.Finset.Lattice.Union (2.1s)
✔ [1245/1310] Built Mathlib.Data.Finset.Sigma (2.3s)
✔ [1246/1310] Built Mathlib.Algebra.GCDMonoid.Nat (2.1s)
✔ [1247/1310] Built Mathlib.Algebra.GCDMonoid.Multiset (2.3s)
✔ [1248/1310] Built Mathlib.Data.Finset.Max (3.8s)
✔ [1249/1310] Built Mathlib.Logic.Equiv.List (2.5s)
✔ [1250/1310] Built Mathlib.SetTheory.Cardinal.Order (3.1s)
✔ [1251/1310] Built Mathlib.Algebra.BigOperators.GroupWithZero.Finset (2.5s)
✔ [1252/1310] Built Mathlib.Algebra.BigOperators.Option (2.3s)
✔ [1253/1310] Built Mathlib.Data.Finset.NoncommProd (3.5s)
✔ [1254/1310] Built Mathlib.Algebra.GroupWithZero.Action.Basic (2.3s)
✔ [1255/1310] Built Mathlib.Data.Fintype.Pi (2.3s)
✔ [1256/1310] Built Mathlib.Data.Set.Finite.Range (2.2s)
✔ [1257/1310] Built Mathlib.Algebra.Quotient (1.9s)
✔ [1258/1310] Built Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (3.7s)
✔ [1259/1314] Built Mathlib.Order.Preorder.Finite (2.6s)
✔ [1260/1314] Built Mathlib.Algebra.BigOperators.Group.Finset.Sigma (2.4s)
✔ [1261/1314] Built Mathlib.Data.Finset.Powerset (2.8s)
✔ [1262/1314] Built Mathlib.Data.Finset.Preimage (2.3s)
✔ [1263/1314] Built Mathlib.Data.Fintype.Sigma (2.5s)
✔ [1264/1314] Built Mathlib.Algebra.GCDMonoid.Finset (2.6s)
✔ [1265/1314] Built Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (2.5s)
✔ [1266/1315] Built Mathlib.Algebra.Group.Submonoid.BigOperators (2.8s)
✔ [1267/1319] Built Mathlib.Basic.Finite.Prod (2.5s)
✔ [1268/1319] Built Mathlib.Data.Set.Countable (2.4s)
✔ [1269/1319] Built Mathlib.GroupTheory.Coset.Defs (3.1s)
✔ [1270/1319] Built Mathlib.Data.Set.Finite.Powerset (1.0s)
✔ [1271/1325] Built Mathlib.Data.Fintype.List (2.3s)
✔ [1272/1325] Built Mathlib.Algebra.GroupWithZero.Action.Opposite (1.4s)
✔ [1273/1325] Built Mathlib.Data.Fintype.Powerset (2.0s)
✔ [1274/1325] Built Mathlib.GroupTheory.Congruence.Defs (3.8s)
✔ [1275/1325] Built Mathlib.Algebra.Module.NatInt (2.3s)
✔ [1276/1328] Built Mathlib.Algebra.Regular.Opposite (1.4s)
✔ [1277/1328] Built Mathlib.Data.Fintype.Vector (1.9s)
✔ [1278/1328] Built Mathlib.Algebra.Group.Subgroup.Basic (7.5s)
✔ [1279/1329] Built Mathlib.Algebra.Group.Pointwise.Set.Finite (2.4s)
✔ [1280/1329] Built Mathlib.Logic.Equiv.Sigma (1.6s)
✔ [1281/1329] Built Mathlib.Algebra.Module.Opposite (1.6s)
✔ [1282/1329] Built Mathlib.Data.Nat.Log (2.4s)
✔ [1283/1331] Built Mathlib.Data.Set.Finite.Lattice (3.8s)
✔ [1284/1331] Built Mathlib.Data.Nat.Prime.Pow (2.3s)
✔ [1285/1331] Built Mathlib.GroupTheory.Congruence.Hom (3.0s)
✔ [1286/1331] Built Mathlib.Data.List.Cycle (3.0s)
✔ [1287/1331] Built Mathlib.Order.Interval.Finset.Defs (6.2s)
✔ [1288/1331] Built Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (3.0s)
✔ [1289/1331] Built Mathlib.Data.Fintype.BigOperators (3.3s)
✔ [1290/1331] Built Mathlib.GroupTheory.Subgroup.Center (2.9s)
✔ [1291/1335] Built Mathlib.Basic.Finite.Sigma (1.9s)
✔ [1292/1335] Built Mathlib.Algebra.IsPrimePow (2.1s)
✔ [1293/1335] Built Mathlib.Algebra.Module.Torsion.Free (2.4s)
✔ [1294/1335] Built Mathlib.Algebra.Order.BigOperators.Group.Multiset (2.4s)
✔ [1295/1335] Built Mathlib.Algebra.Order.Monoid.Multiset (1.8s)
✔ [1296/1336] Built Mathlib.GroupTheory.Coset.Basic (5.4s)
✔ [1297/1336] Built Mathlib.Dynamics.PeriodicPts.Defs (2.6s)
✔ [1298/1339] Built Mathlib.Order.ConditionallyCompleteLattice.Finset (3.4s)
✔ [1299/1339] Built Mathlib.Algebra.Group.Subgroup.Actions (2.0s)
✔ [1300/1342] Built Mathlib.Algebra.Ring.CharZero (2.9s)
✔ [1301/1345] Built Mathlib.Order.Interval.Set.SuccPred (3.3s)
✔ [1302/1345] Built Mathlib.GroupTheory.Subgroup.Centralizer (4.1s)
✔ [1303/1347] Built Mathlib.GroupTheory.QuotientGroup.Defs (5.7s)
✔ [1304/1349] Built Mathlib.SetTheory.Cardinal.Basic (5.0s)
✔ [1305/1349] Built Mathlib.Data.List.NatAntidiagonal (3.1s)
✔ [1306/1349] Built Mathlib.Order.Interval.Finset.Basic (6.2s)
✔ [1307/1349] Built Mathlib.Data.List.Prime (2.3s)
✔ [1308/1349] Built Mathlib.Algebra.BigOperators.Ring.List (3.1s)
✔ [1309/1349] Built Mathlib.Algebra.Order.Antidiag.Prod (6.5s)
✔ [1310/1350] Built Mathlib.Data.Nat.Prime.Infinite (4.6s)
✔ [1311/1350] Built Mathlib.Order.Interval.Finset.SuccPred (5.8s)
✔ [1312/1350] Built Mathlib.GroupTheory.GroupAction.ConjAct (5.6s)
✔ [1313/1350] Built Mathlib.Algebra.Order.BigOperators.Group.Finset (9.3s)
✔ [1314/1350] Built Mathlib.Order.Interval.Set.Infinite (4.9s)
✔ [1315/1357] Built Mathlib.Tactic.FinCases (4.3s)
✔ [1316/1357] Built Mathlib.Data.Multiset.NatAntidiagonal (2.4s)
✔ [1317/1357] Built Mathlib.GroupTheory.GroupAction.Basic (7.2s)
✔ [1318/1357] Built Mathlib.SetTheory.Cardinal.ENat (4.0s)
✔ [1319/1360] Built Mathlib.Order.Interval.Multiset (2.5s)
✔ [1320/1360] Built Mathlib.Algebra.Module.RingHom (1.0s)
✔ [1321/1360] Built Aeneas.Tactic.Simproc.ReduceZMod.Init (2.5s)
✔ [1322/1360] Built Mathlib.Data.Nat.Factors (2.7s)
✔ [1323/1362] Built Mathlib.Algebra.Order.Interval.Finset.SuccPred (3.0s)
✔ [1324/1364] Built Mathlib.GroupTheory.GroupAction.SubMulAction (10s)
✔ [1325/1370] Built Mathlib.Data.Finset.NatAntidiagonal (2.6s)
✔ [1326/1370] Built Mathlib.Algebra.EuclideanDomain.Defs (1.0s)
✔ [1327/1374] Built Mathlib.SetTheory.Cardinal.ToNat (2.6s)
✔ [1328/1374] Built Mathlib.Data.Nat.Prime.Int (2.3s)
✔ [1329/1374] Built Mathlib.Algebra.GroupWithZero.Action.Regular (1.8s)
✔ [1330/1374] Built Mathlib.GroupTheory.Commutator.Basic (9.7s)
✔ [1331/1374] Built Mathlib.Order.Interval.Finset.Nat (3.1s)
✔ [1332/1374] Built Mathlib.Algebra.Group.PUnit (1.6s)
✔ [1333/1374] Built Mathlib.Data.Nat.PrimeFin (2.7s)
✔ [1334/1376] Built Mathlib.Algebra.EuclideanDomain.Field (2.1s)
✔ [1335/1376] Built Mathlib.Algebra.EuclideanDomain.Int (1.8s)
✔ [1336/1376] Built Aeneas.Tactic.Solver.ScalarTac.CondSimpTac (5.8s)
✔ [1337/1376] Built Mathlib.Algebra.EuclideanDomain.Basic (3.0s)
✔ [1338/1378] Built Mathlib.Algebra.Module.Submodule.Defs (4.2s)
✔ [1339/1378] Built Mathlib.SetTheory.Cardinal.Finite (3.3s)
✔ [1340/1378] Built Mathlib.Algebra.Ring.PUnit (1.8s)
✔ [1341/1378] Built Mathlib.Order.Lattice.Nat (2.9s)
✔ [1342/1378] Built Mathlib.Algebra.GroupWithZero.NonZeroDivisors (4.0s)
✔ [1343/1378] Built Mathlib.Algebra.GroupWithZero.Idempotent (1.8s)
✔ [1344/1379] Built Mathlib.Tactic.Abel (4.7s)
✔ [1345/1379] Built Mathlib.Algebra.GroupWithZero.Action.Prod (2.3s)
✔ [1346/1379] Built Mathlib.GroupTheory.GroupAction.Quotient (5.6s)
✔ [1347/1379] Built Mathlib.Algebra.Module.PUnit (2.1s)
✔ [1348/1379] Built Mathlib.Algebra.GroupWithZero.Units.Fintype (2.8s)
✔ [1349/1389] Built Mathlib.Dynamics.PeriodicPts.Lemmas (2.6s)
✔ [1350/1392] Built Mathlib.Algebra.Ring.Idempotent (2.1s)
✔ [1351/1393] Built Mathlib.Algebra.Module.LinearMap.Defs (10s)
✔ [1352/1393] Built Mathlib.Order.OrderIsoNat (2.0s)
✔ [1353/1393] Built Mathlib.GroupTheory.Coset.Card (4.8s)
✔ [1354/1393] Built Mathlib.Algebra.Module.Prod (2.0s)
✔ [1355/1393] Built Mathlib.RingTheory.Ideal.Defs (3.3s)
✔ [1356/1397] Built Mathlib.Algebra.Module.Submodule.Basic (3.3s)
✔ [1357/1397] Built Mathlib.Basic.Finite.Set (2.4s)
✔ [1358/1400] Built Mathlib.Data.Finset.Order (2.2s)
✔ [1359/1402] Built Mathlib.Data.Set.Card (6.8s)
✔ [1360/1402] Built Mathlib.Algebra.Algebra.Defs (3.2s)
✔ [1361/1405] Built Mathlib.NumberTheory.Divisors (9.5s)
✔ [1362/1410] Built Mathlib.Data.Set.Lattice.Order (2.4s)
✔ [1363/1413] Built Mathlib.Order.Hom.CompleteLattice (4.4s)
✔ [1364/1415] Built Mathlib.Data.Set.Monotone (2.2s)
✔ [1365/1417] Built Mathlib.Order.Interval.Set.OrderIso (2.1s)
✔ [1366/1417] Built Mathlib.Order.WellQuasiOrder (2.8s)
✔ [1367/1418] Built Mathlib.Order.Closure (3.1s)
✔ [1368/1419] Built Mathlib.Data.Finset.Lattice.Prod (3.1s)
✔ [1369/1419] Built Mathlib.Algebra.GroupWithZero.Pi (1.5s)
✔ [1370/1419] Built Mathlib.Algebra.Module.Torsion.Field (2.3s)
✔ [1371/1419] Built Mathlib.Algebra.Group.Action.Pi (2.2s)
✔ [1372/1419] Built Mathlib.SetTheory.Cardinal.NatCard (2.8s)
✔ [1373/1420] Built Mathlib.Tactic.Ring.PNat (2.7s)
✔ [1374/1421] Built Mathlib.Algebra.Order.SuccPred.WithBot (2.0s)
✔ [1375/1421] Built Mathlib.Order.ModularLattice (4.3s)
✔ [1376/1424] Built Mathlib.Algebra.GroupWithZero.Action.Pi (2.7s)
✔ [1377/1424] Built Mathlib.Data.ENat.Lattice (3.4s)
✔ [1378/1424] Built Mathlib.Algebra.Ring.Pi (3.5s)
✔ [1379/1424] Built Mathlib.Order.WellFoundedSet (4.2s)
✔ [1380/1424] Built Mathlib.Algebra.Group.Subgroup.Finite (4.1s)
✔ [1381/1424] Built Mathlib.Order.SupClosed (4.8s)
✔ [1382/1424] Built Mathlib.Algebra.Module.Equiv.Defs (10s)
✔ [1383/1424] Built Mathlib.Data.DFinsupp.Defs (6.5s)
✔ [1384/1426] Built Mathlib.Tactic.Ring (3.1s)
✔ [1385/1429] Built Mathlib.Data.Fintype.Pigeonhole (2.8s)
✔ [1386/1434] Built Mathlib.Basic.Rel (4.0s)
✔ [1387/1434] Built Mathlib.Data.Fin.VecNotation (4.1s)
✔ [1388/1436] Built Mathlib.Algebra.Module.Pi (2.8s)
✔ [1389/1438] Built Mathlib.Algebra.Module.Equiv.Opposite (2.8s)
✔ [1390/1438] Built Mathlib.Algebra.Group.Hom.End (2.3s)
✔ [1391/1438] Built Mathlib.Algebra.GroupWithZero.ULift (1.7s)
✔ [1392/1439] Built Mathlib.Order.SupIndep (5.4s)
✔ [1393/1439] Built Mathlib.Algebra.GroupWithZero.Action.Hom (2.6s)
✔ [1394/1439] Built Mathlib.Algebra.Group.Submonoid.Pointwise (4.7s)
✔ [1395/1439] Built Mathlib.Algebra.Module.Torsion.Pi (2.9s)
✔ [1396/1440] Built Mathlib.Algebra.Module.Submodule.Lattice (5.7s)
✔ [1397/1440] Built Mathlib.Data.DFinsupp.Module (3.6s)
✔ [1398/1441] Built Mathlib.Order.Atoms (7.8s)
✔ [1399/1441] Built Mathlib.Algebra.Module.End (2.0s)
✔ [1400/1442] Built Mathlib.RingTheory.NonUnitalSubsemiring.Defs (3.7s)
✔ [1401/1442] Built Mathlib.Algebra.Ring.Action.Subobjects (2.6s)
✔ [1402/1442] Built Mathlib.Algebra.Module.ULift (3.4s)
✔ [1403/1442] Built Mathlib.Algebra.Group.Subsemigroup.Membership (2.3s)
✔ [1404/1443] Built Mathlib.GroupTheory.GroupAction.DomAct.Basic (3.5s)
✔ [1405/1444] Built Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise (2.0s)
✔ [1406/1444] Built Mathlib.Algebra.Module.LinearMap.End (5.7s)
✔ [1407/1444] Built Mathlib.Order.RelSeries (7.0s)
✔ [1408/1444] Built Mathlib.RingTheory.Ideal.Lattice (2.5s)
✔ [1409/1444] Built Mathlib.Algebra.Module.Submodule.RestrictScalars (3.4s)
✔ [1410/1444] Built Mathlib.Algebra.Group.Subgroup.Pointwise (4.0s)
✔ [1411/1444] Built Mathlib.Algebra.GroupWithZero.Center (2.3s)
✔ [1412/1447] Built Mathlib.LinearAlgebra.Span.Defs (4.9s)
✔ [1413/1447] Built Mathlib.Order.CompactlyGenerated.Basic (4.3s)
✔ [1414/1447] Built Mathlib.Algebra.Ring.Center (2.9s)
✔ [1415/1447] Built Mathlib.RingTheory.NonUnitalSubring.Defs (3.5s)
✔ [1416/1449] Built Mathlib.Algebra.Module.Hom (3.3s)
✔ [1417/1453] Built Mathlib.Algebra.Ring.Subsemiring.Defs (3.9s)
✔ [1418/1453] Built Mathlib.Algebra.Ring.Centralizer (1.7s)
✔ [1419/1453] Built Mathlib.Algebra.Module.LinearMap.Basic (3.3s)
✔ [1420/1455] Built Mathlib.Algebra.Group.Subsemigroup.Operations (5.2s)
✔ [1421/1459] Built Mathlib.RingTheory.Ideal.Prime (2.6s)
✔ [1422/1459] Built Mathlib.Algebra.Module.Submodule.LinearMap (3.9s)
✔ [1423/1465] Built Mathlib.Algebra.Ring.Submonoid.Basic (2.2s)
✔ [1424/1469] Built Mathlib.Algebra.Ring.Hom.InjSurj (1.9s)
✔ [1425/1472] Built Mathlib.Algebra.GroupWithZero.Subgroup (3.0s)
✔ [1426/1473] Built Mathlib.Order.KrullDimension (5.1s)
✔ [1427/1473] Built Mathlib.Algebra.Group.Action.TransferInstance (2.9s)
✔ [1428/1473] Built Mathlib.Algebra.NoZeroSMulDivisors.Defs (2.4s)
✔ [1429/1473] Built Mathlib.Algebra.Ring.Subring.Defs (4.1s)
✔ [1430/1476] Built Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (2.2s)
✔ [1431/1476] Built Mathlib.Algebra.Ring.Aut (2.5s)
✔ [1432/1476] Built Mathlib.GroupTheory.QuotientGroup.Basic (7.2s)
✔ [1433/1478] Built Mathlib.Algebra.GroupWithZero.Action.TransferInstance (2.5s)
✔ [1434/1478] Built Mathlib.Algebra.Group.Pointwise.Set.BigOperators (2.9s)
✔ [1435/1478] Built Mathlib.RingTheory.NonUnitalSubsemiring.Basic (4.8s)
✔ [1436/1478] Built Mathlib.Algebra.Group.IsApply (2.1s)
✔ [1437/1480] Built Mathlib.Algebra.Group.Shrink (3.0s)
✔ [1438/1481] Built Mathlib.Data.Finset.NAry (3.6s)
✔ [1439/1481] Built Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (2.8s)
✔ [1440/1483] Built Mathlib.Algebra.Module.Submodule.Map (6.4s)
✔ [1441/1483] Built Mathlib.Algebra.Ring.Action.Group (2.3s)
✔ [1442/1483] Built Mathlib.Algebra.FiniteSupport.Defs (2.2s)
✔ [1443/1483] Built Mathlib.Algebra.Module.TransferInstance (2.5s)
✔ [1444/1483] Built Mathlib.Algebra.Group.Indicator (2.5s)
✔ [1445/1484] Built Mathlib.Algebra.GroupWithZero.Indicator (2.2s)
✔ [1446/1484] Built Mathlib.Algebra.Module.Basic (2.0s)
✔ [1447/1484] Built Mathlib.RingTheory.NonUnitalSubring.Basic (5.3s)
✔ [1448/1484] Built Mathlib.Algebra.Module.Equiv.Basic (11s)
✔ [1449/1488] Built Mathlib.Algebra.BigOperators.Pi (4.0s)
✔ [1450/1488] Built Mathlib.Algebra.Notation.FiniteSupport (2.8s)
✔ [1451/1491] Built Mathlib.Algebra.Ring.Subsemiring.Basic (6.6s)
✔ [1452/1492] Built Mathlib.GroupTheory.Index (7.6s)
✔ [1453/1492] Built Mathlib.Algebra.Module.Submodule.Pointwise (4.9s)
✔ [1454/1492] Built Mathlib.Algebra.Module.Submodule.Ker (4.6s)
✔ [1455/1492] Built Mathlib.Algebra.Module.Shrink (2.5s)
✔ [1456/1499] Built Mathlib.Algebra.Order.Group.Indicator (2.7s)
✔ [1457/1499] Built Mathlib.Algebra.BigOperators.Group.Finset.Pi (2.5s)
✔ [1458/1499] Built Mathlib.Data.Multiset.Antidiagonal (2.5s)
✔ [1459/1499] Built Mathlib.Data.Multiset.Sections (2.2s)
✔ [1460/1499] Built Mathlib.Algebra.Group.Pointwise.Finset.Basic (8.5s)
✔ [1461/1499] Built Mathlib.Algebra.Order.Hom.GroupNorm (2.1s)
✔ [1462/1499] Built Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (1.8s)
✔ [1463/1500] Built Mathlib.Algebra.Module.Submodule.EqLocus (2.5s)
✔ [1464/1508] Built Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (2.8s)
✔ [1465/1511] Built Mathlib.Algebra.Order.BigOperators.Ring.List (2.2s)
✔ [1466/1517] Built Mathlib.Algebra.Order.Hom.RingNorm (2.1s)
✔ [1467/1518] Built Mathlib.Algebra.BigOperators.Ring.Multiset (2.7s)
✔ [1468/1518] Built Mathlib.Algebra.FiniteSupport.Basic (3.5s)
✔ [1469/1519] Built Mathlib.Algebra.Group.Pi.Torsion (1.0s)
✔ [1470/1521] Built Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (2.6s)
✔ [1471/1521] Built Mathlib.Data.List.Find (2.3s)
✔ [1472/1521] Built Mathlib.Algebra.Module.Submodule.Range (4.6s)
✔ [1473/1523] Built Mathlib.Algebra.BigOperators.Group.Finset.Preimage (2.9s)
✔ [1474/1523] Built Mathlib.Data.Rat.BigOperators (2.7s)
✔ [1475/1524] Built Mathlib.Algebra.Ring.NonZeroDivisors (2.5s)
✔ [1476/1525] Built Mathlib.Data.Multiset.Find (2.4s)
✔ [1477/1525] Built Mathlib.Algebra.Order.BigOperators.Ring.Multiset (2.5s)
✔ [1478/1527] Built Mathlib.Algebra.Ring.Subring.Basic (8.9s)
✔ [1479/1527] Built Mathlib.Algebra.Order.AbsoluteValue.Basic (3.9s)
✔ [1480/1528] Built Mathlib.Algebra.BigOperators.Ring.Finset (4.1s)
✔ [1481/1528] Built Mathlib.Algebra.Ring.Submonoid.Pointwise (3.5s)
✔ [1482/1528] Built Mathlib.Algebra.Order.Kleene (3.8s)
✔ [1483/1531] Built Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (2.0s)
✔ [1484/1531] Built Mathlib.Data.Fintype.Lattice (2.4s)
✔ [1485/1536] Built Mathlib.Algebra.Field.IsField (2.2s)
✔ [1486/1536] Built Mathlib.Data.Finsupp.Defs (3.3s)
✔ [1487/1539] Built Mathlib.Algebra.Module.Submodule.Equiv (4.5s)
✔ [1488/1541] Built Mathlib.RingTheory.Coprime.Basic (3.5s)
✔ [1489/1541] Built Mathlib.Data.Finset.Fin (2.5s)
✔ [1490/1541] Built Mathlib.Algebra.Order.BigOperators.Ring.Finset (4.3s)
✔ [1491/1541] Built Mathlib.Algebra.Algebra.Basic (5.2s)
✔ [1492/1541] Built Mathlib.Data.Set.Semiring (3.6s)
✔ [1493/1541] Built Mathlib.Order.Interval.Set.Fin (3.8s)
✔ [1494/1544] Built Mathlib.Data.Fintype.Order (3.6s)
✔ [1495/1545] Built Mathlib.Data.Finsupp.Single (3.5s)
✔ [1496/1545] Built Mathlib.Order.SuccPred.LinearLocallyFinite (3.0s)
✔ [1497/1545] Built Mathlib.Algebra.Order.Interval.Set.Monoid (2.3s)
✔ [1498/1545] Built Mathlib.Algebra.BigOperators.NatAntidiagonal (2.4s)
✔ [1499/1545] Built Mathlib.RingTheory.Coprime.Lemmas (3.4s)
✔ [1500/1547] Built Mathlib.Order.PartialSups (3.1s)
✔ [1501/1547] Built Mathlib.GroupTheory.OrderOfElement (18s)
✔ [1502/1549] Built Mathlib.Order.Interval.Finset.Fin (4.5s)
✔ [1503/1549] Built Mathlib.Data.Finsupp.Indicator (3.4s)
✔ [1504/1554] Built Mathlib.LinearAlgebra.Span.Basic (7.1s)
✔ [1505/1554] Built Mathlib.Algebra.Algebra.Hom (5.6s)
✔ [1506/1554] Built Mathlib.Algebra.Group.Finsupp (4.9s)
✔ [1507/1554] Built Mathlib.Algebra.Order.Interval.Finset.Basic (3.2s)
✔ [1508/1554] Built Mathlib.Tactic.Order.CollectFacts (3.5s)
✔ [1509/1554] Built Mathlib.Order.Disjointed (3.4s)
✔ [1510/1554] Built Mathlib.RingTheory.Multiplicity (6.5s)
✔ [1511/1554] Built Mathlib.RingTheory.Ideal.Span (4.3s)
✔ [1512/1554] Built Mathlib.Data.Finsupp.SMulWithZero (3.1s)
✔ [1513/1554] Built Mathlib.Algebra.BigOperators.Finprod (10s)
✔ [1514/1557] Built Mathlib.Data.Finsupp.Ext (3.5s)
✔ [1515/1559] Built Mathlib.Data.ZMod.Basic (6.6s)
✔ [1516/1559] Built Mathlib.Tactic.Order.Preprocessing (2.8s)
✔ [1517/1559] Built Mathlib.Tactic.Order.Graph.Basic (2.1s)
✔ [1518/1559] Built Mathlib.Tactic.Order.ToInt (3.5s)
✔ [1519/1562] Built Mathlib.LinearAlgebra.BilinearMap (14s)
✔ [1520/1564] Built Mathlib.RingTheory.Ideal.Maximal (3.4s)
✔ [1521/1564] Built Mathlib.Algebra.BigOperators.GroupWithZero.Action (2.7s)
✔ [1522/1564] Built Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (3.9s)
✔ [1523/1564] Built Mathlib.Algebra.Algebra.NonUnitalHom (8.1s)
✔ [1524/1565] Built Mathlib.Tactic.Order.Graph.Tarjan (2.0s)
✔ [1525/1565] Built Mathlib.Algebra.Algebra.Equiv (8.0s)
✔ [1526/1565] Built Mathlib.Algebra.Algebra.ZMod (2.9s)
✔ [1527/1566] Built Mathlib.Order.Filter.Defs (3.4s)
✔ [1528/1570] Built Mathlib.Order.Interval.Set.Disjoint (3.3s)
✔ [1529/1570] Built Mathlib.Algebra.Module.BigOperators (3.6s)
✔ [1530/1570] Built Mathlib.RingTheory.Ideal.Nonunits (3.9s)
✔ [1531/1570] Built Mathlib.Algebra.Module.Submodule.Bilinear (3.9s)
✔ [1532/1571] Built Mathlib.Algebra.Order.Group.Basic (3.0s)
✔ [1533/1574] Built Mathlib.Algebra.BigOperators.Finsupp.Basic (6.8s)
✔ [1534/1576] Built Mathlib.Tactic.Order (4.2s)
✔ [1535/1576] Built Mathlib.Algebra.BigOperators.Intervals (5.7s)
✔ [1536/1577] Built Mathlib.Algebra.Order.GroupWithZero.Synonym (2.3s)
✔ [1537/1577] Built Mathlib.Algebra.Order.Group.Action.Synonym (2.6s)
✔ [1538/1577] Built Mathlib.Algebra.Algebra.Opposite (5.8s)
✔ [1539/1577] Built Mathlib.Algebra.Group.Fin.Tuple (3.3s)
✔ [1540/1578] Built Mathlib.Order.Filter.Basic (5.9s)
✔ [1541/1578] Built Mathlib.Algebra.Algebra.Prod (4.2s)
✔ [1542/1578] Built Aeneas.Tactic.Simproc.ReduceZMod.ReduceZMod (7.7s)
✔ [1543/1580] Built Mathlib.Algebra.Group.Graph (5.4s)
✔ [1544/1580] Built Mathlib.Logic.Equiv.Fin.Basic (4.5s)
✔ [1545/1580] Built Mathlib.Algebra.Order.GroupWithZero.Action.Synonym (3.5s)
✔ [1546/1585] Built Mathlib.Data.Set.Finite.Lemmas (3.9s)
✔ [1547/1585] Built Mathlib.Data.Nat.Choose.Sum (5.3s)
✔ [1548/1595] Built Mathlib.Order.Filter.AtTopBot.Defs (3.5s)
✔ [1549/1595] Built Mathlib.LinearAlgebra.Quotient.Defs (5.5s)
✔ [1550/1596] Built Mathlib.LinearAlgebra.TensorProduct.Defs (8.8s)
✔ [1551/1597] Built Mathlib.Order.Filter.Map (4.8s)
✔ [1552/1597] Built Mathlib.Order.Filter.AtTopBot.Disjoint (1.9s)
✔ [1553/1597] Built Mathlib.Algebra.GroupWithZero.Submonoid.Primal (2.4s)
✔ [1554/1597] Built Mathlib.Data.BitVec (2.4s)
✔ [1555/1600] Built Mathlib.Data.Finsupp.Basic (10s)
✔ [1556/1600] Built Mathlib.Algebra.Algebra.Tower (5.3s)
✔ [1557/1600] Built Mathlib.Order.Filter.Tendsto (2.7s)
✔ [1558/1600] Built Aeneas.Tactic.Solver.ScalarTac.Lemmas (8.4s)
✔ [1559/1610] Built Mathlib.Order.Filter.Bases.Basic (3.8s)
✔ [1560/1610] Built Aeneas.Std.Scalar.BvComp (5.2s)
✔ [1561/1611] Built Mathlib.GroupTheory.FreeGroup.Basic (8.5s)
✔ [1562/1611] Built Mathlib.Algebra.Order.Module.Defs (7.0s)
✔ [1563/1613] Built Mathlib.RingTheory.UniqueFactorizationDomain.Defs (3.0s)
✔ [1564/1613] Built Mathlib.LinearAlgebra.Prod (9.9s)
✔ [1565/1613] Built Mathlib.Tactic.Algebraize (3.8s)
✔ [1566/1617] Built Mathlib.Data.Finsupp.Option (3.1s)
✔ [1567/1617] Built Mathlib.Order.Filter.AtTopBot.Tendsto (2.3s)
✔ [1568/1619] Built Mathlib.Data.Finsupp.SMul (2.0s)
✔ [1569/1624] Built Mathlib.Data.List.GetD (1.6s)
✔ [1570/1624] Built Batteries.Data.Nat.Bitwise.Lemmas (823ms)
✔ [1571/1626] Built Mathlib.Algebra.Order.Nonneg.Module (2.7s)
✔ [1572/1626] Built Aeneas.Tactic.Simp.SimpLemmas (1.7s)
✔ [1573/1628] Built Mathlib.LinearAlgebra.TensorProduct.Basic (8.1s)
✔ [1574/1628] Built Aeneas.Std.Scalar.CloneCopy (3.9s)
✔ [1575/1629] Built Batteries.Data.Nat.Bitwise (641ms)
✔ [1576/1629] Built Batteries.Data.BitVec.Basic (594ms)
✔ [1577/1631] Built Aeneas.Data.ListN (1.2s)
✔ [1578/1631] Built Batteries.Data.Fin.OfBits (596ms)
✔ [1579/1633] Built Batteries.Data.Int (693ms)
✔ [1580/1633] Built Aeneas.Std.Core.Default (2.3s)
✔ [1581/1639] Built Mathlib.Order.Filter.AtTopBot.Basic (3.1s)
✔ [1582/1645] Built Aeneas.Tactic.Conv.Natify.Init (1.7s)
✔ [1583/1646] Built Batteries.Data.BitVec.Lemmas (909ms)
✔ [1584/1647] Built Aeneas.Tactic.Conv.ZModify.Init (1.7s)
✔ [1585/1656] Built Aeneas.Data.Byte (2.5s)
✔ [1586/1657] Built Mathlib.GroupTheory.Finiteness (6.1s)
✔ [1587/1657] Built Mathlib.Data.Nat.Bitwise (3.2s)
✔ [1588/1657] Built Aeneas.Tactic.Simproc.ReduceNat (2.6s)
✔ [1589/1657] Built Mathlib.LinearAlgebra.Finsupp.Defs (5.5s)
✔ [1590/1658] Built Mathlib.LinearAlgebra.Pi (6.3s)
✔ [1591/1659] Built Aeneas.Std.SliceDef (4.4s)
✔ [1592/1659] Built Aeneas.Std.Scalar.LeadingZeros (4.2s)
✔ [1593/1660] Built Mathlib.RingTheory.Finiteness.Defs (3.2s)
✔ [1594/1661] Built Aeneas.Std.Scalar.Pow (4.2s)
✔ [1595/1661] Built Aeneas.Std.Scalar.Rotate (4.1s)
✔ [1596/1661] Built Aeneas.Std.Scalar.EqOrd (5.1s)
✔ [1597/1664] Built Aeneas.Std.Scalar.SaturatingOps (3.8s)
✔ [1598/1664] Built Aeneas.Tactic.Simp.SimpLists.SimpLists (3.6s)
✔ [1599/1669] Built Aeneas.Tactic.Simp.SimpScalar.SimpScalar (3.9s)
✔ [1600/1670] Built Mathlib.LinearAlgebra.TensorProduct.Map (9.9s)
✔ [1601/1670] Built Aeneas.Std.StringDef (3.8s)
✔ [1602/1670] Built Mathlib.LinearAlgebra.Finsupp.LSum (4.4s)
✔ [1603/1670] Built Aeneas.Std.Scalar.WrappingOps.Add (4.3s)
✔ [1604/1677] Built Aeneas.Std.Scalar.WrappingOps.Mul (4.2s)
✔ [1605/1677] Built Mathlib.RingTheory.Finiteness.Basic (4.4s)
✔ [1606/1677] Built Aeneas.Std.Scalar.WrappingOps.Shl (4.1s)
✔ [1607/1680] Built Aeneas.Std.Scalar.WrappingOps.Shr (4.0s)
✔ [1608/1685] Built Aeneas.Std.Scalar.WrappingOps.Sub (4.2s)
✔ [1609/1686] Built Mathlib.Control.Lawful (1.2s)
✔ [1610/1689] Built Aeneas.Tactic.Simp.SimpScalar.Lemmas (4.4s)
✔ [1611/1691] Built Mathlib.Control.Monad.Writer (1.7s)
✔ [1612/1692] Built Aeneas.Std.Alloc.String (2.1s)
✔ [1613/1693] Built Aeneas.Std.RawPtr (3.5s)
✔ [1614/1695] Built Mathlib.LinearAlgebra.Finsupp.Supported (3.1s)
✔ [1615/1695] Built Aeneas.Std.Core.Atomic (2.4s)
✔ [1616/1696] Built Mathlib.RingTheory.Noetherian.Defs (2.0s)
✔ [1617/1696] Built Mathlib.Algebra.Algebra.Bilinear (4.0s)
✔ [1618/1696] Built Mathlib.Control.Monad.Cont (1.0s)
✔ [1619/1698] Built Aeneas.Std.Core.CoreResult (2.9s)
✔ [1620/1701] Built Aeneas.Std.Scalar.WrappingOps (3.5s)
✔ [1621/1701] Built Aeneas.Std.Core.Panic (2.2s)
✔ [1622/1714] Built Aeneas.Std.Core.Marker (2.9s)
✔ [1623/1716] Built Aeneas.Std.Core.Pin (2.1s)
✔ [1624/1717] Built Aeneas.Tactic.Simp.SimpScalar.Tests (3.9s)
✔ [1625/1720] Built Mathlib.Algebra.Module.Submodule.Finsupp (2.5s)
✔ [1626/1720] Built Aeneas.Tactic.Simp.SimpIfs.Init (1.8s)
✔ [1627/1720] Built Aeneas.Std.PrimitivesLemmas (2.0s)
✔ [1628/1720] Built Aeneas.Std.Core.Ptr (3.9s)
✔ [1629/1722] Built Aeneas.Data.Tuples (2.4s)
✔ [1630/1722] Built Aeneas.Data.Range.DivRange.Basic (2.4s)
✔ [1631/1724] Built Mathlib.LinearAlgebra.Finsupp.LinearCombination (4.6s)
✔ [1632/1724] Built Aeneas.Data.Fin (3.6s)
✔ [1633/1725] Built Aeneas.Tactic.Simp.SimpScalar (3.5s)
✔ [1634/1743] Built Aeneas.Data.Range.Lemmas (2.4s)
✔ [1635/1744] Built Aeneas.Do.Elab (4.9s)
✔ [1636/1746] Built Aeneas.Data.Range.Notations (3.5s)
✔ [1637/1746] Built Aeneas.Data.Range.MulRange.Basic (2.2s)
✔ [1638/1749] Built Aeneas.Tactic.Elab.TraitDefault.Test (957ms)
✔ [1639/1749] Built Aeneas.Tactic.Simp.SimpIfs.SimpIfs (3.5s)
✔ [1640/1750] Built Aeneas.Std.Core.Alloc (3.5s)
✔ [1641/1750] Built Aeneas.Tactic.Misc.FCongr.FCongr (972ms)
✔ [1642/1750] Built Aeneas.Data.Range.DivRange.Lemmas (2.9s)
✔ [1643/1751] Built Aeneas.Tactic.Misc.FApplyExact (1.8s)
✔ [1644/1751] Built Aeneas.Data.Range.SRRange.Basic (2.3s)
✔ [1645/1752] Built Aeneas.Tactic.Elab.TraitDefault (967ms)
✔ [1646/1752] Built Mathlib.RingTheory.Ideal.Basic (3.2s)
✔ [1647/1752] Built Aeneas.Tactic.Misc.FCongr (973ms)
✔ [1648/1759] Built Aeneas.Tactic.Elab (890ms)
✔ [1649/1762] Built Aeneas.Tactic.RustAttributes (1.7s)
✔ [1650/1765] Built Aeneas.Tactic.Misc.Let.Let (2.3s)
✔ [1651/1767] Built Aeneas.Data.Range.DivRange.Notations (3.7s)
✔ [1652/1767] Built Mathlib.Algebra.Algebra.Operations (7.2s)
✔ [1653/1767] Built Aeneas.Data.Range.MulRange.Notations (3.7s)
✔ [1654/1768] Built Aeneas.Tactic.Solver.BvTac.Init (1.5s)
✔ [1655/1771] Built Aeneas.Tactic.Simp.SimpIfs (3.8s)
✔ [1656/1773] Built Aeneas.Tactic.Misc.Let (1.7s)
✔ [1657/1774] Built Aeneas.Data.Range.MulRange.Lemmas (3.5s)
✔ [1658/1774] Built Aeneas.Data.Range.SRRange.Notations (3.5s)
✔ [1659/1777] Built Aeneas.Tactic.Simproc.ReduceFin.Init (1.5s)
✔ [1660/1781] Built Aeneas.Tactic.Simp.SimpBoolProp (3.4s)
✔ [1661/1783] Built Aeneas.Tactic.Solver.Grind (973ms)
✔ [1662/1784] Built Aeneas.Tactic.Simp.RingEqNF.Tactic (3.1s)
✔ [1663/1784] Built Aeneas.Tactic.Misc (1.7s)
✔ [1665/1825] Built Aeneas.Data.Range.DivRange (3.5s)
✔ [1666/1825] Built Aeneas.Tactic.Simproc.ReduceZMod (3.5s)
✔ [1667/1825] Built Aeneas.Tactic.Simproc.ReduceFin.ReduceFin (2.4s)
✔ [1668/1825] Built Aeneas.Tactic.Step.InferPost (3.1s)
✔ [1669/1825] Built Aeneas.Data.Range.MulRange (3.2s)
✔ [1670/1825] Built Aeneas.Tactic.Solver.Grind.Tests (3.3s)
✔ [1671/1825] Built AeneasMeta.Split (3.9s)
✔ [1672/1825] Built Aeneas.Tactic.Simproc.ReduceFin (1.7s)
✔ [1673/1825] Built Aeneas.Tactic.Simp.RingEqNF.Tests (3.1s)
✔ [1674/1825] Built Mathlib.RingTheory.Ideal.Operations (5.0s)
✔ [1675/1825] Built Aeneas.Tactic.Simp.RingEqNF (1.7s)
✔ [1676/1825] Built Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (1.6s)
✔ [1677/1825] Built Aeneas.Tactic.Solver.ScalarTac.Tests (6.0s)
✔ [1678/1825] Built Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain (1.8s)
✔ [1679/1825] Built Mathlib.RingTheory.Ideal.Maps (3.6s)
✔ [1680/1825] Built Mathlib.RingTheory.Ideal.Prod (1.4s)
✔ [1681/1825] Built Mathlib.RingTheory.PrincipalIdealDomain (1.6s)
✔ [1682/1825] Built Mathlib.RingTheory.Int.Basic (1.3s)
✔ [1683/1825] Built Aeneas.Tactic.Solver.Arith.Lemmas (2.3s)
✔ [1684/1825] Built Aeneas.Tactic.Solver.Arith (2.2s)
✔ [1685/1825] Built Aeneas.Tactic.Solver.ScalarTac (2.3s)
✔ [1686/1825] Built Aeneas.Tactic.Conv.Natify.Natify (2.9s)
✔ [1687/1825] Built Aeneas.Tactic.Conv.ZModify.ZModify (2.9s)
✔ [1688/1825] Built Aeneas.Tactic.Conv.Zify (2.8s)
✔ [1689/1825] Built Aeneas.Std.Scalar.Misc (3.8s)
✔ [1690/1825] Built Aeneas.Tactic.Solver.ScalarDecrTac (4.1s)
✔ [1691/1825] Built Aeneas.Tactic.Conv.Natify (3.6s)
✔ [1692/1825] Built Aeneas.Tactic.Step.GrindState (4.3s)
✔ [1693/1825] Built Aeneas.Std.Range (4.4s)
✔ [1694/1825] Built Aeneas.Tactic.Conv.ZModify (4.1s)
✔ [1695/1825] Built Aeneas.Std.Scalar.Casts (5.2s)
✔ [1696/1825] Built Aeneas.Std.Scalar.Bitwise (5.4s)
✔ [1697/1825] Built Aeneas.Data.List.List (7.3s)
✔ [1698/1825] Built Aeneas.Std.Scalar.Ops.Neg (4.2s)
✔ [1699/1825] Built Aeneas.Std.Scalar.Ops.Rem (4.9s)
✔ [1700/1825] Built Aeneas.Std.Scalar.Ops.Sub (4.9s)
✔ [1701/1825] Built Aeneas.Std.Scalar.Ops.Add (4.9s)
✔ [1702/1825] Built Aeneas.Std.Scalar.Ops.Mul (4.9s)
✔ [1703/1825] Built Aeneas.Std.Scalar.Ops.Div (5.0s)
✔ [1704/1825] Built Aeneas.Data.List (4.4s)
✔ [1705/1825] Built Aeneas.Std.Array.Core (4.8s)
✔ [1706/1825] Built Aeneas.Data.Range.SRRange.Lemmas (5.3s)
✔ [1707/1825] Built Aeneas.Std.Scalar.CheckedOps.Rem (4.4s)
✔ [1708/1825] Built Aeneas.Std.Scalar.CheckedOps.Sub (5.1s)
✔ [1709/1825] Built Aeneas.Std.Scalar.CheckedOps.Add (5.1s)
✔ [1710/1825] Built Aeneas.Std.Scalar.CheckedOps.Mul (5.2s)
✔ [1711/1825] Built Aeneas.Std.Scalar.Ops (4.3s)
✔ [1712/1825] Built Aeneas.Std.Scalar.Notations (5.6s)
✔ [1713/1825] Built Aeneas.Std.Scalar.CheckedOps.Div (4.8s)
✔ [1714/1825] Built Aeneas.Data.Array (4.7s)
✔ [1715/1825] Built Aeneas.Std.Array.Array (5.7s)
✔ [1716/1825] Built Aeneas.Data.Range.SRRange (4.4s)
✔ [1717/1825] Built Aeneas.Data.BitVec (6.9s)
✔ [1718/1825] Built Aeneas.Std.Scalar.OverflowingOps.Div (5.1s)
✔ [1719/1825] Built Aeneas.Data.Discriminant (5.1s)
✔ [1720/1825] Built Aeneas.Std.Scalar.OverflowingOps.Mul (5.7s)
✔ [1721/1825] Built Aeneas.Std.Slice (7.9s)
✔ [1722/1825] Built Aeneas.Std.Scalar.Default (4.5s)
✔ [1723/1825] Built Aeneas.Std.Scalar.OverflowingOps.Sub (6.5s)
✔ [1724/1825] Built Aeneas.Std.Scalar.CheckedOps (3.0s)
✔ [1725/1825] Built Aeneas.Std.Core.Fmt (4.0s)
✔ [1726/1825] Built Aeneas.Data.Range (3.4s)
✔ [1727/1825] Built Aeneas.Data.Vector (4.7s)
✔ [1728/1825] Built Aeneas.Std.Scalar.OverflowingOps.Add (8.3s)
✔ [1729/1825] Built Aeneas.Std.Core.Hash (3.4s)
✔ [1730/1825] Built Aeneas.Std.Scalar.CoreConvertNum (4.0s)
✔ [1731/1825] Built Aeneas.Std.Std.Io (3.8s)
✔ [1732/1825] Built Aeneas.Std.Core.Error (4.1s)
✔ [1733/1825] Built Aeneas.Std.Array.ArrayDebug (4.3s)
✔ [1734/1825] Built Aeneas.Std.Scalar.Display (4.0s)
✔ [1735/1825] Built Aeneas.Std.Scalar.Fmt (4.0s)
✔ [1736/1825] Built Aeneas.Std.Core.Iter (5.0s)
✔ [1737/1825] Built Aeneas.Data (3.9s)
✔ [1738/1825] Built Aeneas.Std.Array.ArraySlice (5.0s)
✔ [1739/1825] Built Aeneas.Tactic.Setup (3.6s)
✔ [1740/1825] Built Aeneas.Std.Scalar.OverflowingOps (3.2s)
✔ [1741/1825] Built Aeneas.Std.Core.Discriminant (2.7s)
✔ [1742/1825] Built Aeneas.Std.Std (2.6s)
✔ [1743/1825] Built Aeneas.Std.Array (2.3s)
✔ [1744/1825] Built Aeneas.Std.Scalar (2.2s)
✔ [1745/1825] Built Aeneas.Std.SliceIter (3.4s)
✔ [1746/1825] Built Aeneas.Std.Target (2.5s)
✔ [1747/1825] Built Aeneas.Std.String (2.9s)
✔ [1748/1825] Built Proofs.ChunkLemmas (3.0s)
✔ [1749/1825] Built Aeneas.Std.Alloc.Vec (4.1s)
✔ [1750/1825] Built Aeneas.Std.RangeIter (4.3s)
✔ [1751/1825] Built Aeneas.Std.Core.CoreOption (3.5s)
✔ [1752/1825] Built Aeneas.Std.Core.FmtWithSlice (3.5s)
✔ [1753/1825] Built Aeneas.Std.StringIter (3.9s)
✔ [1754/1825] Built Proofs.ComputeChunks (3.6s)
✔ [1755/1825] Built Proofs.FourChunks (3.7s)
✔ [1756/1825] Built Aeneas.Std.Alloc.Slice (3.1s)
✔ [1757/1825] Built Aeneas.Std.Alloc.Vec.IntoIter (3.2s)
✔ [1758/1825] Built Aeneas.Std.Core (2.2s)
✔ [1759/1825] Built Aeneas.Std.Alloc (1.9s)
✔ [1760/1825] Built Aeneas.Tactic.Conv.Bvify.Bvify (9.5s)
✔ [1761/1825] Built Aeneas.Std (1.0s)
✔ [1762/1825] Built Aeneas.Tactic.Conv.Bvify.Lemmas (2.8s)
✔ [1763/1825] Built Aeneas.Tactic.Conv.Bvify.Tests (2.2s)
✔ [1764/1825] Built Aeneas.Do.Delab (2.7s)
✔ [1765/1825] Built Aeneas.Tactic.Conv.Bvify (2.1s)
✔ [1766/1825] Built Aeneas.Tactic.Simp.SimpLists.Tests (3.8s)
✔ [1767/1825] Built Aeneas.Command.Decompose.TestsRec (3.3s)
✔ [1768/1825] Built Aeneas.Tactic.Conv (2.0s)
✔ [1769/1825] Built Aeneas.Tactic.Simp.SimpLists (2.5s)
✔ [1770/1825] Built Aeneas.Do.Tests (3.9s)
✔ [1771/1825] Built Aeneas.Tactic.Simp.SimpListsScalar (2.3s)
✔ [1772/1825] Built Aeneas.Command.Decompose.Tests (5.0s)
✔ [1773/1825] Built Aeneas.Do (2.6s)
✔ [1774/1825] Built Aeneas.Tactic.Simp (1.0s)
✔ [1775/1825] Built Aeneas.Command.Decompose.TestsBig (11s)
✔ [1776/1825] Built Aeneas.Command (1.2s)
✔ [1777/1825] Built Aeneas.Tactic.Step.Step (7.3s)
✔ [1778/1825] Built Aeneas.Tactic.Solver.BvTac.BvTac (15s)
✔ [1779/1825] Built Aeneas.Tactic.Step.StepArraySpec (2.9s)
✔ [1780/1825] Built Aeneas.Tactic.Step.Tests.DspecInduction (2.8s)
✔ [1781/1825] Built Aeneas.Tactic.Simproc.BvSimprocs (2.9s)
✔ [1782/1825] Built Aeneas.Tactic.Step.StepStar (6.6s)
✔ [1783/1825] Built Aeneas.Tactic.Simproc (2.5s)
✔ [1784/1825] Built Aeneas.Tactic.Step.Deprecated (2.8s)
✔ [1785/1825] Built Aeneas.Tactic.Solver.BvTac.Lemmas (7.7s)
✔ [1786/1825] Built Aeneas.Tactic.Step (2.1s)
✔ [1787/1825] Built Aeneas.Tactic.Solver.BvTac (2.4s)
✔ [1788/1825] Built Aeneas.Tactic.Solver.BvTac.Tests (10s)
✔ [1789/1825] Built Aeneas.Tactic.Step.Tests.TupleDestruct (4.6s)
✔ [1790/1825] Built Aeneas.Tactic.Step.Tests.MaxRecDepthMetavar (4.8s)
✔ [1791/1825] Built Aeneas.Tactic.Step.Tests.UncurryBind (4.8s)
✔ [1792/1825] Built Aeneas.Tactic.Step.Tests.MvcgenSpec (5.1s)
✔ [1793/1825] Built Aeneas.Tactic.Step.Tests.SpecParameters (4.4s)
✔ [1794/1825] Built Aeneas.Tactic.Step.Tests.HigherOrderOption (5.5s)
✔ [1795/1825] Built Aeneas.Tactic.Step.Tests.IntroOutputsRecursion (5.7s)
✔ [1796/1825] Built Aeneas.Tactic.Step.Tests.Coin (5.8s)
✔ [1797/1825] Built Aeneas.Tactic.Step.Tests.IntroOutputs (7.6s)
✔ [1798/1825] Built Aeneas.Tactic.Step.Tests.HigherOrder (6.6s)
✔ [1799/1825] Built Aeneas.Tactic.Solver (3.4s)
✔ [1800/1825] Built Aeneas.Tactic.Step.Tests.ParserErrors (3.9s)
✔ [1801/1825] Built Aeneas.Tactic.Step.Tests.DischargeTactic (3.9s)
✔ [1802/1825] Built Aeneas.Tactic.Step.Tests.Triple (4.1s)
✔ [1803/1825] Built Aeneas.Tactic.Step.Tests (1.9s)
✔ [1804/1825] Built Aeneas.Tactic.Tests (271ms)
✔ [1805/1825] Built Aeneas.Tactic (2.0s)
✔ [1806/1825] Built Aeneas (2.1s)
✔ [1807/1825] Built Adler2 (2.3s)
✔ [1808/1825] Built Proofs.LoopBridge (2.7s)
✔ [1809/1825] Built Proofs.Smoke (2.8s)
✔ [1810/1825] Built Proofs.AlgoHelpers (3.0s)
✔ [1811/1825] Built Proofs.Codec (3.0s)
✔ [1812/1825] Built Proofs.Spec (3.1s)
✔ [1813/1825] Built Proofs.AlgoOps (4.2s)
✔ [1814/1825] Built Proofs.LaneMath (2.4s)
✔ [1815/1825] Built Proofs.Loop4 (2.6s)
✔ [1816/1825] Built Proofs.LaneLoop (2.4s)
✔ [1817/1825] Built Proofs.RawBridge (2.2s)
✔ [1818/1825] Built Proofs.SumLoops (2.4s)
✔ [1819/1825] Built Proofs.GroupBridge (2.1s)
✔ [1820/1825] Built Proofs.OuterLoop (2.2s)
✔ [1821/1825] Built Proofs.FinalCombine (4.5s)
✔ [1822/1825] Built Proofs.SplitPrelude (2.2s)
✔ [1823/1825] Built Proofs.FinalTail (2.1s)
✔ [1824/1825] Built Proofs.Compute (2.3s)
✔ [1825/1825] Built Proofs.PublicUpdate (2.0s)
Build completed successfully (1825 jobs).

$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"data","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]}],"conclusion":"∃ out, adler2.adler32_slice data = Aeneas.Std.Result.ok out ∧ ↑out = adler2.encode (adler2.run (1, 0) ↑data)","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"adler2.adler32_slice","text":"adler2.adler32_slice"},{"text":" "},{"text":"data"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"↑"},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"adler2.encode","text":"adler2.encode"},{"text":" "},{"text":"("},{"ref":"adler2.run","text":"adler2.run"},{"text":" "},{"ref":"Prod.mk","text":"("},{"text":"1"},{"ref":"Prod.mk","text":", "},{"text":"0"},{"ref":"Prod.mk","text":")"},{"text":" "},{"text":"↑"},{"text":"data"},{"text":")"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U32","source":{"first_line":671,"last_line":671}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Adler2","name":"adler2.adler32_slice","source":{"first_line":396,"last_line":402}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.U32","source":{"first_line":35,"last_line":35}},{"module":"Proofs.Spec","name":"adler2.encode","source":{"first_line":24,"last_line":24}},{"module":"Proofs.Spec","name":"adler2.run","source":{"first_line":19,"last_line":20}},{"module":"Init.Prelude","name":"Prod.mk","source":{"first_line":614,"last_line":614}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice.val","source":{"first_line":21,"last_line":22}}],"definitions_truncated":false,"first_line":30,"last_line":43,"module":"Proofs.PublicUpdate","program":null,"program_head":null,"statement":"∀ (data : Aeneas.Std.Slice.{0} Aeneas.Std.U8),\n  @Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32) (adler2.adler32_slice data)\n        (@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))\n      (@Eq.{1} Nat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out)\n        (adler2.encode\n          (adler2.run\n            (@Prod.mk.{0, 0} Nat Nat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n              (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))\n            (@Aeneas.Std.Slice.val.{0} Aeneas.Std.U8 data))))","theorem":"adler2.adler32_slice_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"s","type":"adler2.Adler32","type_segments":[{"ref":"adler2.Adler32","text":"adler2.Adler32"}]}],"conclusion":"∃ out, s.checksum = Aeneas.Std.Result.ok out ∧ ↑out = ↑s.b * 65536 + ↑s.a","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"text":"s"},{"text":"."},{"ref":"adler2.Adler32.checksum","text":"checksum"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"↑"},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"↑"},{"text":"s"},{"text":"."},{"ref":"adler2.Adler32.b","text":"b"},{"ref":"HMul.hMul","text":" * "},{"text":"65536"},{"ref":"HAdd.hAdd","text":" + "},{"text":"↑"},{"text":"s"},{"text":"."},{"ref":"adler2.Adler32.a","text":"a"}],"definitions":[{"module":"Adler2","name":"adler2.Adler32","source":{"first_line":23,"last_line":28}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U32","source":{"first_line":671,"last_line":671}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Adler2","name":"adler2.Adler32.checksum","source":{"first_line":380,"last_line":387}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.U32","source":{"first_line":35,"last_line":35}},{"module":"Init.Prelude","name":"HAdd.hAdd","source":{"first_line":1481,"last_line":1481}},{"module":"Init.Prelude","name":"instHAdd","source":{"first_line":1784,"last_line":1786}},{"module":"Init.Prelude","name":"instAddNat","source":{"first_line":1892,"last_line":1893}},{"module":"Init.Prelude","name":"HMul.hMul","source":{"first_line":1500,"last_line":1500}},{"module":"Init.Prelude","name":"instHMul","source":{"first_line":1792,"last_line":1794}},{"module":"Init.Prelude","name":"instMulNat","source":{"first_line":1913,"last_line":1914}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.U16","source":{"first_line":34,"last_line":34}},{"module":"Adler2","name":"adler2.Adler32.b","source":{"first_line":28,"last_line":28}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Adler2","name":"adler2.Adler32.a","source":{"first_line":27,"last_line":27}}],"definitions_truncated":false,"first_line":10,"last_line":30,"module":"Proofs.Codec","program":null,"program_head":null,"statement":"∀ (s : adler2.Adler32),\n  @Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32) (adler2.Adler32.checksum s)\n        (@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))\n      (@Eq.{1} Nat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out)\n        (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)\n          (@HMul.hMul.{0, 0, 0} Nat Nat Nat (@instHMul.{0} Nat instMulNat)\n            (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 (adler2.Adler32.b s))\n            (@OfNat.ofNat.{0} Nat (nat_lit 65536) (instOfNatNat (nat_lit 65536))))\n          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 (adler2.Adler32.a s))))","theorem":"adler2.checksum_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"sum","type":"Aeneas.Std.U32","type_segments":[{"ref":"Aeneas.Std.U32","text":"Aeneas.Std.U32"}]}],"conclusion":"∃ out, adler2.Adler32.from_checksum sum = Aeneas.Std.Result.ok out ∧ ↑out.a = ↑sum % 65536 ∧ ↑out.b = ↑sum / 65536","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"adler2.Adler32.from_checksum","text":"adler2.Adler32.from_checksum"},{"text":" "},{"text":"sum"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"↑"},{"text":"out"},{"text":"."},{"ref":"adler2.Adler32.a","text":"a"},{"ref":"Eq","text":" = "},{"text":"↑"},{"text":"sum"},{"ref":"HMod.hMod","text":" % "},{"text":"65536"},{"ref":"And","text":" ∧ "},{"text":"↑"},{"text":"out"},{"text":"."},{"ref":"adler2.Adler32.b","text":"b"},{"ref":"Eq","text":" = "},{"text":"↑"},{"text":"sum"},{"ref":"HDiv.hDiv","text":" / "},{"text":"65536"}],"definitions":[{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U32","source":{"first_line":671,"last_line":671}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Adler2","name":"adler2.Adler32","source":{"first_line":23,"last_line":28}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Adler2","name":"adler2.Adler32.from_checksum","source":{"first_line":371,"last_line":378}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.U16","source":{"first_line":34,"last_line":34}},{"module":"Adler2","name":"adler2.Adler32.a","source":{"first_line":27,"last_line":27}},{"module":"Init.Prelude","name":"HMod.hMod","source":{"first_line":1529,"last_line":1529}},{"module":"Init.Prelude","name":"instHMod","source":{"first_line":1800,"last_line":1802}},{"module":"Init.Prelude","name":"Nat.instMod","source":{"first_line":2408,"last_line":2408}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.U32","source":{"first_line":35,"last_line":35}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Adler2","name":"adler2.Adler32.b","source":{"first_line":28,"last_line":28}},{"module":"Init.Prelude","name":"HDiv.hDiv","source":{"first_line":1518,"last_line":1518}},{"module":"Init.Prelude","name":"instHDiv","source":{"first_line":1796,"last_line":1798}},{"module":"Init.Prelude","name":"Nat.instDiv","source":{"first_line":2320,"last_line":2320}}],"definitions_truncated":false,"first_line":32,"last_line":47,"module":"Proofs.Codec","program":null,"program_head":null,"statement":"∀ (sum : Aeneas.Std.U32),\n  @Exists.{1} adler2.Adler32 fun (out : adler2.Adler32) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} adler2.Adler32) (adler2.Adler32.from_checksum sum)\n        (@Aeneas.Std.Result.ok.{0} adler2.Adler32 out))\n      (And\n        (@Eq.{1} Nat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 (adler2.Adler32.a out))\n          (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod)\n            (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 sum)\n            (@OfNat.ofNat.{0} Nat (nat_lit 65536) (instOfNatNat (nat_lit 65536)))))\n        (@Eq.{1} Nat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 (adler2.Adler32.b out))\n          (@HDiv.hDiv.{0, 0, 0} Nat Nat Nat (@instHDiv.{0} Nat Nat.instDiv)\n            (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 sum)\n            (@OfNat.ofNat.{0} Nat (nat_lit 65536) (instOfNatNat (nat_lit 65536))))))","theorem":"adler2.from_checksum_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[],"conclusion":"adler2.Adler32.new = Aeneas.Std.Result.ok { a := 1#u16, b := 0#u16 }","conclusion_segments":[{"ref":"adler2.Adler32.new","text":"adler2.Adler32.new"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"ref":"adler2.Adler32.mk","text":"{ "},{"text":"a"},{"ref":"adler2.Adler32.mk","text":" := "},{"text":"1"},{"ref":"Aeneas.Std.U16.ofNat","text":"#u16"},{"ref":"adler2.Adler32.mk","text":", "},{"text":"b"},{"ref":"adler2.Adler32.mk","text":" := "},{"text":"0"},{"ref":"Aeneas.Std.U16.ofNat","text":"#u16"},{"ref":"adler2.Adler32.mk","text":" }"}],"definitions":[{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Adler2","name":"adler2.Adler32","source":{"first_line":23,"last_line":28}},{"module":"Adler2","name":"adler2.Adler32.new","source":{"first_line":365,"last_line":369}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Adler2","name":"adler2.Adler32.mk","source":{"first_line":26,"last_line":26}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U16.ofNat","source":{"first_line":705,"last_line":705}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Proofs.Smoke","name":"adler2.new_spec._proof_1","source":null},{"module":"Proofs.Smoke","name":"adler2.new_spec._proof_2","source":null}],"definitions_truncated":false,"first_line":10,"last_line":13,"module":"Proofs.Smoke","program":null,"program_head":null,"statement":"@Eq.{1} (Aeneas.Std.Result.{0} adler2.Adler32) adler2.Adler32.new\n  (@Aeneas.Std.Result.ok.{0} adler2.Adler32\n    (adler2.Adler32.mk\n      (Aeneas.Std.U16.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) adler2.new_spec._proof_1)\n      (Aeneas.Std.U16.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) adler2.new_spec._proof_2)))","theorem":"adler2.new_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"s","type":"adler2.Adler32","type_segments":[{"ref":"adler2.Adler32","text":"adler2.Adler32"}]},{"binder":"explicit","kind":"variable","name":"bytes","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]}],"conclusion":"∃ out, s.write_slice bytes = Aeneas.Std.Result.ok out ∧ adler2.observe out = adler2.run (adler2.observe s) ↑bytes","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"text":"s"},{"text":"."},{"ref":"adler2.Adler32.write_slice","text":"write_slice"},{"text":" "},{"text":"bytes"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"ref":"adler2.observe","text":"adler2.observe"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"adler2.run","text":"adler2.run"},{"text":" "},{"text":"("},{"ref":"adler2.observe","text":"adler2.observe"},{"text":" "},{"text":"s"},{"text":")"},{"text":" "},{"text":"↑"},{"text":"bytes"}],"definitions":[{"module":"Adler2","name":"adler2.Adler32","source":{"first_line":23,"last_line":28}},{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Adler2","name":"adler2.Adler32.write_slice","source":{"first_line":389,"last_line":394}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"Prod","source":{"first_line":603,"last_line":618}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Proofs.Spec","name":"adler2.observe","source":{"first_line":22,"last_line":22}},{"module":"Proofs.Spec","name":"adler2.run","source":{"first_line":19,"last_line":20}},{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice.val","source":{"first_line":21,"last_line":22}}],"definitions_truncated":false,"first_line":23,"last_line":28,"module":"Proofs.PublicUpdate","program":null,"program_head":null,"statement":"∀ (s : adler2.Adler32) (bytes : Aeneas.Std.Slice.{0} Aeneas.Std.U8),\n  @Exists.{1} adler2.Adler32 fun (out : adler2.Adler32) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} adler2.Adler32) (adler2.Adler32.write_slice s bytes)\n        (@Aeneas.Std.Result.ok.{0} adler2.Adler32 out))\n      (@Eq.{1} (Prod.{0, 0} Nat Nat) (adler2.observe out)\n        (adler2.run (adler2.observe s) (@Aeneas.Std.Slice.val.{0} Aeneas.Std.U8 bytes)))","theorem":"adler2.write_slice_spec","translation_rerun":false,"version":1}

=== stderr ===
info: aeneas: materializing new dependency
info: aeneas: fetching revision 'be86ab0f1989d04944292b345b24c435be3ad10a' from https://github.com/AeneasVerif/aeneas
info: aeneas: checking out revision 'be86ab0f1989d04944292b345b24c435be3ad10a'
info: mathlib: materializing new dependency
info: mathlib: fetching revision '56a005855ea17e0b0958f73ec801ae140b0a1679' from https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '56a005855ea17e0b0958f73ec801ae140b0a1679'
info: plausible: materializing new dependency
info: plausible: fetching revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24' from https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24'
info: LeanSearchClient: materializing new dependency
info: LeanSearchClient: fetching revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372' from https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372'
info: importGraph: materializing new dependency
info: importGraph: fetching revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93' from https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93'
info: proofwidgets: materializing new dependency
info: proofwidgets: fetching revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04' from https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04'
info: aesop: materializing new dependency
info: aesop: fetching revision '4a174c490d8707121c4a9290800489f105d85e07' from https://github.com/leanprover-community/aesop
info: aesop: checking out revision '4a174c490d8707121c4a9290800489f105d85e07'
info: Qq: materializing new dependency
info: Qq: fetching revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8' from https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8'
info: batteries: materializing new dependency
info: batteries: fetching revision '66e469188fe07963e5cf666c7d4433f45b8131c5' from https://github.com/leanprover-community/batteries
info: batteries: checking out revision '66e469188fe07963e5cf666c7d4433f45b8131c5'
info: Cli: materializing new dependency
info: Cli: fetching revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8' from https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8'

Environment

Extraction target: aarch64-apple-darwin (macOS arm64), default Cargo features.
Lean: 4.35.0.
Aeneas: be86ab0f1989d04944292b345b24c435be3ad10a.
Charon: 08d7c9d50144bd84848212c24701253585e90d1f.
Extraction Rust: nightly-2026-09-17.
Native-test Rust: 1.91.1.

The local verification toolchain pins are recorded in verification/toolchain.json.

What is trusted

Trusted boundaries

Translation: the pinned Charon/Aeneas Rust-to-LLBC-to-Lean translation.
Library models: the correspondence between Aeneas standard-library models
and Rust, including slice and iterator semantics.
Proof checking: the Lean kernel. The transitive theorem audit permits only
propext, Classical.choice, and Quot.sound.

The audit rejects sorryAx, custom axioms, and native-decision axioms. The
algorithm contracts do not assume correctness of the optimized compute body.

Technical limitations

Scope exclusions

This report concerns the computation core under default Cargo features for the
macOS arm64 extraction target. It does not establish whole-crate correctness.
The following remain outside the formal scope:

Generic BufRead I/O and its error behavior.
Derived traits and Hasher laws.
no_std configurations and alternative targets.

Native no_std tests are separate finite observations, not formal proofs for
that configuration.

Tool limitations

Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Dependencies (1)

CrateReports

rustc-std-workspace-core ^1.0.0 · optional—

Comments (0)

No comments.