Downloading lean

Stream: new members

[Matthew Honnor]

Hi all,

I have been trying to download lean and have followed the instructions on https://leanprover-community.github.io/install/windows.html . Everything looked good (I have downloaded lean on another computer before and everything seems the same). However when I try to start a lean project it is not able to find any imports. Looking at the output in the terminal when I run

 leanproject new my_project

I get the following at the start of the output:

fatal: detected dubious ownership in repository at '//icnas3.cc.ic.ac.uk/mhonnor/my_project'
To add an exception for this directory, call:

        git config --global --add safe.directory '%(prefix)///icnas3.cc.ic.ac.uk/mhonnor/my_project'
WARNING: failed to initialize git repository
configuring my_project 0.1
Cmd('git') failed due to: exit code(129)
  cmdline: git diff --abbrev=40 --full-index --raw
  stderr: 'warning: Not a git repository. Use --no-index to compare two paths outside a working tree
usage: git diff --no-index [<options>] <path> <path>

I assume that this is the problem I'm having. Any help with this would be much appreciated.
Thanks,
Matthew.

[Kevin Buzzard]

It looks like git is failing for some reason but I would imagine that as far as lean goes things should be working fine. If you open the root directory of the project folder with VS Code does it all work fine? PS Hi Matthew!

[Matthew Honnor]

Hi Kevin,

I'm not sure what the root directory is I'm afraid. I've opening the project folder in VS Code and then things look like this when I try to run an import:

image.png

Thanks.

[Anne Baanen]

Since there is no _target folder, you probably need to (re-)add the mathlib dependency. Could you try going to the my_project folder in the command line and running leanproject add-mathlib?

[Kevin Buzzard]

Yes, the error is worse than I expected: there is no mathlib right now. You're using some kind of Imperial shared drive, right? Why not just try making the repository on a local drive on the computer you're using, and then if it works then just move it all into the shared drive.

[Matthew Honnor]

I have tried running this and had the following output:

image.png

Thanks for your help

[Kevin Buzzard]

When you use the command line, it's just like a graphical file manager which you use to move between directories and to double-click on applications, just without the graphics. In particular when you're using the command line you are "in" a certain directory, even though it's harder to see where you are than when you're using a file manager. I'm suggesting that you move to another directory and try installing there instead. Right now you are trying to create a Lean project in some kind of networked drive which might not have the right permissions.

[Anne Baanen]

Okay, so it looks like the helper programs aren't even allowed to modify files in your project, but VS Code is? :open_mouth: I agree with Kevin that it's likely the shared drive is causing trouble somehow.

[Kevin Buzzard]

Right now you are in /h/my_project. This is some kind of shared file system. Can you move to /c/somewhere/you/have/write/access/to, with something like cd /c/ and then ls and then cd (directory which looks promising) and then continue going until you find a place on the computer you're using which git won't complain about?

[Kevin Buzzard]

e.g. /c/users/mhonnor/desktop or something?

[Matthew Honnor]

I see, I will try this and hopefully it will fix the problem. Thanks for all your help

[Matthew Honnor]

Everything is working now! :tada: Thanks Kevin and Anne for all your help