Installation issue

[DanielHL]

I tried to follow the instructions in the readme, but when I run lake build and then restart the Lean file, I get an error. I seem may files successfully built in the infoviewer, but two builds fail:

- Auto.Lib.AbstractMVars
- Duper.Util.AbstractMVars```

The more specific error trace is:

error: Duper/Util/AbstractMVars.lean:139:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Duper/Util/AbstractMVars.lean:139:7: fields missing: 'mvars'
error: Duper/Util/AbstractMVars.lean:152:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Duper/Util/AbstractMVars.lean:152:7: fields missing: 'mvars'
error: Duper/Util/AbstractMVars.lean:184:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Duper/Util/AbstractMVars.lean:184:7: fields missing: 'mvars'
error: Lean exited with code 1

and

error: Auto/Lib/AbstractMVars.lean:135:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Auto/Lib/AbstractMVars.lean:135:7: fields missing: 'mvars'
error: Auto/Lib/AbstractMVars.lean:148:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Auto/Lib/AbstractMVars.lean:148:7: fields missing: 'mvars'
error: Auto/Lib/AbstractMVars.lean:183:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Auto/Lib/AbstractMVars.lean:183:7: fields missing: 'mvars'
error: Lean exited with code 1

I encountered the same error on two Mac notebooks -- one with Intel chips, and one with Apple chips. On the apple chip machine, zipperposition 2.1 is installed.

[hanwenzhu]

@DanielHL This is because LeanHammer @ main is currently at v4.20.0, while you are probably building it on a newer version like v4.21.0-rc3. We are currently upgrading to v4.21.0-rc3. To address your issue, you can either fix your Lean versions in your lakefile.toml and lean-toolchain at v4.20.0, or bump LeanHammer to the branch temp-v4.21.0-rc3 by adding in your lakefile.toml (where temp- means we are currently still working on this):

[[require]]
name = "Hammer"
git = "https://github.com/JOSHCLUNE/LeanHammer"
rev = "temp-v4.21.0-rc3"