Probability directory file doesn't exist

Stream: new members

[Tomer]

import Mathlib
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.Sym.Card
import Mathlib.Probability.Distributions.SetBernoulli--Trying to define a renadom graph

open Finset
open MeasureTheory Measure ProbabilityTheory unitInterval
open SimpleGraph
--open Classical Mathlib.Combinatorics

namespace Tringles
variable {n : ℕ}
variable {V : Type*} {p : I}
instance : MeasurableSpace (SimpleGraph V) := .comap Adj inferInstance
#check setBernoulli
noncomputable def binomialRandom : Measure (SimpleGraph V) :=
  setBer(Sym2.diagSetᶜ, p).comap edgeSet

end Tringles

This is the code I am trying to run, and the error I get is this

/home/me/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lake setup-file /home/me/Leanproject/this/This.lean - --no-build --no-cache failed:

stderr:
✖ [7744/7746] Running Mathlib.Probability.Distributions.SetBernoulli
error: no such file or directory (error code: 2)
file: /home/me/Leanproject/this/.lake/packages/mathlib/Mathlib/Probability/Distributions/SetBernoulli.lean
✖ [7745/7746] Running setup-file /home/me/Leanproject/this/This.lean
trace: file identified as module: This
error: This.lean: bad import 'Mathlib.Probability.Distributions.SetBernoulli'
Some required targets logged failures:

• Mathlib.Probability.Distributions.SetBernoulli
• setup-file /home/me/Leanproject/this/This.lean
  Failed to build module dependencies.
  

Is there is a way to update the folders or re-download the library?

[Michael Rothgang]

That file exists in the most recent mathlib --- are you sure you're using a sufficiently new version of mathlib?

[Michael Rothgang]

That aside, import Mathlib should suffice --- there's no need to import individual modules in addition to that.

[Damiano Testa]

It seems to have been introduced in #31908.

[Tomer]

Solved, it was not updated for some reason