no idea what i'm doing with mathlib

Stream: new members

[John Doe]

i am having a lot of trouble importing anything from mathlib even though i think it is installed

my lean code:

import Mathlib.Algebra.BigOperators

open BigOperators
open Finset

def sumSquares (n : ℕ) : ℕ :=
  ∑ i in Finset.Icc 1 n, i^2

my lakefile.toml:

name = "test_project_3"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["TestProject3"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[lean_lib]]
name = "TestProject3"

the error in vscode:

`c:\Users\name\.elan\toolchains\leanprover--lean4---v4.25.0-rc2\bin\lake.exe setup-file C:/Users/name/programming/lean4/test_project_3/TestProject3.lean -` failed:

stderr:
✖ [3/4] Running Mathlib.Algebra.BigOperators
error: no such file or directory (error code: 2)
  file: C:\Users\name\programming\lean4\test_project_3\.lake\packages\mathlib\Mathlib\Algebra\BigOperators.lean
✖ [4/4] Running setup-file C:/Users/name/programming/lean4/test_project_3/TestProject3.lean
trace: file identified as module: TestProject3
error: TestProject3.lean: bad import 'Mathlib.Algebra.BigOperators'
Some required targets logged failures:
- Mathlib.Algebra.BigOperators
- setup-file C:/Users/name/programming/lean4/test_project_3/TestProject3.lean
Failed to build module dependencies.

in powershell, i did lake exe cache get (which took ~20 mins) but lake build failed similarly.

[Damiano Testa]

Mathlib.Algebra.BigOperators does not seem to be a file, but a dir. You can only import files.

[John Doe]

ok

[John Doe]

i tried very hard and the following seems to work

import Mathlib.Algebra.Group.Pointwise.Finset.BigOperators

open Finset
open scoped BigOperators

-- #eval (1 + 2 + 3 : Nat)   -- => 6

#eval (∑ i ∈ range 4, i)

[Eric Wieser]

import Mathlib is usually what you actually want

[John Doe]

import Mathlib seems very slow for me but i could try it again

[John Doe]

ok no i started trying to import mathlib 5 minutes ago and vscode still hasn't finished updating

[John Doe]

so i just don't think it's a valid option for me

[Weiyi Wang]

You should ensure you run lake exe cache get first (and occasionally I restart vscode after running this just to get rid of weird cache problem), then import Mathlib should take just a few second

[John Doe]

i did that before, it took about 20 minutes

[John Doe]

do i need to do it again now

[Weiyi Wang]

hmm, that's weird. During the 20 minutes, does it show it is building anything?

[Eric Wieser]

John Doe said:

do i need to do it again now

It should be faster the second time

[Eric Wieser]

Are you on Windows? Is your antivirus getting in the way?

[John Doe]

ok, let me try it now

[John Doe]

import Mathlib.Algebra.Group.Pointwise.Finset.BigOperators

open Finset
open BigOperators

-- #eval (1 + 2 + 3 : Nat)   -- => 6

#eval (∑ i ∈ range 4, i)

current code

[John Doe]

Eric Wieser said:

Are you on Windows? Is your antivirus getting in the way?

i am on windows; how do i tell if that is slowing things down?

[Weiyi Wang]

oh sorry, I didn't read the whole context. Did you mean getting cache itself took 20 minutes?

[John Doe]

i am going to run lake exe cache get now, let's see how long it takes this time

[Weiyi Wang]

You don't need to run cache get multiple times as long as it succeeds the first time and you didn't update mathlib version

[John Doe]

ok. should i cancel the current run then?

[Weiyi Wang]

if it is ongoing I wouldn't cancel it. But I also wonder why this one is slow. Perhaps slow internet?

[Weiyi Wang]

It usually takes me no more than a minute, but I do have somewhat fast connection

[John Doe]

it's giving errors anyway so i cancelled it

The requested operation cannot be performed on a file with a user-mapped section open. (os error 1224)

[John Doe]

if it is ongoing I wouldn't cancel it. But I also wonder why this one is slow. Perhaps slow internet?

my internet is usually reasonable but maybe it was bad just during that time

[Weiyi Wang]

Is this on Windows natively or Windows WSL?

[John Doe]

regardless, import Mathlib definitely took an unreasonable amount of time even after i got the cache the first time

[John Doe]

windows 10?

[John Doe]

i'm not linux

[Weiyi Wang]

Ok I assume that's not WSL if you say "not linux". Then I have no idea what that error means

[John Doe]

my guess is it's just because i have some folder open

[Weiyi Wang]

If your "lake exe cache get" fails with any error, then import Mathlib will likely needs to rebuild locally, which is like 30 minutes or something

[John Doe]

it succeeded the first time

[Weiyi Wang]

hmm, could also be just a conflict between vscode terminal and vscode extensions. You can try closing vscode and just running that command in a standalone command line / powershell

[John Doe]

oh, to be clear, all of these commands have been run in powershell

[John Doe]

i am not very familiar with vscode, usually i just program in notepad++

[Aaron Liu]

John Doe said:

it's giving errors anyway so i cancelled it

The requested operation cannot be performed on a file with a user-mapped section open. (os error 1224)

Usually when this happens I just stop-process -name "lean" and try again

[John Doe]

ok i closed windows file explorer and voidtools everything and vscode and ran lake exe cache get again

there was a brief flicker of text but i couldn't read it because it disappeared too quickly, then no changes for around 70s (i am using the stopwatch app on my phone), then it said:

Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7492 file(s)

total time now at 5 minutes and counting

[Weiyi Wang]

hmm, if it is slow on Decompressing, it could be slow disk, or antivirus scanning, or a combination of both

[John Doe]

it completed successfully after roughly 9 minutes total. let me try import Mathlib again. it could just be my computer is slow in which case i'm screwed

[John Doe]

okay import Mathlib actually did finish loading in vscode after ~11 minutes.

good to know that it can work in theory; however, this is still very awkward.

[Weiyi Wang]

Yeah those numbers still look slow to me, but good to know that there isn't anything broken that completely block the process. In another thread there was some success story about adding Lean folder to Windows Defender's list to skip scanning. Other than that, it is probably about the hardware performance

[John Doe]

thanks for giving advice. at least i can start actually trying to prove things now

[Alfredo Moreira-Rosa]

Slowness can come from many things (more likely first) :

• low memory (<= 4 GB of RAM) => computer using swap all the time
• antivirus / corporate protected computer
• slow disk (not SSD, or not nvme SSD)
• slow CPU (like old intel i3 series)

A lot of cheap chrome books enter this category.

[Etienne Marion]

My old laptop was very slow to process import Mathlib too, because of performance. One trick you can use is get started in the web editor and then use #min_imports to get a decent list of imports which you can run locally. Then if you need a result that you do not import you can check the file in documentation and then import that to your file.