Ali Miller

Stream: new members

[Alistair Miller]

Hi! I'm Ali and I'm new here - I'm doing a PhD in operator algebras at Queen Mary Uni of London and just saw Kevin's talk the other day at the BMC.

[Johan Commelin]

@Alistair Miller Welcome! You might have already found it, but a good place to start is https://leanprover-community.github.io/learn.html

[Alistair Miller]

Thanks! This website seems really useful

[Alistair Miller]

I'm having a couple of issues with installation to do with the fact that my laptop is managed by QMUL and I don't have admin rights etc, but I can probably get those sorted eventually. I suppose the browser version should be good enough to try things out and get started anyway?

[Bryan Gin-ge Chen]

You can play the Natural Number Game in the browser, but I wouldn't recommend attempting too much more.

[Adam Topaz]

IIRC, root privileges are not required to set things up... @Alistair Miller what issues are you having?

[Alistair Miller]

The issues I'm having are to do with python. In particular, I'm not sure how to "Add Python 3.x to PATH" in https://leanprover-community.github.io/install/windows.html (Python is already on the laptop)

[Alistair Miller]

so "which python" doesn't find anything

[Adam Topaz]

Oh. Windows. Sorry I can't help with that! Hopefully another windows user can chime in. Maybe @Eric Wieser ?

[Alistair Miller]

Haha yes, Windows... I imagine it's something I'll need IT support for anyway so I can look forward to trying things out on monday :upside_down:

[Eric Rodriguez]

Ali, try searching "Edit the System Environment Variables" → Environment Variables, and then in the "User variables" (should be top one, scroll down to PATH, click it and then press Edit just below it

[Eric Rodriguez]

You should then be able to add the folder where Python is in to a new line there, and then after restarting your PC which python _should_ work

[Eric Rodriguez]

Sorry, in Windows it's where python

[Alistair Miller]

Eric Rodriguez said:

Ali, try searching "Edit the System Environment Variables" → Environment Variables, and then in the "User variables" (should be top one, scroll down to PATH, click it and then press Edit just below it

Unfortunately this seems to require admin privileges, but I can ask the IT staff to do this so thanks!

[Eric Rodriguez]

Even just user variables? That's odd... but yeah if not ask your IT staff!

[Alistair Miller]

ooh actually I seem to be able to open it this time

[Kevin Buzzard]

If you think this is hard, wait until you start proving theorems :P

[Adam Topaz]

I think proving theorems is easier than figuring out how to set up path variables in windows

[Kevin Buzzard]

Maybe, but you've had a lot of practice proving theorems now :-)

[Alistair Miller]

so I'm in "Edit environment variable" and I should then click "New" and paste the location of the folder that python is in?

[Kevin Buzzard]

I think you're supposed to be changing the environment variable called PATH or $PATH or whatever

[Eric Rodriguez]

Yeah, paste the Python folder there

[Eric Rodriguez]

image.png

[Eric Rodriguez]

should look something like this

[Eric Rodriguez]

(ignore my specific folders not the relevant part :b) just that I highlighted Path behind)

[Eric Rodriguez]

(deleted)

[Alistair Miller]

I did this and it immediately forgot that I did this, I can post screenshots hold on

[Kevin Buzzard]

The PATH variable should be a list of directories, and they're the ones which your OS will look in if you type something on the command line. e.g. if you type python on the command line I'm assuming that it doesn't work right now, but that is because none of the directories listed in PATH have got a file in them called python.exe. The idea is to tell PATH where your python.exe is.

[Alistair Miller]

Alright it's now there - does it have to be the original python file or can it be the shortcut?

[Kevin Buzzard]

Ultimately your aim is to get python3 --version and pip3 --version working on the command line. I think that as long as they work, you should be OK.

[Eric Rodriguez]

It has to be the folder where python.exe is located

[Eric Rodriguez]

cmd and such like don't see through shortcuts

[Alistair Miller]

hooray, which python found something (the second time)

[Kevin Buzzard]

you need python3 to work I think. Do you have write access to the directory where python is installed?

[Kevin Buzzard]

In the docs they just suggest making a copy of python.exe and calling it python3.exe.

[Kevin Buzzard]

But if you can't write to the directory then you might have trouble doing what they say in the docs.

[Alistair Miller]

ah I just tried the next step and "cp "$(which python)" "$(which python)"3" failed due to permissions - is this copying and renaming a fix to this step?

[Eric Rodriguez]

yeah, that's code that only works on linux

[Johan Commelin]

I guess you can create a directory python_stuff in your documents folder, and copy python there.

[Johan Commelin]

Then add python_stuff to your path.

[Alistair Miller]

I'm doing this in git bash by the way

[Eric Rodriguez]

python3 may already be there actually

[Eric Rodriguez]

My python install came with it

[Eric Rodriguez]

I think maybe the wisest next step is just trying to see if leanproject works; if not, I think it's probably debuggable

[Kevin Buzzard]

Kevin Buzzard said:

Ultimately your aim is to get python3 --version and pip3 --version working on the command line. I think that as long as they work, you should be OK.

It's worth checking to see if these two commands work by now. If they do, you're all set. This is your aim right now.

[Alistair Miller]

alright so python3 seems to work but pip3 doesn't

[Alistair Miller]

(both in cmd and in git bash)

[Kevin Buzzard]

you can perhaps try doing what Johan suggests -- copy pip to a new directory which you have write access to, add that new directory to PATH and then rename pip to pip3. Or you can try what Eric suggests, and just go for it anyway.

[Alistair Miller]

should pip be in the same folder that python.exe was in?

[Kevin Buzzard]

I don't know enough about python on windows to answer this question

[Kevin Buzzard]

oh -- your original pip should be, if you're asking "where is it?"

[Kevin Buzzard]

what I don't know is whether it will continue to work if you copy it elsewhere.

[Alistair Miller]

yes I found it in the "Scripts" subfolder of the folder that python.exe was in, but I copied it and renamed it and it doesn't seem to work

[Alistair Miller]

Unable to create process using '\\sfs1.qm.ds.qmul.ac.uk\H2\Documents\python.exe \\sfs1.qm.ds.qmul.ac.uk\H2\Documents\Python\pip3-script.py --version'

[Alistair Miller]

That happens when I try the pip3 --version command

[Kevin Buzzard]

Well you can either go risky and just ignore the problem and continue and try to fix things up later, or you can just re-install python 3 (i.e. download and install from the internet) in a directory which you do have write access to, and then add this directory to the path and remove the annoying python3 directory from the path.

[Eric Rodriguez]

hmm, this is why i thought the copypasting may not work; stuff maybe in the subdirs. @anyone who knows better, does leanproject use pip3 internally to self-update or does it just use python3 to run its stuff?

[Kevin Buzzard]

If python3 --version is working you might just want to chance it and continue on, and we'll see if we can work around any errors which occur. But my suggestion of installing another python in a place which you have write access to is bound to work (it just involves a bunch more fiddling).

[Alistair Miller]

I could try copying over the entire folder that python.exe was in, and then renaming python and pip to python3 and pip3? Downloading and installing python from the internet is unlikely to be approved by IT given that they are already providing me with python though

[Kevin Buzzard]

I think that copying folders around is unlikely to work. I don't really understand what you're saying about downloading and installing python from the internet -- are you allowed to download a pdf file from the internet and put it on your computer? There's no difference between downloading a pdf and downloading a programming langauge, is there?

[Alistair Miller]

hm, at least if I attempt to download python in the usual way it prompts me for an admin login

[Alistair Miller]

It's running the installer that prompts this not downloading the installer

[Kevin Buzzard]

I can say nothing more. I have never used Windows in my life and I have no real idea how to solve the problems you're facing. Did you try the "just go for it" method yet?

[Alistair Miller]

the next step on https://leanprover-community.github.io/install/windows.html was to use pip3, which didn't work. What does the "just go for it" method involve?

[Alistair Miller]

my impression is that I need pip3 to get mathlib, is this true?

[Kevin Buzzard]

Just use pip instead.

[Kevin Buzzard]

It's the same thing

[Kevin Buzzard]

(assuming you have python3 installed and not python2!)

[Alistair Miller]

Yes I'm fairly sure it's python3! So I'm finding that pip --version is also not working, I'm going to try adding the Scripts subfolder to Path additionally to see if that fixes it.

[Kevin Buzzard]

Or just write path/to/pip install mathlibtools (i.e. write the fully qualified path name on the command line)

[Alistair Miller]

hm neither of those are working. However, I just ran Python and it says

Warning:
This Python interpreter is in a conda environment, but the environment has
not been activated. Libraries may fail to load. To activate this environment
please see https://conda.io/activation

So I'm going to look into fixing this as it might be the source of my problems

[Eric Rodriguez]

ahh, seems your computer has conda installed... that makes things a lot more annoying; probably worth just asking IT guys here, this starts being very non-trivial

[Eric Rodriguez]

can confirm the NNG is good fun to mess around with in the meantime, while this gets sorted!

[Alistair Miller]

Yes that seems like a good idea! thanks all for your patience

[Alistair Miller]

Out of interest are there any other operator algebraists around here?

[Eric Wieser]

Sounds like you've ended up here: https://xkcd.com/1987/

[Alistair Miller]

yep I've asked some other PhD students and they've also had to get in touch with IT staff to get python working properly

[Alistair Miller]

I might have a go at getting things working on my personal PC though once I've explored the natural numbers game a bit more :)

[Eric Wieser]

Usually the problem is everyone tells you to install python from scratch a different way, sometimes with a gap of months, and you forget you also have three other installations somewhere

[Alistair Tucker]

I have conda on my mac and it works ok. I can't be sure exactly what I did but it must have begun with something like:

conda create -n mathlibtools toml pygithub certifi gitpython requests click tqdm networkx pydot pyyaml
conda activate mathlibtools

If I've got all the requisite dependencies in that first line then leanproject and friends will never even try to call pip.

[Alistair Miller]

Much smoother on my personal laptop! currently looking at the tutorial project

[Alistair Miller]

How intensive does lean get on your pc?

[Alistair Miller]

(this is a very slow pc)

[Kevin Buzzard]

If you are using leanproject correctly then you should have a fully compiled mathlib, but even with that things can be a bit painful if you have < 8 gigs of ram.

[Eric Rodriguez]

depends very much on the size of the project :b I've got some theorems that take milliseconds to update, some a few seconds, and the whole of mathlib takes an hour to compile

[Eric Rodriguez]

how do you change allocated ram btw @Kevin Buzzard ? I've run into ram limits before but I have quite a bit

[Johan Commelin]

@Eric Rodriguez In VScode there is a setting for it

[Eric Rodriguez]

dope, thanks Johan

[Alistair Miller]

yes I've got 4 gig on this one - we'll see!

[Alistair Miller]

After I've had a look through the tutorial project are there any recommendations for what to look at next?

[Eric Rodriguez]

I've been liking Kevin's course that he uploaded here: https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/

[Alistair Miller]

great thanks - this looks well-suited to me

[Johan Commelin]

https://leanprover-community.github.io/learn.html

[Bryan Gin-ge Chen]

(We should add Kevin's course to that page!)

[Kevin Buzzard]

At some point soon I will tidy up the README on github so that it points to the 8 blog posts.

[Patrick Massot]

Alistair Miller said:

How intensive does lean get on your pc?

At least with default settings (and I don't know if this can be changed) lean will eat up everything you have. Using Lean on an unplugged laptop is a very good way to see you battery level going down really fast (and warm up your room).

[Alistair Miller]

So I'm reading through the mathematics_in_lean tutorial, and I've hit a slight snag at the end of the introduction at https://leanprover-community.github.io/mathematics_in_lean/introduction.html

In the last example, I tried opening it up and using a comma, but I get the message "command expected". Is this what is supposed to happen?

[Kevin Buzzard]

Are you saying: "I typed this

example : ∀ m n : nat, even n → even (m * n) :=
by intros; simp * with parity_simps

into Lean and then I replaced the semicolon with a comma and it didn't work"? Or are you saying something else?

[Alistair Miller]

I'm saying I put a comma at the end and it didn't work

[Alistair Miller]

a comma after "parity_simps" that is

[Kevin Buzzard]

That's intended behaviour. What's your question?

[Kevin Buzzard]

If you want to investigate the proof, you coudl change by to begin ... end:

import data.nat.parity tactic
open nat

-- BEGIN
example : ∀ m n : nat, even n → even (m * n) :=
begin
  intros m n hn,
  simp * with parity_simps,
end

[Alistair Miller]

ahh that makes sense, thanks!