mathlib dependency

Stream: new members

[Jakob Scholbach]

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

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

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

[Bryan Gin-ge Chen]

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]

@Jakob Scholbach Welcome!

[Johan Commelin]

Little Zulip hint: if you format code like this:

```lean
code goes here
```

then you'll get syntax highlighting for free

[Johan Commelin]

@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]

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

[Jakob Scholbach]

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]

+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]

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]

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]

Yes, sure. Thanks.

[Johan Commelin]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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.