Cannot get Lean4 and Mathlib working in Emacs

Stream: general

[Sophia C]

So, I'm trying to learn lean. I've got a basic testing repo set up via by running lake +leanprover-community/mathlib4:lean-toolchain new Testing math I have also installed the Lean4-mode for Emacs following the directions in the corresponding github repo.

I then created a file called Primes.lean in the Test folder (made by lake). It has a single line in it:

import Mathlib.Data.Nat.Prime

The lean goals window now shows this error:

1:0:
`/home/sophia/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/lake setup-file /home/sophia/lean/MathInLean/MathInLean/Primes.lean Init Mathlib.Data.Nat.Prime` failed:

stderr:
✖ [1/3] Running imports (/home/sophia/lean/MathInLean/MathInLean/Primes.lean)
error: /home/sophia/lean/MathInLean/MathInLean/Primes.lean: bad import 'Mathlib.Data.Nat.Prime'
✖ [3/3] Running Mathlib.Data.Nat.Prime
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Prime.lean
Some builds logged failures:
- imports (/home/sophia/lean/MathInLean/MathInLean/Primes.lean)
- Mathlib.Data.Nat.Prime
error: build failed

[Sophia C]

The project structure looks like this:

├── lakefile.lean
├── lake-manifest.json
├── lean-toolchain
├── MathInLean
│   ├── Basic.lean
│   └── Primes.lean
├── MathInLean.lean
└── README.md

The only thing I've changed from the initial template that was generated is adding the Primes.lean file.

[Henrik Böving]

It appears to me that this changed to Mathlib.Data.Nat.Prime.Basic

[Sophia C]

That has in fact resolved my issues! Thanks!

[Henrik Böving]

We should probably change that template? Who controls this? Lake? CC @Mac Malone

[Mac Malone]

@Henrik Böving Lake does control the template. I am confused as to what change you are suggesting, though? The error here just seems like a mispelled import -- unless I am missing something?

[Henrik Böving]

Oh, it sounded to me like the import was auto generated by the template

[Henrik Böving]

if that's not the case we can't do anything of course

[Sophia C]

@Henrik Böving No. The default template includes everything except the file Primes.lean, which I added myself.
My issue is that I'm trying to follow along with Mathematics In Lean, and I found this file, which uses an incorrect import: https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

[Yaël Dillies]

Yeah, the file was renamed very recently. I'm sure @Patrick Massot wouldn't mind if you opened a PR/issue to the MIL repo

[Sophia C]

I don't seem to be able to submit github issues to that particular github repo, and I don't really want to go through all the effort required to make a PR right now.

[Patrick Massot]

I will soon update MIL to a more recent version of Lean and Mathlib so I am bound to hit this issue.

[Yaël Dillies]

Let's wait for Patrick :racecar:

[Patrick Massot]

Yaël, I think encouraging beginners to open bumping PRs to MIL is not super wise. Of course PRs fixing typos or clarifying explanations are good for beginners.

[Patrick Massot]

More generally there is a very common theme where very early beginners see something in MIL or another book and try to copy-paste it into a new project (or live.lean-lang.org) and I very confused to see it does not work because of some version mismatch. I don’t know what to do about that. People are used to much more stable environments when learning programming languages or general software. They simply don’t expect that kind of issue.