latest mathlib does not build?

Stream: mathlib4

[Jared green]

i was trying to update everything on my mac, and now mathlib doesnt build. my entire project is at https://github.com/jaredgreen2/polySat

[Kim Morrison]

For problems like this, you will need to tell us:

• exactly what sequence of commands you are typing to produce the error
• what the error is

[Kim Morrison]

Without that, you are asking someone to clone your project and discover this themselves.

[Jared green]

import Init.PropLemmas
import Std.Data.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas

[Jared green]

thats from basic2. infoview says it fails, though cant copy the error info to zulip because its way too long. its on mathlib revision 13286789733bdf68f17116bf21c39c0646cd76c5, lean 4.9.0-rc3.

[Jared green]

the infoview shows errors inStd.Util.ExtendedBinder, Std.Tactic.OpenPrivate, Std.Data.Option.Init.Lemmas, Std.Tactic.HaveI, Std.Lean.Command, Std.Tactic.ByCases, Std.Lean.Position, Std.Lean.Syntax, Std.Lean.Parser, Std.Lean.LocalContext, Std.Lean.Tactic, Std.Tactic.Lint.Basic, Std.Data.Array.Init.Basic, Std.Data.Fin.Init.Lemmas, Std.Data.List.Init.Basic, Std.Classes.Dvd, Std.Data.Ord, Std.Lean.PersistentHashMap, Std.Classes.BEq, Std.Lean.Delaborator, Std.Lean.Elab.Tactic, Std.Tactic.GuardExpr, Std.Tactic.RCases, and Std.CodeAction.Attr .

[Shreyas Srinivas]

Two things :

1. How did you update mathlib. What commands did you run.
2. Did you try the restart file button

[Jared green]

just lake update, and then i pushed the restart file button.

[Jared green]

i just updated again and the same errors occur.

[Ruben Van de Velde]

Have you tried quitting vs code and restarting?

[Jared green]

thats what i did.

[Jared green]

i am committing with a file containing the error info.

[Mauricio Collares]

You depend on version 0.0.8 of Duper, which uses Lean v4.6.0-rc1. It's likely that it depends on an older version of Std.

[Mauricio Collares]

Updating to version 0.0.13 (which uses Lean v4.8.0-rc2) will solve some of the issues, but maybe not all

[Jared green]

how do i update duper?

[Mauricio Collares]

Edit your lakefile.lean and either remove the @ "0.0.8" pin or change it to 0.0.13, then run lake update again

[Jared green]

now i get unknown package Std

[Jared green]

solved: i comment out the line with std

[Shreyas Srinivas]

You need to change it to batteries.

[Shreyas Srinivas]

In the last 1.5 months Std was renamed to batteries.

[Shreyas Srinivas]

Oh wait, are you talking about duper's dependency?

[Mauricio Collares]

It's a file in the repo, basic2.lean. But depending on what's being used, Batteries might not be needed. Some of Std.Data.List was upstreamed to Init.Data.List.

[Mauricio Collares]

(If that's not the case, follow the instructions at https://github.com/leanprover-community/batteries to add Batteries to your lakefile.lean)