Zulip Chat Archive

Stream: new members

Topic: group theory

Anatole Dedecker (Jun 24 2021 at 13:05):

You might also be interested to have a look at https://leanprover-community.github.io/lftcm2020/

Sai Gopal (Jun 24 2021 at 13:19):

https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/README.md

Sai Gopal (Jun 24 2021 at 13:20):

I have installed and set up everything for lean

Sai Gopal (Jun 24 2021 at 13:20):

can someone help me how to install it for using it

Sai Gopal (Jun 24 2021 at 13:21):

they asked to "by firing up a command line" means what ?

Adam Topaz (Jun 24 2021 at 13:22):

What operating system are you using?

Sai Gopal (Jun 24 2021 at 13:22):

windows

Sai Gopal (Jun 24 2021 at 13:22):

10

Adam Topaz (Jun 24 2021 at 13:22):

https://leanprover-community.github.io/install/windows.html

Sai Gopal (Jun 24 2021 at 13:22):

Thank you

Sai Gopal (Jun 24 2021 at 13:23):

I am not looking for this

Sai Gopal (Jun 24 2021 at 13:23):

https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/README.md

Sai Gopal (Jun 24 2021 at 13:24):

This is a GitHub project and how should I use the excercises

Adam Topaz (Jun 24 2021 at 13:26):

The link I sent will walk you through installing lean and the user tools which are needed for the "How to play" section in the link you sent

Adam Topaz (Jun 24 2021 at 13:28):

Ah I see your earlier message now. So you have lean and mathlibtools set up?

Sai Gopal (Jun 24 2021 at 13:30):

yes

Adam Topaz (Jun 24 2021 at 13:30):

If so, then you need to open up a terminal, and run the commands mentioned under the How to Play section.

I don't know the best way to do this in windows. I hope another windows user will chime in.

Eric Rodriguez (Jun 24 2021 at 13:32):

what stage are you at right now? very happy to walk you through this

Adam Topaz (Jun 24 2021 at 13:33):

The windows directions I sent involve running commands in a terminal. How did you set up lean and tools without a terminal?

Sai Gopal (Jun 24 2021 at 13:33):

Well, I just set up all tools and went through natural number game.

Eric Rodriguez (Jun 24 2021 at 13:34):

did you do the natural number game online or locally?

Sai Gopal (Jun 24 2021 at 13:34):

nothing more. I want to play group theory git hub project whose link i shared earlier

Sai Gopal (Jun 24 2021 at 13:35):

online

Eric Rodriguez (Jun 24 2021 at 13:35):

okay, have you got VSCode installed?

Sai Gopal (Jun 24 2021 at 13:35):

yes

Adam Topaz (Jun 24 2021 at 13:35):

Did you set up elan?

Adam Topaz (Jun 24 2021 at 13:35):

(that's not a typo)

Sai Gopal (Jun 24 2021 at 13:36):

yes

Eric Rodriguez (Jun 24 2021 at 13:36):

what happens if you type leanproject on a commandline

Sai Gopal (Jun 24 2021 at 13:40):

an executable file opened

Eric Rodriguez (Jun 24 2021 at 13:42):

alright, try clone that git repo to some folder somewhere in your system

Adam Topaz (Jun 24 2021 at 13:42):

Do you have git installed, as in the directions I sent? If so, start by running git bash and that will open a terminal. Then you can try leanproject in the terminal window

Sai Gopal (Jun 24 2021 at 13:44):

yes. I opened gitbash and typed "leanproject" which opened .exe file now what ?

Eric Wieser (Jun 24 2021 at 13:44):

What do you mean by "opened exe file"?

Sai Gopal (Jun 24 2021 at 13:44):

@Eric Rodriguez I did not get you

Eric Wieser (Jun 24 2021 at 13:45):

did it run it and print out help text like

Usage: leanproject.py [OPTIONS] COMMAND [ARGS]...

Sai Gopal (Jun 24 2021 at 13:45):

no

Eric Wieser (Jun 24 2021 at 13:45):

(I think a zulip maintainer should move this to #new members since this is installation troubleshooting)

Eric Wieser (Jun 24 2021 at 13:46):

(but until they do we can keep troubleshooting here)

Eric Rodriguez (Jun 24 2021 at 13:46):

@Sai Gopal on gitbash, do you know how to navigate to a folder?

Eric Wieser (Jun 24 2021 at 13:46):

Sai Gopal said:

no

Then what did it do? Can you attach a screenshot?

Sai Gopal (Jun 24 2021 at 13:48):

@Eric Rodriguez NO

Notification Bot (Jun 24 2021 at 13:49):

This topic was moved here from #general > group theory by Mario Carneiro

Eric Rodriguez (Jun 24 2021 at 13:49):

Sai, make a folder somewhere where you'd want to keep the tutorial project and then try take a screenshot of where that folder is

Eric Rodriguez (Jun 24 2021 at 13:50):

this gets easier with time I promise you ^^

Eric Wieser (Jun 24 2021 at 13:50):

In case you don't know, you can take a screenshot with ⊞ Win + shift + s

Sai Gopal (Jun 24 2021 at 13:52):

then ?

Eric Wieser (Jun 24 2021 at 13:52):

Paste the screenshot into zulip

Sai Gopal (Jun 24 2021 at 13:53):

ok the folder I created ?

Sai Gopal (Jun 24 2021 at 13:53):

Its just on desktop.

Eric Wieser (Jun 24 2021 at 13:54):

Can you take a screenshot of what happens when you say

yes. I opened gitbash and typed "leanproject" which opened .exe file now what ?

Sai Gopal (Jun 24 2021 at 13:54):

sure this ILL send

Sai Gopal (Jun 24 2021 at 13:56):

I think I was mistaken last time

Sai Gopal (Jun 24 2021 at 13:56):

It has printed some content

Sai Gopal (Jun 24 2021 at 13:57):

this time

Sai Gopal (Jun 24 2021 at 13:59):

what to do next ?

Sai Gopal (Jun 24 2021 at 13:59):

it displayed sm options

Eric Rodriguez (Jun 24 2021 at 13:59):

can you send a screenshot of what you see?

Eric Wieser (Jun 24 2021 at 14:02):

Sai Gopal said:

what to do next ?

Assuming I read your earlier message correctly, you should follow the isntructions at https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/README.md#how-to-play

Sai Gopal (Jun 24 2021 at 14:03):

Capture.JPG

Eric Rodriguez (Jun 24 2021 at 14:05):

awesome, can you type in this in:

cd desktop
leanproject get ImperialCollegeLondon/formalising-mathematics
code formalising-mathematics

Sai Gopal (Jun 24 2021 at 14:10):

done

Eric Rodriguez (Jun 24 2021 at 14:13):

awesome! you should have something like this:
image.png

Eric Rodriguez (Jun 24 2021 at 14:13):

click on week_2 and Part_A_Groups.lean

Eric Rodriguez (Jun 24 2021 at 14:14):

that will get you started on the group tutorial

Eric Wieser (Jun 24 2021 at 14:19):

Note that this is a tutorial on "how to build groups in lean from scratch", and less about how to use the docs#group in mathlib.

Sai Gopal (Jun 24 2021 at 14:19):

2.JPG i got till here

Eric Wieser (Jun 24 2021 at 14:20):

Did you run that code command?

Eric Rodriguez (Jun 24 2021 at 14:20):

press enter! :b

Eric Rodriguez (Jun 24 2021 at 14:21):

Eric Wieser said:

Note that this is a tutorial on "how to build groups in lean from scratch", and less about how to use the docs#group in mathlib.

(was very helpful for understanding the group API, though, IMO)

Eric Wieser (Jun 24 2021 at 14:22):

Yes, the best answer to "how do I use this complex thing in a language I'm only just starting and haven't installed before" is probably "take a slightly more complex tutorial first", which in this case happens to be a tutorial about a similar thing to what you originally wanted!

Sai Gopal (Jun 24 2021 at 14:22):

@Eric Rodriguez @Eric Wieser Thank you for being so patient
finally im in

Adam Topaz (Jun 24 2021 at 14:24):

You may have to install the lean extension in vscode if you haven't done that already

Kevin Buzzard (Jun 24 2021 at 15:40):

Is there a way of putting that course repo up on gitpod?

Eric Wieser (Jun 24 2021 at 16:00):

I was just thinking that - but gitpod doesn't work with the lean extension right now due to the open-vsx server being down

Eric Wieser (Jun 24 2021 at 16:00):

Otherwise you can just copy the gitpod.yml from lean-liquid and all will work fine

Matthew Ballard (Jun 24 2021 at 16:04):

Eric Wieser said:

I was just thinking that - but gitpod doesn't work with the lean extension right now due to the open-vsx server being down

This is just for installation right?

Eric Wieser (Jun 24 2021 at 16:05):

Yes, but gitpod installs from scratch each time you open it

Eric Wieser (Jun 24 2021 at 16:05):

So we can set up gitpod right now, but no one will be able to use it until the server comes back up

Matthew Ballard (Jun 24 2021 at 16:05):

Even if you install the extension from vsix?

Eric Wieser (Jun 24 2021 at 16:06):

Where do you suggest getting the vsix from?

Eric Wieser (Jun 24 2021 at 16:07):

I mean yes you can probably build it yourself. Getting it from the visual studio marketplace supposedly violates Microsoft's ToS.

Matthew Ballard (Jun 24 2021 at 16:11):

Eric Wieser said:

I mean yes you can probably build it yourself. Getting it from the visual studio marketplace supposedly violates Microsoft's ToS.

I don't see that

Eric Wieser (Jun 24 2021 at 16:13):

I'm referencing https://www.gitpod.io/docs/vscode-extensions which says

Please note that .vsix files downloaded from the Visual Studio Marketplace should not be installed in Gitpod, because Microsoft prohibits the direct use of their marketplace by any non-Microsoft software, even though most extensions are actually open source and not developed or maintained by Microsoft.

Matthew Ballard (Jun 24 2021 at 16:14):

Ah.

Matthew Ballard (Jun 24 2021 at 16:19):

Offered without any guarantee of usability :)
lean-0.16.36.vsix

Matthew Ballard (Jun 24 2021 at 16:20):

(From source)

Matthew Ballard (Jun 24 2021 at 16:35):

And it looks like it is back up anyway.

Bryan Gin-ge Chen (Jun 24 2021 at 16:41):

(For what it's worth, the .vsix files are also available here)

Adam Topaz (Jun 24 2021 at 16:44):

I'm confused. How does the gitpod link on mathlib PRs work?

Adam Topaz (Jun 24 2021 at 16:46):

Oh nevermind. I understand now that gitpod uses the open-vsx server to get the open source extensions

Matthew Ballard (Jun 24 2021 at 16:50):

Nevermind. It looks like I lied. The vsix install currently gets overwritten by the open-vsx version.

Last updated: Dec 20 2023 at 11:08 UTC