Zulip Chat Archive

Stream: new members

Topic: mathlib dependency

Jakob Scholbach (Nov 09 2019 at 20:21):

I am trying to use mathlib for the first time. I successfully applied the tutorial here https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md and also did the first steps here https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

But when I write "import topology.basic" in a file as explained there, I get an error message in VS as

test.lean:1:0: error
file 'theory\set_theory' not found in the LEAN_PATH
test.lean:1:0: error
invalid import: theory.set_theory
could not resolve import: theory.set_theory

The mathlib files were successfully downloaded (situated in C:\Users\me\lean\alggeo\_target\deps\mathlib\src). My folder
C:\Users\me\lean\alggeo contains a file named leanpkg.path having as contents

path _target/deps/mathlib/src
path ./src

What needs to be done to resolve this problem? Thanks!

Bryan Gin-ge Chen (Nov 09 2019 at 20:23):

Did you open the C:\Users\me\lean\alggeo folder in VS Code or just a file in it? You need to do the former, otherwise Lean will not look for dependencies in the right place.

Johan Commelin (Nov 09 2019 at 20:23):

@Jakob Scholbach Welcome!

Johan Commelin (Nov 09 2019 at 20:24):

Little Zulip hint: if you format code like this:

code goes here

then you'll get syntax highlighting for free

Johan Commelin (Nov 09 2019 at 20:25):

@Jakob Scholbach Did you follow one of the installation tutorials? E.g. this one: https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md ?

Reid Barton (Nov 09 2019 at 20:26):

Where is theory.set_theory coming from? The only place I've seen it is in another new user question like yours.

Jakob Scholbach (Nov 09 2019 at 20:27):

Thanks, yes I did follow the tutorial except for opening not the folder in VS, but the file. Bryan's tip helped me. Now it works.

Kevin Buzzard (Nov 09 2019 at 20:31):

+1 to Reid's question. It would be nice to resolve why some new users are reporting this error. Is there some error in some docs somewhere?

Jakob Scholbach (Nov 09 2019 at 20:33):

I saw this theory.set_theory here https://leanprover.github.io/reference/using_lean.html#import-resolution, but the problem also arose with imports such as import topology.basic. But again, the latter now works, so the problem is solved, thanks everyone.

Kevin Buzzard (Nov 09 2019 at 20:36):

Absolute imports are resolved according to the entries in the leanpkg.path file. That is, when executing import theory.set_theory, Lean looks for a file called theory/set_theory.lean in the src directories of all (transitive) dependencies as well as the current package.

This is in the Lean reference manual! It might well be the case that Lean looks for that file -- but it is not made at all clear that no such file exists in any repository we know of e.g. mathlib!

Jakob Scholbach (Nov 09 2019 at 20:37):

Yes, sure. Thanks.

Johan Commelin (Nov 09 2019 at 20:38):

Ha, I guess it would be helpful if that example refered to a file that actually ships with core Lean

Johan Commelin (Nov 09 2019 at 20:39):

Ooh, that doesn't make sense... because you don't need to import from core Lean

Bryan Gin-ge Chen (Nov 09 2019 at 20:42):

You do have to import for some stuff provided with core Lean, e.g. system.io. You don't need to import stuff inside init, which, admittedly, is essentially everything provided which is useful for doing math.

Last updated: Dec 20 2023 at 11:08 UTC