Zulip Chat Archive
Stream: new members
Topic: unknown identifier 'finset.sum_erase_add'
Jelmer Firet (Dec 12 2021 at 16:05):
I have mathlib installed and can work with many of the definitions in there.
However finset.sum_erase_add seems not to be available, even though it is documented in mathlib:
https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html#finset.sum_erase_add
unknown identifier 'finset.sum_erase_add'
state:
d n : ℕ,
i : fin d,
f : fin d → ℕ,
f_sum : ∑ (i : fin d), f i = n
⊢ ∑ (x : fin d) in finset.univ.erase i, f x + f i = n
I just upgraded mathlib with leanproject (both globally and locally) and restarted lean in VSCode. The issue persists.
mathlib commit that leanproject used : d856bf9b7fd5c46c24e5b0159ffc8e9bbec20242
Kevin Buzzard (Dec 12 2021 at 16:06):
Can you post fully working code? aka "are you sure you imported the right file?"
Kevin Buzzard (Dec 12 2021 at 16:07):
Jelmer Firet (Dec 12 2021 at 16:08):
Kevin Buzzard (Dec 12 2021 at 16:08):
PS I'm not sure there's such a thing as a global mathlib, but this is another matter
Kevin Buzzard (Dec 12 2021 at 16:09):
Sorry, I'm on mobile. Is algebra.big_operators.basic imported?
Jelmer Firet (Dec 12 2021 at 16:09):
Yes (accidentally even twice)
Kevin Buzzard (Dec 12 2021 at 16:12):
(note that I just edited my post to add .basic, in case that makes a difference). I'm not at lean right now, sorry, and I can't see your file because the Android app doesn't let me download it (it wants to switch to another app to view it and the other app doesn't have access to the Zulip instance). Hopefully someone at a computer can help
Kevin Buzzard (Dec 12 2021 at 16:14):
Actually maybe I can do epsilon more debugging. I'm assuming you're working in a lean project. Is this project mathlib itself or a project with mathlib as a dependency?
Kevin Buzzard (Dec 12 2021 at 16:15):
Do other definitions in algebra.big_operators.basic work?
Jelmer Firet (Dec 12 2021 at 16:17):
Kevin Buzzard said:
Actually maybe I can do epsilon more debugging. I'm assuming you're working in a lean project. Is this project mathlib itself or a project with mathlib as a dependency?
Should be a project with mathlib as a dependency. It is just somewhere to play around with lean
Jelmer Firet (Dec 12 2021 at 16:18):
Yes, for example finset.sum_singleton works which is also in algebra.big_operators.basic. Other than this issue I seem to be able to use sums just fine.
Yaël Dillies (Dec 12 2021 at 16:40):
Btw we've an almost complete proof of Sperner's lemma at branch#sperner-again
Kevin Buzzard (Dec 12 2021 at 16:41):
So on the command line navigate to the root directory of the project that the file is in, then change directory to _target/deps/mathlib and run git log. Is the most recent commit from today?
Kevin Buzzard (Dec 12 2021 at 16:42):
The reason I ask this is that you said something a bit weird about updating mathlib earlier
Jelmer Firet (Dec 12 2021 at 16:45):
The commit hash corresponds to the branch origin/lean-3.35.1 which was last updated yesterday.
Jelmer Firet (Dec 12 2021 at 16:46):
Kevin Buzzard said:
PS I'm not sure there's such a thing as a global mathlib, but this is another matter
https://leanprover-community.github.io/leanproject.html#global-mathlib-install
I have since removed ~/.lean but still the same issue
Kevin Buzzard (Dec 12 2021 at 16:57):
Your answers do not correspond to my question at all. Here is a conjecture: you have several mathlibs installed on your system and your file is looking at the wrong one. Can we start again? Are you working within a lean project? Have you opened the root directory of the project in VS Code?
Kevin Buzzard (Dec 12 2021 at 17:00):
Here's an easy thing you can do -- write #check finset.<name of a lemma in algebra.big_operators.basic which is working for you> and then right click on the name of the lemma and jump to definition. Now you'll be in the version of mathlib which lean is using in your file. Can you see the declaration sum_erase_add there? My guess is no
Kevin Buzzard (Dec 12 2021 at 17:01):
Re global install--note the "this is generally discouraged" line and right now you're seeing why.
Jelmer Firet (Dec 12 2021 at 17:03):
The project opened in VSCode was different than the one the file was in. Opened the right folder in VSCode and now it works
Kevin Buzzard (Dec 12 2021 at 17:03):
Nice!
Kevin Buzzard (Dec 12 2021 at 17:04):
Yeah you need to open the relevant root project directory if you're working on a file in a project. The entire system is a little brittle.
Kevin Buzzard (Dec 12 2021 at 17:04):
This is a common gotcha
Last updated: Dec 20 2023 at 11:08 UTC