Probelm in analysis.real about mathlib HOT 12 CLOSED

It sounds like it is confusing the notation '' used for function image with an empty character literal. Does import data.set.basic work?

from mathlib.

Yes, it does work.

from mathlib.

Do you compile the most recent mathlib using leanpkg build?
It works for me without problem. Do you have any changes in mathlib?

from mathlib.

Yes. I did exactly that:
leanpkg add https://github.com/leanprover/mathlib
then
leanpkg build. I did no changes to mathlib.

from mathlib.

If you just create a file test.lean with "import analysis.real" and then type lean test.lean are there any problems? I am using lean linux nightly (my output of lean --version is Lean (version 3.3.1, commit 07bb7d809b6b, Release)) and mathlib HEAD and if I run this in a directory with an appropriate leanpkg.path then it works fine for me.

from mathlib.

Another idea -- why not try removing all .olean files in your mathlib (and then making them again with the current version of leanpkg if you want)? In the past .olean files compiled with previous versions of Lean have caused pretty random problems which were hard to debug.

from mathlib.

If you just create a file test.lean with "import analysis.real" and then type lean test.lean are there any problems? I am using lean linux nightly (my output of lean --version is Lean (version 3.3.1, commit 07bb7d809b6b, Release)) and mathlib HEAD and if I run this in a directory with an appropriate leanpkg.path then it works fine for me.

Indeed, running lean (exactly the same version here) from the command line works fine (i.e. no errors)

from mathlib.

Do you mean "I can import analysis.real with no errors if I do it from the command line"? If so, then the issue is with your IDE set-up I guess. But if you mean "I can run lean --version no problem" then what happens if you try to import analysis.real from the command line?

from mathlib.

I meant the first thing: "I can import analysis.real with no errors if I do it from the command line". So it seams to be a problem in Visual Studio config.

from mathlib.

So in VS Code, File->Preferences->Settings will open user settings and you can see the value attached to "lean.executablePath" to check to see if you are using the right lean. Another gotcha is that if you open a folder with File -> Open Folder and if this folder has a leanpkg.path in then I think this overwrites any LEAN_PATH system variable which you might have set, and in this case you might be using the wrong mathlib. Try opening the root dir of your project with File -> Open Folder and see if this fixes it. These things are very fiddly to set up :-/

from mathlib.

Actually, the problem laid in the fact that running leanpkg build in the top directory of the project did not compiled mathlib. One needs to go to _target/deps/mathlib and run it from there. So I think the issue can be closed now.

from mathlib.

Use lean --make instead of leanpkg build

from mathlib.