Zulip Chat Archive

Stream: new members

Topic: getting started


view this post on Zulip Brandon Wu (May 07 2020 at 20:19):

hi there! i am very new to this, and i was having some difficulty with the installation / the overall setup of lean. right now i'm trying to use it in vscode with the extension, but I'm unsure as to exactly how lean operates - do I simply make a new file with some specified extension or is it more involved?

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:23):

You make a new project, as we desperately try to flag several times in the installation instructions

view this post on Zulip Kevin Buzzard (May 07 2020 at 20:23):

or you clone the tutorial project

view this post on Zulip Brandon Wu (May 07 2020 at 20:31):

my setup currently lives on my school's unix servers, so i sometimes run into trouble installing things - most recently ive been running into an error "/tmp/tmp.p0mYwop9QR/elan-init: /lib64/libc.so.6: version `GLIBC_2.18' not found (required by /tmp/tmp.p0mYwop9QR/elan-init)" when trying to install elan

view this post on Zulip Patrick Massot (May 07 2020 at 20:39):

That's a very bad omen.

view this post on Zulip Patrick Massot (May 07 2020 at 20:39):

What kind of Unix is that?

view this post on Zulip Reid Barton (May 07 2020 at 20:43):

sounds like one which is no longer as young as it once was

view this post on Zulip Reid Barton (May 07 2020 at 20:46):

"school's unix servers" is likely to be RHEL [some appallingly low number]

view this post on Zulip Brandon Wu (May 07 2020 at 20:53):

If it's relevant, I go to Carnegie Mellon and this is my school's Andrew server that I typically do all my work from. Is there no hope other than managing things locally, then?

view this post on Zulip Reid Barton (May 07 2020 at 20:58):

Well, if you already have the required build tools (cmake for Lean, the rust toolchain for elan) then it should be pretty easy to build your own binaries.

view this post on Zulip Reid Barton (May 07 2020 at 20:58):

Though I've never tried building elan

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:33):

Hi all, I am a number theorist and I have recently discovered some of Kevin Buzzard's talks. I have downloaded Lean, played with the natural number game and done some of Patrick Massot's exercises... I wonder where to go now to learn/play/do stuff. For instance, how could I check if basic results about group theory are there (e.g. : finite group of order p^2 is abelian, or "quotient by the centre is cyclic==> group is abelian), or how/where can I try to prove them? Many thanks!

view this post on Zulip Jalex Stark (May 08 2020 at 14:35):

doing exercises on codewars is a nice way to learn things

view this post on Zulip Jalex Stark (May 08 2020 at 14:36):

you can answer some of your questions by navigating in mathlib to the group_theory folder

view this post on Zulip Jalex Stark (May 08 2020 at 14:37):

either by using the html docs or in your own VSCode project by going to the "target" folder

view this post on Zulip Jalex Stark (May 08 2020 at 14:38):

i guess you can also read the code on github directly

view this post on Zulip Johan Commelin (May 08 2020 at 14:40):

@Filippo A. E. Nuccio Welcome! Do you have a working Lean setup on your own computer?

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:40):

Yes, I do. And thanks for the welcome.

view this post on Zulip Johan Commelin (May 08 2020 at 14:40):

Once you want to do something serious, the online web editors no longer are good enough

view this post on Zulip Johan Commelin (May 08 2020 at 14:40):

Ok, great

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:41):

Jalex Stark said:

i guess you can also read the code on github directly

Thanks! I will try doing so, then. I have also tried to read a bit about "compatibility" with future/past version. Is it true that whatever we're doing in Lean 3 now will need to be redone from scratch in Lean 4?

view this post on Zulip Johan Commelin (May 08 2020 at 14:41):

In that case, I would follow the instructions for setting up a new project, add mathlib as dependency, and try to state some of your group theory lemmas

view this post on Zulip Johan Commelin (May 08 2020 at 14:42):

I don't think we'll have to redo things from scratch. But there will be some weeks where we have to solve a lot of technical porting issues.

view this post on Zulip Johan Commelin (May 08 2020 at 14:42):

Luckily we have some very good regex hackers in our community.

view this post on Zulip Mario Carneiro (May 08 2020 at 14:43):

Also I think the day is fast approaching that we get enough parser data from lean core to be able to do better than regex

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:44):

Ah ok, good news. I' ll try to set up a new project, although I have not found a documentation about "basics" of group theory (e.g. what's the name for its order?) I suspect it should be at the address suggested by Jalex Stark

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:44):

Thanks to both of you for your answers, I'll try my luck!

view this post on Zulip Johan Commelin (May 08 2020 at 14:47):

@Filippo A. E. Nuccio We just reuse card for the order. Note that you need to add [fintype G] to assume that your group is finite. And then fintype.card G gives you the order of the group.

view this post on Zulip Johan Commelin (May 08 2020 at 14:47):

If you have any arbitrary group... you need to deal with cardinals :sad:

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:49):

@Johan Commelin Thanks! This is precisely the kind of info I'd love to see written somewhere: where should I look exactly, rather than asking everything here? I feel a huge leap between solving Patrick's exercices and opening my project from scartch

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:50):

(it reminds me of the first time I tried to type a LaTeX document before discovering the Short Guide To LaTeX...)

view this post on Zulip Jalex Stark (May 08 2020 at 14:52):

asking here is not super expensive, and learning from answers here will give you intuitions on where to look

view this post on Zulip Jalex Stark (May 08 2020 at 14:53):

if you feel bad about using people's time, just commit to start answering questions once you know things :)

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:55):

Indeed, that was my problem. I feel a bit bad in asking stupid things like: where do I start from? As far as I know I should:
1) Create a new project, and import mathlib (this is OK)
2) Import "all" things which I suspect I might need to speak about finite groups: here I am already puzzled
3) Learn something about types/classes/structures...: no idea at all.

view this post on Zulip Jalex Stark (May 08 2020 at 14:57):

For your 3), I find myself skimming chapter 10 of TPiL every couple of weeks and understanding more of it in proportion to how much engineering I've done between readings

view this post on Zulip Bryan Gin-ge Chen (May 08 2020 at 14:57):

There isn't a great solution right now for 2), but see the very recent in-progress "mathematics in Lean" book: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/new.20Lean.20.2F.20mathlib.20tutorial

For 3), the standard source / reference for Lean is still "Theorem proving in Lean": https://leanprover.github.io/theorem_proving_in_lean/

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 14:58):

@Bryan Gin-ge Chen Thanks!

view this post on Zulip Bryan Gin-ge Chen (May 08 2020 at 15:00):

(TPiL is short for "Theorem Proving in Lean" around here, so my suggestion was essentially the same as Jalex's.)

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 15:01):

Another stupid question: is it normal that each time I create a new project, some 120 MB get downloaded? I played a bit creating projects and I realise I have used almost a GB for nothing. Not a big deal, per se, just seems a bit odd.

view this post on Zulip Bryan Gin-ge Chen (May 08 2020 at 15:04):

Yes, unfortunately. Most of that space is taken up by mathlib's .olean files, which are like the compiled version of the .lean files.

view this post on Zulip Nam (May 08 2020 at 15:05):

i'll add that Hitchhiker's Guide explains stuffs pretty well.

view this post on Zulip Bryan Gin-ge Chen (May 08 2020 at 15:06):

Yes, I like that book too. You can find it with the other course materials here: https://lean-forward.github.io/logical-verification/2020/index.html#material

view this post on Zulip Kevin Buzzard (May 08 2020 at 15:07):

@Filippo A. E. Nuccio here is some basic group theory being done in Lean: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/group/level01_extended.lean

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 15:07):

@Nam @Bryan Gin-ge Chen Ok, thanks. I'll have a look there.

view this post on Zulip Filippo A. E. Nuccio (May 08 2020 at 15:10):

@Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

view this post on Zulip Patrick Massot (May 08 2020 at 16:29):

Filippo A. E. Nuccio said:

Thanks! This is precisely the kind of info I'd love to see written somewhere: where should I look exactly, rather than asking everything here? I feel a huge leap between solving Patrick's exercices and opening my project from scartch

Maybe I should give more context in the tutorials README (I gave it here, but it's not on GitHub). Currently there is a steady stream of people who want to learn Lean for math. This is great but the self-teaching material that exists is not yet up to this task. As a kind of urgency plaster, I translated the exercises from my first year undergraduate course where I used Lean, simply adding a couple of tactics that allow more efficiency. The course was not about learning Lean, it was about learning how to write rigorous proofs. So it stops very far from the point where you can develop new maths in Lean, and it very carefully avoid painful points, like handling inclusion maps. I simply hoped it would keep people busy for some time, and teach useful stuff while we work on https://github.com/leanprover-community/mathematics_in_lean that should ultimately contain much more.

view this post on Zulip Kevin Buzzard (May 08 2020 at 16:41):

Filippo A. E. Nuccio said:

Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

The file I linked to imports other files from that project, so yes you'd be better off downloading the entire project. But nowadays I usually work within a local copy of mathlib.

view this post on Zulip Patrick Massot (May 08 2020 at 16:50):

Filippo A. E. Nuccio said:

Another stupid question: is it normal that each time I create a new project, some 120 MB get downloaded? I played a bit creating projects and I realise I have used almost a GB for nothing. Not a big deal, per se, just seems a bit odd.

This is not a stupid question at all. Each time you create a new project, you download mathlib, with its full git history. That's about 37Mo. Then, if you don't already have them, you download compiled mathlib files. After unpacking, this adds about 80 Mo. If you already have those compiled files they are not downloaded but they are copied to your new project folder, which now weights about 120 Mo. This makes sense when you have a couple of projects that depend on different versions of mathlib, that you want to update independently (mathlib moves really fast, and a mathlib update can break your project non-trivially). But it doesn't make sense if you simply want to play with creating Lean projects. There are ways to improve on this, but limited time resources to modify leanproject. The current workflow works nicely for serious users who have a handful of projects that need to be really independent, and for people who want to play with one toy project. So improving this is very low priority. But feel free to contribute if fixing this is important to you. This is much much easier than proving things.

view this post on Zulip Patrick Stevens (May 08 2020 at 18:11):

I'll try and address the git cloning thing in https://github.com/leanprover-community/mathlib-tools/pull/47 - it's a first draft but I am going to eat now

view this post on Zulip Filippo A. E. Nuccio (May 09 2020 at 13:01):

Kevin Buzzard said:

Filippo A. E. Nuccio said:

Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

The file I linked to imports other files from that project, so yes you'd be better off downloading the entire project. But nowadays I usually work within a local copy of mathlib.

Thanks!

view this post on Zulip Jalex Stark (May 09 2020 at 13:03):

people on this thread may like reading this community wiki page

view this post on Zulip Filippo A. E. Nuccio (May 09 2020 at 13:04):

Patrick Massot said:

Filippo A. E. Nuccio said:

Another stupid question: is it normal that each time I create a new project, some 120 MB get downloaded? I played a bit creating projects and I realise I have used almost a GB for nothing. Not a big deal, per se, just seems a bit odd.

This is not a stupid question at all. Each time you create a new project, you download mathlib, with its full git history. That's about 37Mo. Then, if you don't already have them, you download compiled mathlib files. After unpacking, this adds about 80 Mo. If you already have those compiled files they are not downloaded but they are copied to your new project folder, which now weights about 120 Mo. This makes sense when you have a couple of projects that depend on different versions of mathlib, that you want to update independently (mathlib moves really fast, and a mathlib update can break your project non-trivially). But it doesn't make sense if you simply want to play with creating Lean projects. There are ways to improve on this, but limited time resources to modify leanproject. The current workflow works nicely for serious users who have a handful of projects that need to be really independent, and for people who want to play with one toy project. So improving this is very low priority. But feel free to contribute if fixing this is important to you. This is much much easier than proving things.

Thanks, this makes everything much clearer. I now really need to start making my hands dirty with some proof, but I'll be back to the forum as soon as I have more questions or comments. I think that this issue of dowloading 120 MB really not crucial for the time being.

view this post on Zulip Patrick Massot (May 09 2020 at 13:52):

I'll try and address the git cloning thing in https://github.com/leanprover-community/mathlib-tools/pull/47 - it's a first draft but I am going to eat now

@Patrick Stevens what is the current status of that effort? I'm about to release version 0.0.6

view this post on Zulip Patrick Massot (May 09 2020 at 13:52):

Note that there is no problem releasing 0.0.7 in a couple of days if you are not ready.

view this post on Zulip Patrick Stevens (May 09 2020 at 14:15):

Sorry, I kind of forgot about it and it has some test failures I haven't explained - let me just have a quick look again

view this post on Zulip Patrick Stevens (May 09 2020 at 14:15):

Part of the problem is that it's been literally years since I coded in Python, so everything is hard again :P

view this post on Zulip Patrick Massot (May 09 2020 at 14:20):

I should have asked a more specific question. I didn't look at that PR yet because it was flagged as a draft, do you want me to look at it now?

view this post on Zulip Patrick Massot (May 09 2020 at 14:21):

Also you should probably rebase on master before doing anything else on your branch

view this post on Zulip Patrick Stevens (May 09 2020 at 14:29):

The current status is "tests are failing when I enable the new mode and I have no idea why". I just turned my new flag to default to "off" and now the only test that is failing is the one that asserts the new behaviour - so it's definitely my change that is broken - but I was hoping to finish this without having to work out how to run it locally

view this post on Zulip Patrick Stevens (May 09 2020 at 14:29):

In hindsight, quite an optimistic hope

view this post on Zulip Patrick Massot (May 09 2020 at 14:31):

The error message on Travis suggests you invented some feature of git python

view this post on Zulip Patrick Stevens (May 09 2020 at 14:32):

(fear not, I'll squash away all these ridiculous commits)

view this post on Zulip Patrick Massot (May 09 2020 at 14:33):

And also that you didn't rebase on master

view this post on Zulip Patrick Massot (May 09 2020 at 14:33):

But this is not a problem at all

view this post on Zulip Patrick Massot (May 09 2020 at 14:33):

This can wait

view this post on Zulip Patrick Massot (May 09 2020 at 14:33):

I'll release 0.0.6 now

view this post on Zulip Patrick Stevens (May 09 2020 at 14:33):

Not rebasing isn't a problem if I'm going to squash-merge anyway, right?

view this post on Zulip Patrick Stevens (May 09 2020 at 14:33):

Sure, go for it

view this post on Zulip Patrick Massot (May 09 2020 at 14:34):

Oh sorry, I didn't see your new commits.

view this post on Zulip Patrick Massot (May 09 2020 at 14:34):

Yes, we can clean up history before merging

view this post on Zulip Patrick Massot (May 09 2020 at 14:35):

My actual question is: why do you think you can pass the depth argument to Repo.clone_from like this?

view this post on Zulip Patrick Stevens (May 09 2020 at 14:37):

Its docstring contains the text " :param multi_options: See clone method", and the clone method's docstring contains the text

   :param multi_options: A list of Clone options that can be provided multiple times.  One
        option per list item which is passed exactly as specified to clone.
        For example ['--config core.filemode=false', '--config core.ignorecase',
                     '--recurse-submodule=repo1_path', '--recurse-submodule=repo2_path'

view this post on Zulip Patrick Stevens (May 09 2020 at 14:45):

Do you mind if I add "/venv" to the .gitignore? I'm finally seeing if I can run the thing myself

view this post on Zulip Patrick Massot (May 09 2020 at 15:06):

Python 3.8.0 (default, Dec  7 2019, 17:45:02)
Type 'copyright', 'credits' or 'license' for more information
IPython 7.12.0 -- An enhanced Interactive Python. Type '?' for help.

In [1]: from git import Repo

In [2]:  Repo.clone_from('https://github.com/leanprover-community/tutorials.git'
   ...: , 'test_target', ['--depth=1'])
---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
<ipython-input-2-e474310ae324> in <module>
----> 1 Repo.clone_from('https://github.com/leanprover-community/tutorials.git', 'test_target', ['--depth=1'])

~/.pyenv/versions/3.8.0/lib/python3.8/site-packages/git/repo/base.py in clone_from(cls, url, to_path, progress, env, multi_options, **kwargs)
   1015         if env is not None:
   1016             git.update_environment(**env)
-> 1017         return cls._clone(git, url, to_path, GitCmdObjectDB, progress, multi_options, **kwargs)
   1018
   1019     def archive(self, ostream, treeish=None, prefix=None, **kwargs):

~/.pyenv/versions/3.8.0/lib/python3.8/site-packages/git/repo/base.py in _clone(cls, git, url, path, odb_default_type, progress, multi_options, **kwargs)
    952                          v=True, universal_newlines=True, **add_progress(kwargs, git, progress))
    953         if progress:
--> 954             handle_process_output(proc, None, progress.new_message_handler(), finalize_process, decode_streams=False)
    955         else:
    956             (stdout, stderr) = proc.communicate()

AttributeError: 'list' object has no attribute 'new_message_handler'

view this post on Zulip Patrick Massot (May 09 2020 at 15:06):

This has nothing to do with leanproject, this is simply not how Repo.clone_from works (at least the version I have here).

view this post on Zulip Patrick Stevens (May 09 2020 at 15:07):

Patrick Massot said:

This has nothing to do with leanproject, this is simply not how Repo.clone_from works (at least the version I have here).

Sure, I understand the message; I simply followed what I thought were clear and simple instructions from the docstring :P but nothing is clear and simple when you haven't touched a language for years

view this post on Zulip Patrick Massot (May 09 2020 at 15:10):

No problem. I'm very happy when people want to contribute to leanproject, and there is no hurry at all. I released anyway since there was a critical bug since the appearance of an unfortunately named branch in the mathlib repository

view this post on Zulip Patrick Massot (May 09 2020 at 15:11):

And now I need to leave

view this post on Zulip Filippo A. E. Nuccio (May 12 2020 at 11:48):

Filippo A. E. Nuccio said:

Kevin Buzzard said:

Filippo A. E. Nuccio said:

Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

The file I linked to imports other files from that project, so yes you'd be better off downloading the entire project. But nowadays I usually work within a local copy of mathlib.

Thanks!

I am trying to play with the group_game, and I can prove something (for central elements, right and left cosets coincide) but I don't understand the definition of "central_subgroup". I am wondering what's the policy: is there a stream to discuss that project in particular, should I throw my question at everyone in the chat? And whom should I show my partial solution to see if it is correct, should I paste it here? Thanks

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:54):

Oh I didn't even write the central subgroup stuff, that was written by @Jason KY. who is probably very busy with exams right now.

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:54):

and I am very busy with marking them :-/

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:56):

But one thing I would definitely recommend is that if you have any questions about this then please don't ask them in this generic thread, start a new topic with title the group theory game or something. You are more likely to get answers that way. Put it in #maths if you like.

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:59):

Also, feel free to write your own questions and PR them (or just post working Lean code as "issues" if you don't have a clue about github). Both Jason and I are busy with other things right now but we should get back to this in June.

view this post on Zulip Filippo A. E. Nuccio (May 12 2020 at 12:01):

Kevin Buzzard said:

Oh I didn't even write the central subgroup stuff, that was written by Jason KY. who is probably very busy with exams right now.

Oh, thanks. Very clear, then. I'll do so and I will try to understand how to "PR" them.

view this post on Zulip Jason KY. (May 12 2020 at 12:19):

Hi, Filippo
I defined the center of a group G as the set of elements of G that commutes and then I defined it to be a subgroup by proving all the subgroup axioms.
To be honest, I'm not sure if this is a good way to define this myself, I still learning myself!

view this post on Zulip Filippo A. E. Nuccio (May 12 2020 at 12:20):

Jason KY. said:

Hi, Filippo
I defined the center of a group G as the set of elements of G that commutes and then I defined it to be a subgroup by proving all the subgroup axioms.
To be honest, I'm not sure if this is a good way to define this myself, I still learning myself!

I see; I have moved the discussion to maths/group theory game-> should we continue there?

view this post on Zulip edderiofer (May 12 2020 at 19:27):

I'm struggling with the Advanced Worlds; specifically, I'm trying to apply some theorem statements to existing hypotheses to get new hypotheses to work with, but I can't figure out the syntax.

view this post on Zulip Patrick Massot (May 12 2020 at 19:28):

#mwe?

view this post on Zulip Jalex Stark (May 12 2020 at 19:29):

Hey @edderiofer ! I guess you're playing the natural number game? if you search this chat you may find a lot of discussions relevant to your problems :)

view this post on Zulip Jalex Stark (May 12 2020 at 19:29):

If you have a more specific question, you can hit the "new topic" button, give it an appropriate title, and show us the code you're struggling with

view this post on Zulip edderiofer (May 12 2020 at 19:29):

For instance, in Advanced Multiplication World 4, I do the following:
induction c with d hd generalizing b, simp, intro h,
which is fine. Now I want to use eq_zero_or_eq_zero_of_mul_eq_zero to deduce from h that a = 0 ∨ b = 0, but I can't figure out the syntax for it; have g := mul_eq_zero_iff(h), throws an error.

view this post on Zulip Jalex Stark (May 12 2020 at 19:30):

We need code that compiles, so that we can run it locally and see the same things you're seeing

view this post on Zulip Jalex Stark (May 12 2020 at 19:30):

otherwise this is a big game of telephone where everybody loses

view this post on Zulip Jalex Stark (May 12 2020 at 19:31):

Did you read the error?

view this post on Zulip edderiofer (May 12 2020 at 19:32):

Yes, but I don't understand it.

view this post on Zulip Jalex Stark (May 12 2020 at 19:32):

The errors have lots of useful information in them

view this post on Zulip Jalex Stark (May 12 2020 at 19:32):

If you want help here, you'll have to produce a #mwe

view this post on Zulip edderiofer (May 12 2020 at 19:32):

On Advanced Multiplication World Level 4 of the Natural Number Game,
induction c with d hd generalizing b, simp, intro h, have g := mul_eq_zero_iff(h),
throws an error on the last line.

view this post on Zulip Jalex Stark (May 12 2020 at 19:32):

yes, I think you said all of that already

view this post on Zulip edderiofer (May 12 2020 at 19:33):

Then I'm not sure what you want from me.

view this post on Zulip Jalex Stark (May 12 2020 at 19:34):

you could either give us a #mwe or tell us what youre error message is, I think both of those would enable progress

view this post on Zulip Jalex Stark (May 12 2020 at 19:34):

(did you notice that #mwe is a link to a page with a description of what we want?)

view this post on Zulip edderiofer (May 12 2020 at 19:34):

I get the error:

type mismatch at application mul_eq_zero_iff h term h has type a * b = 0 : Prop but is expected to have type mynat : Type state: 2 goals a : mynat, ha : a ≠ 0, b : mynat, h : a * b = 0 ⊢ b = 0

case mynat.succ a : mynat, ha : a ≠ 0, d : mynat, hd : ∀ (b : mynat), a * b = a * d → b = d, b : mynat ⊢ a * b = a * succ d → b = succ d

view this post on Zulip Jalex Stark (May 12 2020 at 19:35):

mul_eq_zero_iff is a function of several arguments, the first of which is a nat

view this post on Zulip Jalex Stark (May 12 2020 at 19:35):

try mul_eq_zero_iff _ _ h

view this post on Zulip edderiofer (May 12 2020 at 19:36):

That gets me this error:

function expected at
  mul_eq_zero_iff ?m_1 ?m_2
term has type
  ?m_1 * ?m_2 = 0  ?m_1 = 0  ?m_2 = 0
state:
2 goals
a : mynat,
ha : a  0,
b : mynat,
h : a * b = 0
 b = 0

case mynat.succ
a : mynat,
ha : a  0,
d : mynat,
hd :  (b : mynat), a * b = a * d  b = d,
b : mynat
 a * b = a * succ d  b = succ d

view this post on Zulip Jalex Stark (May 12 2020 at 19:37):

from this part of the error function expected at mul_eq_zero_iff ?m_1 ?m_2 you can see that it wants exactly two arguments

view this post on Zulip Jalex Stark (May 12 2020 at 19:37):

so try one fewer underscore

view this post on Zulip edderiofer (May 12 2020 at 19:38):

have g := mul_eq_zero_iff _ h, gets me this error:

type mismatch at application
  mul_eq_zero_iff ?m_1 h
term
  h
has type
  a * b = 0 : Prop
but is expected to have type
  mynat : Type
state:
2 goals
a : mynat,
ha : a  0,
b : mynat,
h : a * b = 0
 b = 0

case mynat.succ
a : mynat,
ha : a  0,
d : mynat,
hd :  (b : mynat), a * b = a * d  b = d,
b : mynat
 a * b = a * succ d  b = succ d

view this post on Zulip Jalex Stark (May 12 2020 at 19:39):

What do you think this part of the error means?

term
  h
has type
  a * b = 0 : Prop
but is expected to have type
  mynat : Type

view this post on Zulip edderiofer (May 12 2020 at 19:40):

That I need a second mynat as the second input.

view this post on Zulip edderiofer (May 12 2020 at 19:41):

have g := mul_eq_zero_iff _ _, compiles, but gives me this set of goals:

4 goals
a : mynat,
ha : a  0,
b : mynat,
h : a * b = 0,
g : ?m_1 * ?m_2 = 0  ?m_1 = 0  ?m_2 = 0
 b = 0

a : mynat,
ha : a  0,
b : mynat,
h : a * b = 0
 mynat

a : mynat,
ha : a  0,
b : mynat,
h : a * b = 0
 mynat

case mynat.succ
a : mynat,
ha : a  0,
d : mynat,
hd :  (b : mynat), a * b = a * d  b = d,
b : mynat
 a * b = a * succ d  b = succ d

which isn't what I wanted.

view this post on Zulip Jalex Stark (May 12 2020 at 19:41):

right, I think you should figure out which specific mynats to fill in the underscores with

view this post on Zulip Jalex Stark (May 12 2020 at 19:42):

(it's probably a and b in some order)

view this post on Zulip Patrick Massot (May 12 2020 at 19:44):

Jalex, you're not helping by keeping answering without a #mwe

view this post on Zulip Patrick Massot (May 12 2020 at 19:45):

You know that, in the long run, you're not helping him or her.

view this post on Zulip Jalex Stark (May 12 2020 at 19:45):

I could stop replying, yeah; I guess my fear is that they'll give up on the natural number game

view this post on Zulip Jalex Stark (May 12 2020 at 19:45):

really my goal is to try to understand why people don't respond gracefully to requests for a #mwe

view this post on Zulip Jalex Stark (May 12 2020 at 19:46):

i don't have a very good model of what's going on in their head

view this post on Zulip Jalex Stark (May 12 2020 at 19:46):

but also like, I think it is interesting to have discussions with new people about how to read error messages

view this post on Zulip Jalex Stark (May 12 2020 at 19:47):

maybe we need a natural number game stream to insulate the rest of the server from specificall this sort of interaction

view this post on Zulip edderiofer (May 12 2020 at 19:48):

In my case, I'm not sure how the description I gave:

On Advanced Multiplication World Level 4 of the Natural Number Game,
induction c with d hd generalizing b, simp, intro h, have g := mul_eq_zero_iff(h),
throws an error on the last line.

doesn't constitute a MWE (or in this case, a MN-WE).

view this post on Zulip Jalex Stark (May 12 2020 at 19:49):

did you read the definition at the link?

view this post on Zulip Jalex Stark (May 12 2020 at 19:49):

for us, a #mwe is something that we can copy-paste into a local Lean instance

view this post on Zulip edderiofer (May 12 2020 at 19:50):

OK, but how do I get the list of imports if I'm playing the Natural Number Game?

view this post on Zulip Jalex Stark (May 12 2020 at 19:51):

(and yeah, "working" is a strange word, for us it means "throws the error that i'm interested in getting help with")

view this post on Zulip Jalex Stark (May 12 2020 at 19:51):

you could start by including the theorem statement

view this post on Zulip Jalex Stark (May 12 2020 at 19:52):

I can add some guidance to that link about the natural number game

view this post on Zulip edderiofer (May 12 2020 at 19:52):

That would definitely be helpful.

view this post on Zulip Jalex Stark (May 12 2020 at 19:52):

okay so what happens if you try to post the theorem statement and your proof script?

view this post on Zulip Jalex Stark (May 12 2020 at 19:53):

I think it's ~40% likely that if I copy it into my local instance, it will just work, since a lot of the natural number definitions are in core

view this post on Zulip ROCKY KAMEN-RUBIO (May 12 2020 at 19:53):

@edderiofer When we say an MWE (Minimum Working Example), we mean something we can copy and paste directly into a local Lean compiler and get the same result. It may not be obvious how to do this if Natural Number Game has been your only exposure to lean. For example, the following does not work because it's just a series of tactics.

induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff(h),

This does count, because I've included the theorem statement and imports (notice that I'm using nat instead of mynat, which is specific to NNG).

import data.nat.basic
theorem mul_left_cancel (a b c : nat) (ha : a  0) : a * b = a * c  b = c :=
begin
induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff(h),
end

view this post on Zulip Jalex Stark (May 12 2020 at 19:54):

@ROCKY KAMEN-RUBIO you're missing import tactic

view this post on Zulip ROCKY KAMEN-RUBIO (May 12 2020 at 19:55):

Thanks!

view this post on Zulip Patrick Massot (May 12 2020 at 19:55):

The case of the NNG is the easiest actually: you can copy-paste the url, eg http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=7&level=1

view this post on Zulip edderiofer (May 12 2020 at 19:55):

The following works (on https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=9&level=4):

theorem mul_left_cancel (a b c : mynat) (ha : a  0) : a * b = a * c  b = c :=
begin
induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff a b,
rwa g at h,

but is there a quicker way to perform the last two lines to go from h : a * b = 0 to h : a = 0 ∨ b = 0?

view this post on Zulip ROCKY KAMEN-RUBIO (May 12 2020 at 19:55):

Jalex Stark said:

ROCKY KAMEN-RUBIO you're missing import tactic

import data.nat.basic
import tactic
theorem mul_left_cancel (a b c : nat) (ha : a  0) : a * b = a * c  b = c :=
begin
induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff(h),
end

view this post on Zulip Patrick Massot (May 12 2020 at 19:55):

Jalex, I think it would be good idea to mention this url "trick" in the #mwe webpage

view this post on Zulip Jalex Stark (May 12 2020 at 19:55):

you could do rwa mul_eq_zero_iff a b at h,

view this post on Zulip Jalex Stark (May 12 2020 at 19:56):

and then in fact if you replace the a and b with underscores it should figure it out for you

view this post on Zulip edderiofer (May 12 2020 at 19:56):

Ah, OK.

view this post on Zulip Jalex Stark (May 12 2020 at 19:57):

thanks for the patience here, we really want to help new people and avoid burnout, so we want to make processes to make helping new people more efficient

view this post on Zulip edderiofer (May 12 2020 at 19:58):

What if the theorem I wanted to use was a single-direction implication? You can't use rw then, can you?

view this post on Zulip Jalex Stark (May 12 2020 at 19:59):

then you want apply

view this post on Zulip Jalex Stark (May 12 2020 at 20:00):

well, apply f works if f : A \to B and B is the goal

view this post on Zulip ROCKY KAMEN-RUBIO (May 12 2020 at 20:00):

@edderiofer This might seem like a silly distinction, but getting in the habit of doing this really does speed up the process of assessing errors when your questions get more complex. It's totally understandable if you're confused this early on. Keep at it, and keep asking questions if you get stuck!

view this post on Zulip Jalex Stark (May 12 2020 at 20:00):

sometimes I do find myself using a lemma to generate an equality and then rwing that equality

view this post on Zulip Patrick Massot (May 12 2020 at 20:01):

I don't know what is explained in the game at this point, but the normal way to write this beginning of proof would be:

induction c with d hd generalizing b,
simp,
intro h,
cases (mul_eq_zero_iff a b).mp h with ha' hb,

or, even better,

induction c with d hd generalizing b,
simp,
intro h,
exact or.resolve_left ((mul_eq_zero_iff a b).mp h) ha,

view this post on Zulip Jalex Stark (May 12 2020 at 20:02):

where "normal" means "mathlib-approved"?

view this post on Zulip Patrick Massot (May 12 2020 at 20:02):

efficiency approved

view this post on Zulip ROCKY KAMEN-RUBIO (May 12 2020 at 20:02):

Jalex Stark said:

sometimes I do find myself using a lemma to generate an equality and then rwing that equality

Technically I think NNG doesn't let you define external lemmas outside of the current tactic proof, so you would have to use a have statement or something.

view this post on Zulip edderiofer (May 12 2020 at 20:03):

I don't think .mp is explained in the game at this point?

view this post on Zulip Jalex Stark (May 12 2020 at 20:03):

yes when i said "lemma" I did mean "add somethign new to the local context with have" not "define something with the lemma keyword"

view this post on Zulip Patrick Massot (May 12 2020 at 20:03):

I have no idea what is explained here. I'm too old. I started Lean long before this game was written

view this post on Zulip Jalex Stark (May 12 2020 at 20:04):

I agree that NNG does not want you to use .mp

view this post on Zulip Jalex Stark (May 12 2020 at 20:04):

I learned about .mp by using Lean in VSCode and having it pop out of suggest or library_search sometimes

view this post on Zulip ROCKY KAMEN-RUBIO (May 12 2020 at 20:04):

Jalex Stark said:

yes when i said "lemma" I did mean "add somethign new to the local context with have" not "define something with the lemma keyword"

Cool, just wanted to make that distinction because of the keyword lemma.

view this post on Zulip Jalex Stark (May 12 2020 at 20:05):

Patrick, is adding a local hypothesis and using rw really much less efficient than the term mode proof?

view this post on Zulip Jalex Stark (May 12 2020 at 20:05):

I guess in my mind the only time to care about that much efficiency is if you're putting code into mathlib

view this post on Zulip Jalex Stark (May 12 2020 at 20:05):

but maybe I am wrong

view this post on Zulip Patrick Massot (May 12 2020 at 20:06):

I mostly meant efficiency in writing speed.

view this post on Zulip Jalex Stark (May 12 2020 at 20:07):

well that's definitely not true if I'm the one writing :P

view this post on Zulip Patrick Massot (May 12 2020 at 20:07):

I also have another constraint from my teaching use of Lean. The ultimate goal of my course is to teach traditional math writing. Lean is only an intermediate tool. Hence I prefer having only one line of Lean for one sentence on paper. Here you would say: ab = 0 and a neq 0 hence b=0, matching the number of lines of my efficient proof.

view this post on Zulip Jalex Stark (May 12 2020 at 20:07):

interesting

view this post on Zulip Jalex Stark (May 12 2020 at 20:08):

Kevin writes a lot of "literate lean" where he uses multiple lines of Lean for one line of math

view this post on Zulip Patrick Massot (May 12 2020 at 20:08):

But on that example, I would not expect my students to write this line, this is too advanced term mode.

view this post on Zulip Jalex Stark (May 12 2020 at 20:09):

ah okay

view this post on Zulip Jalex Stark (May 12 2020 at 20:09):

making the math proof move slower seems better than making the lean move faster, for the purpose of teaching first-years

view this post on Zulip Jalex Stark (May 12 2020 at 20:10):

I guess most people here (including @edderiofer) are coming form the perspective of already being fluent in "terse" mathematical sentences

view this post on Zulip Jalex Stark (May 12 2020 at 20:11):

I made a small edit to the #mwe page. @edderiofer do you think the current state of the page would have caused you to post a link?

view this post on Zulip edderiofer (May 12 2020 at 20:12):

If "Natural Number Game" were capitalized, definitely.

view this post on Zulip Jalex Stark (May 12 2020 at 20:16):

haha thanks, fixing that now

view this post on Zulip Jalex Stark (May 12 2020 at 20:19):

okay, I added a fairly explicit example to #mwe

view this post on Zulip edderiofer (May 12 2020 at 20:20):

Yep, that works.

view this post on Zulip Jalex Stark (May 12 2020 at 20:21):

edderiofer, I think i recognize your name from /r/math and /r/mathriddles ? Have you seen this pair of riddle and Codewars question?
and this other pair, where the translation was in the other direction?

view this post on Zulip Mario Carneiro (May 12 2020 at 20:22):

Regarding #mwe generation, it would be nice if NNG had a "MWE button" that takes the user's text together with the surrounding theorem and the imports and puts it in your clipboard. Since this has to be what is being sent to lean this should not be too difficult

view this post on Zulip Mario Carneiro (May 12 2020 at 20:23):

it's still not perfect because of the mynat issue, but it should be enough for the cognoscenti

view this post on Zulip edderiofer (May 12 2020 at 20:24):

No, I haven't seen either of those pairs, but yes, you probably do recognize me from there.

view this post on Zulip Jalex Stark (May 12 2020 at 20:27):

cool, I am khanh93 on reddit, though I post a lot less so you may not recognize me

view this post on Zulip edderiofer (May 12 2020 at 20:30):

Yep, definitely don't recognize that username.

view this post on Zulip edderiofer (May 12 2020 at 20:31):

So who's going to post the MWE button feature request to GitHub?

view this post on Zulip Jalex Stark (May 12 2020 at 20:31):

well I think the biggest problem is that we don't have anyone doing active development on the NNG engine :(

view this post on Zulip Jalex Stark (May 12 2020 at 20:32):

though I guess the github project is a great place to store these desiderata

view this post on Zulip Jalex Stark (May 12 2020 at 20:32):

I think this project is the relevant one
https://github.com/mpedramfar/Lean-game-maker

view this post on Zulip Bryan Gin-ge Chen (May 12 2020 at 20:32):

The person to ping is @Mohammad Pedramfar, I think. Unless he's said he's taking a step back from development.

view this post on Zulip edderiofer (May 12 2020 at 20:32):

I thought it was this one? https://github.com/ImperialCollegeLondon/natural_number_game

view this post on Zulip Jalex Stark (May 12 2020 at 20:33):

I think, though obviously mohammad is the best person to comment, that the latter project is for the content of the game levels and the former is for the engine

view this post on Zulip edderiofer (May 12 2020 at 20:34):

Ah, OK. Well, I'm still stuck on this level, so I think I'll just go off and make food now.

view this post on Zulip Jalex Stark (May 12 2020 at 20:34):

(I'm hoping "stuck" means "still trying to think of a new idea" and not "there was a question I asked that didn't receive any attention, because everyone was talking about the meta problem of how to phrase the question")

view this post on Zulip edderiofer (May 12 2020 at 20:42):

Still trying to think of a new idea.

view this post on Zulip Mohammad Pedramfar (May 12 2020 at 20:51):

Jalex Stark said:

well I think the biggest problem is that we don't have anyone doing active development on the NNG engine :(

The latest commit was 5 days ago! :(
Is there any issue with the game? Or do you want some extra features?

view this post on Zulip edderiofer (May 12 2020 at 20:52):

Hmm. If I could prove that a is the successor of some number, since it's nonzero, this would be a lot easier, I think?

view this post on Zulip Jalex Stark (May 12 2020 at 20:53):

Mohammad Pedramfar said:

Jalex Stark said:

well I think the biggest problem is that we don't have anyone doing active development on the NNG engine :(

The latest commit was 5 days ago! :(
Is there any issue with the game? Or do you want some extra features?

hah, sorry! I was not following closely enough. Now I remember that you recently made it so that progress is saved! I think the work you're doing is very valuable :)

view this post on Zulip Jalex Stark (May 12 2020 at 20:53):

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

view this post on Zulip Jalex Stark (May 12 2020 at 20:53):

edderiofer said:

Hmm. If I could prove that a is the successor of some number, since it's nonzero, this would be a lot easier, I think?

try cases a

view this post on Zulip Jalex Stark (May 12 2020 at 20:55):

Jalex Stark said:

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

so it would have the URL of the current level plus the current proof script, and I guess also the statement of the theorem so that people who don't click the link can follow the discussion

view this post on Zulip edderiofer (May 12 2020 at 20:56):

Oh, right, I misread what cases a does in this case.

view this post on Zulip edderiofer (May 12 2020 at 20:56):

Is there a quick way to comment out a line?

view this post on Zulip Mario Carneiro (May 12 2020 at 20:56):

-- comment

view this post on Zulip Bryan Gin-ge Chen (May 12 2020 at 20:57):

ctrl+/ (or cmd+/ if you're on macOS) should be the keybind for line comment.

view this post on Zulip Jalex Stark (May 12 2020 at 20:57):

that's in VSCode, I think in the NNG you just have to type the comment character

view this post on Zulip Jalex Stark (May 12 2020 at 20:58):

there's also block comments

/-
like this
-/

view this post on Zulip Bryan Gin-ge Chen (May 12 2020 at 21:00):

Jalex Stark said:

that's in VSCode, I think in the NNG you just have to type the comment character

Oh, you're right. For some reason I thought the web editors supported it too.

view this post on Zulip Jalex Stark (May 12 2020 at 21:02):

a lot of web editors have the same keybinding

view this post on Zulip Jalex Stark (May 12 2020 at 21:02):

I use cmd-/ in jupyter and overleaf

view this post on Zulip edderiofer (May 12 2020 at 21:02):

How do I flip an equality? If I have a * b = 0 as a hypothesis, how do I turn it into 0 = a * b?

view this post on Zulip Jalex Stark (May 12 2020 at 21:03):

symmetry at h

view this post on Zulip edderiofer (May 12 2020 at 21:04):

Thanks.

view this post on Zulip Jalex Stark (May 12 2020 at 21:04):

btw it's better for the server if we have new questions in new topics.

view this post on Zulip Jalex Stark (May 12 2020 at 21:04):

mostly so that people later can read old conversations

view this post on Zulip edderiofer (May 12 2020 at 21:06):

Ah, alright.

view this post on Zulip Mohammad Pedramfar (May 12 2020 at 21:22):

Mario Carneiro said:

Regarding #mwe generation, it would be nice if NNG had a "MWE button" that takes the user's text together with the surrounding theorem and the imports and puts it in your clipboard. Since this has to be what is being sent to lean this should not be too difficult

The things that are sent to the Lean server are not limited to what can be seen on the screen. There could be hidden lines. And several of the tactics used in the NNG are redefined to work slightly differently. So it won't really be a minimal working example. It generally won't work. It would need the imports and everything.

view this post on Zulip Mohammad Pedramfar (May 12 2020 at 21:28):

Jalex Stark said:

Jalex Stark said:

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

so it would have the URL of the current level plus the current proof script, and I guess also the statement of the theorem so that people who don't click the link can follow the discussion

That's doable, but it will only be useful for Zulip. The user won't be able to actually run the text that's copied into the clipboard. Wouldn't it be confusing for the users who don't use Zulip?

view this post on Zulip Kevin Buzzard (May 12 2020 at 21:32):

@edderiofer did you get the answer to your question? I've only just arrived.

view this post on Zulip edderiofer (May 12 2020 at 21:42):

Which of my many questions? :P

(Yes.)

view this post on Zulip Mario Carneiro (May 12 2020 at 21:46):

Mohammad Pedramfar said:

The things that are sent to the Lean server are not limited to what can be seen on the screen. There could be hidden lines. And several of the tactics used in the NNG are redefined to work slightly differently. So it won't really be a minimal working example. It generally won't work. It would need the imports and everything.

I know. Unless there is a good reason to hide them (e.g. if the solution is in there), I'm thinking everything in the level file, including any hidden lines, but not the entirety of NNG.

view this post on Zulip Jalex Stark (May 12 2020 at 21:46):

Mohammad Pedramfar said:

Jalex Stark said:

Jalex Stark said:

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

so it would have the URL of the current level plus the current proof script, and I guess also the statement of the theorem so that people who don't click the link can follow the discussion

That's doable, but it will only be useful for Zulip. The user won't be able to actually run the text that's copied into the clipboard. Wouldn't it be confusing for the users who don't use Zulip?

hah, I guess around here we have some kind of bias towards zulip users :)
The text that comes out is pretty close to working, which is plenty good if you're using it to talk to people, but maybe is disheartening if you're working on your own. I agree that it's not clear whether there's a version of this that's useful on average over all users.

view this post on Zulip Mario Carneiro (May 12 2020 at 21:47):

So there is the possibility that it's not a perfect MWE but it should get close enough for people to get the gist

view this post on Zulip Jalex Stark (May 12 2020 at 21:47):

Mario Carneiro said:

So there is the possibility that it's not a perfect MWE but it should get close enough for people to get the gist

unless the people are not yet good at reading error messages

view this post on Zulip Mario Carneiro (May 12 2020 at 21:48):

I think if you want a faithful version of NNG offline you can download the repo and use vscode

view this post on Zulip Jalex Stark (May 12 2020 at 21:49):

oh yeah I forgot that is a thing

view this post on Zulip Kenny Lau (May 12 2020 at 21:49):

why can't we just use the NNG website?

view this post on Zulip Mario Carneiro (May 12 2020 at 21:49):

but my goal here is to improve the state of affairs over

induction b, apply h1 h2
it doesn't work

view this post on Zulip Jalex Stark (May 12 2020 at 21:50):

well I think the goal is to make it so that first time posters are more likely to post a complete thing

view this post on Zulip Jalex Stark (May 12 2020 at 21:50):

having them link us to the NNG website is good

view this post on Zulip Mario Carneiro (May 12 2020 at 21:51):

it also requires me to load a link, which may be more or less complicated if I'm on a phone or something

view this post on Zulip Mario Carneiro (May 12 2020 at 21:51):

having inline code is good

view this post on Zulip Mario Carneiro (May 12 2020 at 21:52):

but when people type text into NNG all the context is gone. I want some bare minimum of context to understand the question. I have no idea what world 4 level 7 is

view this post on Zulip Reid Barton (May 12 2020 at 21:56):

I think it'd be more useful to have the NNG website give the user a link to the level they're solving with their code filled in

view this post on Zulip Reid Barton (May 12 2020 at 21:57):

Then you get more of the true context (including whatever the level is supposed to be teaching, etc)

view this post on Zulip Kevin Buzzard (May 12 2020 at 21:57):

@Jalex Stark while you're here, I pushed a new version of NNG recently, and now I have a FAQ and thanks to Mohammad, save game functionality. You seemed to have some very clear visions for what this game should look like and we recently had a conversation about it; I am hoping I dealt with some of your comments in v1.3.2 but I'd be very happy to hear if you still had more.

view this post on Zulip Kevin Buzzard (May 12 2020 at 21:58):

@Mario Carneiro as of recently we can actually link directly to that level (this is new as of about last week), so it will be much easier in the future. I don't have any idea either, and when I look in the source code the worlds are called different things to what the users call them which makes life even worse :-)

view this post on Zulip Kevin Buzzard (May 12 2020 at 21:58):

Not only that, remember that I am using a modified rw, induction, cases etc, so these things are actually perhaps not appropriate for mwes in the traditional sense.

view this post on Zulip Mario Carneiro (May 12 2020 at 21:59):

My main complaint is about "raw" tactic scripts. Even if it doesn't run, seeing theorem foo : ... at the start makes things a lot easier

view this post on Zulip Jalex Stark (May 12 2020 at 21:59):

Kevin Buzzard said:

Mario Carneiro as of recently we can actually link directly to that level (this is new as of about last week), so it will be much easier in the future. I don't have any idea either, and when I look in the source code the worlds are called different things to what the users call them which makes life even worse :-)

We added some text to the #mwe page telling people to use level links when they post in zulip chat :)
(I'll think a bit on your other question.)

view this post on Zulip Reid Barton (May 12 2020 at 22:02):

I think there are weird features or hacks you can use to cause some surrounding text to be included if the user copies their text, but not sure if advisable

view this post on Zulip Mohammad Pedramfar (May 12 2020 at 22:30):

An idea I had was to put the theorem statements into the editor together with the proof, but make the first and the last line read-only. So the user can't edit the statement, but when they want to copy, they can select all of it. Unfortunately, monaco-editor, which is used in the NNG and other places with Lean on the web, doesn't have this option. One way to go around it would be to use another text editor, like Ace editor, which has this function. But that seems to be very difficult. I would need to redefine the Lean syntax and autocompletion and highlighting and everything for a new editor. Besides, this seems to be the only way Ace editor is better. Monaco editor is the web-based version of VS code, which is why things work so well.

view this post on Zulip Reid Barton (May 12 2020 at 22:32):

Maybe just have a button which has the effect of copying the user's text together with the surrounding statement/tactic?

view this post on Zulip Bryan Gin-ge Chen (May 12 2020 at 22:32):

I wrote some Lean integration for CodeMirror for my Observable notebooks which I could try to extract if there's interest.

view this post on Zulip Mohammad Pedramfar (May 12 2020 at 22:37):

Reid Barton said:

Maybe just have a button which has the effect of copying the user's text together with the surrounding statement/tactic?

Yeah, I'm starting to think adding a button that would copy the content and the statement would be the most efficient way. The main page of NNG has a link to a FAQ page describing why Lean is different than the NNG, so I guess it wouldn't be that confusing for a user when they see it doesn't work.

view this post on Zulip Mohammad Pedramfar (May 12 2020 at 22:39):

Bryan Gin-ge Chen said:

I wrote some Lean integration for CodeMirror for my Observable notebooks which I could try to extract if there's interest.

That might be useful, but I'll go with the simpler approach this time. :)
It's on github, right? Why didn't you use monaco-editor?

view this post on Zulip Bryan Gin-ge Chen (May 12 2020 at 22:52):

It's on github, right? Why didn't you use monaco-editor?

Yes, CodeMirror is on github. I remember thinking that monaco would be too heavy-weight (in terms of file-size) to include, and it also looked to be a lot of work to bundle it properly for my use-case. In the end it wasn't too hard to write a Lean integration for CodeMirror following what was already done for monaco in the lean-web-editor, since the CodeMirror API is fairly simple.

view this post on Zulip Mohammad Pedramfar (May 13 2020 at 00:59):

That's good to know. My impression was that it would be difficult to use another editor.

view this post on Zulip Mohammad Pedramfar (May 22 2020 at 21:14):

I forgot to mention it here. The button is added in the Lean-game-maker repo. It will be there in the next update of the game. It took a while since I was fixing a few bugs.


Last updated: May 12 2021 at 22:15 UTC