no such file or directory (error code: 2)

Stream: mathlib4

[Kajani Kaunda]

Hello. I am getting the following error message. How do I fix it?

c:\Users\KAJANI.DESKTOP-TF4BQ6L\.elan\toolchains\leanprover--lean4---v4.10.0-rc2\bin\lake.exe setup-file C:/DATA/AIR/LEAN/test/PRIME-INFINITY.lean Init Test.Basic Mathlib.Data.Nat.Prime failed:

stderr:
✖ [1/4] Running Mathlib.Data.Nat.Prime
error: no such file or directory (error code: 2)
file: .\.\.lake/packages\mathlib\.\.\Mathlib\Data\Nat\Prime.lean

[Kevin Buzzard]

docs#Nat.Prime

[Kajani Kaunda]

Kevin Buzzard said:

docs#Nat.Prime

Thank you Sir. Let me read that link.

[Kevin Buzzard]

Indeed there is no module called Mathlib.Data.Nat.Prime. Try changing it to Mathlib.Data.Nat.Prime.Basic

[Kajani Kaunda]

Kevin Buzzard said:

Indeed there is no module called Mathlib.Data.Nat.Prime. Try changing it to Mathlib.Data.Nat.Prime.Basic

Ok, Let me try that now ...

[Kevin Buzzard]

Sorry, that first comment was for me not you, I'm on mobile so needed a link to the module to see what it was called (it says at the top)

[Kajani Kaunda]

Kevin Buzzard said:

Sorry, that first comment was for me not you, I'm on mobile so needed a link to the module to see what it was called (it says at the top)

Noted.

[Kevin Buzzard]

The definition of a prime number seems to be in a ...Defs file, but the theorems are now in a ...Basic file. I guess this changed recently
Where did you see the out of date import?

[Kajani Kaunda]

Kevin Buzzard said:

The definition of a prime number seems to be in a ...Defs file, but the theorems are now in a ...Basic file. I guess this changed recently
Where did you see the out of date import?

A you tube Video!

[Kajani Kaunda]

The following now works. No errors! thank you so much. I was using the code to test my first VS Code + Lean setup. You are a life saver, thank you. The YouTube video was from the Lean community YouTube channel. A good Video I must say. No ones fault really, considering the rapid changes in the tech landscape. I thought I should mention that.

import Test.Basic
--Now the following line works Beautifully, no error.
import Mathlib.Data.Nat.Prime.Basic
open Nat
#eval 11 + 33
#eval hello
theorem infinitude_of_primes : ∀ N, ∃ p ≥ N, Prime p := by
  sorry -- Replace with actual proof

[Kevin Buzzard]

Videos are the hardest to update :-)