build issues: A dataset of proofs for 20 IMO problems ...

Stream: Machine Learning for Theorem Proving

[Eric Wieser]

Can you add a lake-manifest.json to your repo? Without it, it is impossible for a human to check if your proofs actually work!

[Roozbeh Yousefzadeh]

Thanks for the suggestion -- I added the file. The proofs compile with no error using Lean 4.17.0 and also Lean 4.17.0-rc1.

[Eric Wieser]

You should also add the lean-toolchain and lakefiles.lean files

[Eric Wieser]

(the manifest was important because it specifies the mathlib version, not just the Lean version)

[Roozbeh Yousefzadeh]

Makes sense. I added both lean-toolchain and lakefile.lean.

[Eric Wieser]

The lakefile.lean looks like you copied it from mathlib, which means it is not going to work.

[Eric Wieser]

Similarly, in https://github.com/roozbeh-yz/IMO-Steps/commit/a0b8f80d4e6e4aa9f861e63614dce54bb8625c55 you overwrote a good lake-manifest.json with a bad one

[Roozbeh Yousefzadeh]

Thank you, Eric. I have now replaced them with the correct files.

[Eric Wieser]

If I attempt to build your code, I get

Dependency Mathlib uses a different lean-toolchain
  Project uses leanprover/lean4:v4.17.0
  Mathlib uses leanprover/lean4:v4.17.0-rc1

Probably the advice here can be used to fix this, though then I get

$ lake build
error: no such file or directory (error code: 2)
  file: ././././ImoSteps.lean

[Roozbeh Yousefzadeh]

I added the ImoSteps.lean , though I'm not sure why there is such a file. I also implemented the advice regarding the upgrade to v4.17.0. Please let me know if there are any other issues.

[Eric Wieser]

Roozbeh Yousefzadeh said:

added the ImoSteps.lean , though I'm not sure why there is such a file

This is because you promised it existed in your lakefile.toml.

If you switch to a lakefile.lean, then you can write

@[default_target]
lean_lib imo_proofs where
  globs := #[.submodules `imo_proofs]

and delete ImoSteps.lean.

[Eric Wieser]

@Mac Malone, can you confirm there is no way to use the submodules spelling from a toml file?

[Notification Bot]

13 messages were moved here from #Machine Learning for Theorem Proving > A dataset of proofs for 20 IMO problems and extracted lemmas by Eric Wieser.

[Mac Malone]

@Eric Wieser The TOMl syntax is globs = ["imo_proofs.+"].

This shorthand can also be used in Lean as well: globs := #[`imo_proofs.+].

[Damiano Testa]

imo_proofs.+ is valid syntax? Wow!

[Patrick Massot]

Where is this documented?

[Kim Morrison]

It seems like it should be on https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#lake-config, but is not. Would someone like to open an issue against the language reference for globs?

[Eric Wieser]

Is `.+ legal for "all files"?

[Mac Malone]

@Eric Wieser No.

[Roozbeh Yousefzadeh]

Thank you everyone for your comments and advice.

[Eric Wieser]

I think the build is still broken ; you can test by running lake build inside your project