gitpod with "mathematics in Lean"

Stream: new members

[Cris Perdue]

I'm starting to go through Mathematics in Lean using gitpod. The document says "If you click on the line, VS Code will show you Lean’s feedback in the Lean Goal window". I see an infoview window with messages. Is the Goal window different, and how do I see it (if so)??

[Arthur Paulino]

Oh, the "Lean Goal Window" is precisely the "Lean Infoview"

[Arthur Paulino]

If you place your cursor somewhere in between the begin and the end of a theorem you should see something like this:

α : Type
x : α
inst✝ : BEq α
l : NEList α
⊢ NEList.contains l x = true ↔ List.contains (NEList.toList l) x = true

[Cris Perdue]

Thanks much. Unfortunately I'm not getting anything like that.
Probably I need some import statements that I don't have.
Is there a tidy way to just reset all my state and start over?

[Arthur Paulino]

Can you send a screenshot of what you currently see?

[Cris Perdue]

Sure. I added some imports stolen from overview.lean and now things look a bit better. For a screenshot should I just attach the image file?

[Mario Carneiro]

Here's an example:

example (n : nat) : n < 1 + n :=
begin
  rw nat.add_comm,
end

If you put your cursor after the begin then the infoview should show the goal like this

1 goal
n: ℕ
⊢ n < 1 + n

and moving past the rw should change the 1 + n to n + 1

[Cris Perdue]

Screen-Shot-2022-04-05-at-16.16.16.png

[Mario Carneiro]

your cursor needs to be in a begin-end block to see the goal

[Mario Carneiro]

not the mouse cursor, the blinky line

[Mario Carneiro]

that picture looks like everything is working properly

[Arthur Paulino]

Oops, sorry. English is not my mother tongue. I think it's called caret cursor?

[Cris Perdue]

Yes, I am now getting the results you propose. Still I'm very uncomfortable fumbling around with VS Code.

[Arthur Paulino]

If you're more comfortable with Emacs or Neovim, there are tools to make those talk to the Lean server as well

[Cris Perdue]

Thank you both. I can use both Emacs and vi/vim, but Mathematics in Lean seems to assume VSCode.
Plus it's not clear how to connect Emacs or whatnot in the gitpod environment.
My Mac is M1-based and Lean is quite problematic in that environment.

[Cris Perdue]

Is there a way to undo all my changes to files in the VSCode workspace?

[Cris Perdue]

I mean Lean is problematic in an M1-based environment -- constantly runs out of memory.

[Arthur Paulino]

Ouch :/
Well, I'm not well-versed with VS Code either. I just use it with as a generic text editor with common ctrl+c ctrl+v etc shortcuts.

Maybe someone else will be able to help you further at this point

[Cris Perdue]

Ok, tnx!

[Julian Berman]

You should be able to be successful with an M1 (I use one), but indeed not everything is as seamless as it should/could be. Do feel free to ask any specific questions you have, someone should be able to help.

[Julian Berman]

Running out of memory shouldn't happen -- generally that means that your glossary#cache is missing -- but leanproject should have gotten you one if you followed the instructions from the README

[Julian Berman]

If you're still running into that specific issue let us know, we can try to diagnose it.

[Julian Berman]

(I think indeed you shouldn't try to use emacs within gitpod -- if you are going to do so, you want to follow the parts of the instructions that show you how to run mathematics_in_lean on your own computer)

[Alex J. Best]

@Cris Perdue if you are comfortable with git you can use that from the terminal within gitpod to revert your changes. There is also a vscode interface for git in the sidebar to make this less fiddly if you want to try that too

[Cris Perdue]

@Alex J. Best Thanks, Alex. After a few more minutes I did figure out that I can access git from the command line and it worked great. I will look in the sidebar now also.