no such file error

Stream: mathlib4

[Bolton Bailey]

I am currently experiencing the following error on master:

`/Users/boltonbailey/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/lake setup-file /Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/Mathlib/Algebra/Algebra/Hom.lean Init Mathlib.Algebra.Algebra.Basic Mathlib.Algebra.BigOperators.Finsupp --no-build` failed:

stderr:
warning: std: repository './.lake/packages/std' has local changes
warning: proofwidgets: repository './.lake/packages/proofwidgets' has local changes
error: 'Mathlib.Algebra.Algebra.Basic' ▸ 'Mathlib.Algebra.CharZero.Lemmas' ▸ 'Mathlib.Algebra.Function.Support' ▸ 'Mathlib.Algebra.Group.Prod' ▸ 'Mathlib.Algebra.Group.Opposite' ▸ 'Mathlib.Algebra.Group.Commute.Defs' ▸ 'Mathlib.Algebra.Group.Semiconj.Defs' ▸ 'Mathlib.Algebra.Group.Defs' ▸ 'Mathlib.Tactic.TypeStar' ▸ 'Std' ▸ 'Std.Classes.SatisfiesM': no such file or directory (error code: 2)
  file: ./.lake/packages/std/././Std/Classes/SatisfiesM.lean

How do I troubleshoot this?

[Ruben Van de Velde]

I would attempt to remove the entire .lake folder first (or move it elsewhere, if you're feeling very risk-averse)

[Bolton Bailey]

This seems to be working, thanks