macOS installation

Stream: lean4

[josedeodo]

I suppose that I have installed lean4,but when I type source ~/.bash_profile in the terminal, it shows that no such file or directory.so how can I deal with it?

[Notification Bot]

josedeodo has marked this topic as resolved.

[Alexander Kurz]

Hi, I am new to lean. I followed the instructions at https://leanprover-community.github.io/install/macos_details.html for lean4 in vscode. I created a file test.lean which contains one line #eval 1+1 . The instructions say "A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." but there is no green line. Instead the #eval is underlined with a blue curly line. Any ideas what I could try?

[josedeodo]

Alexander Kurz 发言道：

Hi, I am new to lean. I followed the instructions at https://leanprover-community.github.io/install/macos_details.html for lean4 in vscode. I created a file test.lean which contains one line #eval 1+1 . The instructions say "A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." but there is no green line. Instead the #eval is underlined with a blue curly line. Any ideas what I could try?

Nice to meet you.I just type in the terminal "/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile".and it woks ,but I do not know how to do next.Maybe you could try this way?

[Alexander Kurz]

josedeodo said:

Alexander Kurz 发言道：

Hi, I am new to lean. I followed the instructions at https://leanprover-community.github.io/install/macos_details.html for lean4 in vscode. I created a file test.lean which contains one line #eval 1+1 . The instructions say "A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." but there is no green line. Instead the #eval is underlined with a blue curly line. Any ideas what I could try?

Nice to meet you.I just type in the terminal "/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile".and it woks ,but I do not know how to do next.Maybe you could try this way?

Thanks. But I am not sure what your advice is. Do you suggest that I install lean again using the curl command?

[josedeodo]

Alexander Kurz 发言道：

josedeodo said:

Alexander Kurz 发言道：

Hi, I am new to lean. I followed the instructions at https://leanprover-community.github.io/install/macos_details.html for lean4 in vscode. I created a file test.lean which contains one line #eval 1+1 . The instructions say "A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." but there is no green line. Instead the #eval is underlined with a blue curly line. Any ideas what I could try?

Nice to meet you.I just type in the terminal "/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile".and it woks ,but I do not know how to do next.Maybe you could try this way?

Thanks. But I am not sure what your advice is. Do you suggest that I install lean again using the curl command?

yes.try it?

[Notification Bot]

josedeodo has marked this topic as unresolved.

[josedeodo]

josedeodo 发言道：

Alexander Kurz 发言道：

josedeodo said:

Alexander Kurz 发言道：

Hi, I am new to lean. I followed the instructions at https://leanprover-community.github.io/install/macos_details.html for lean4 in vscode. I created a file test.lean which contains one line #eval 1+1 . The instructions say "A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." but there is no green line. Instead the #eval is underlined with a blue curly line. Any ideas what I could try?

Nice to meet you.I just type in the terminal "/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile".and it woks ,but I do not know how to do next.Maybe you could try this way?

Thanks. But I am not sure what your advice is. Do you suggest that I install lean again using the curl command?

yes.try it?

but I have not address my own problem.my English is so poor///

[Chris Wong]

Alexander Kurz said:

... The instructions say "A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." but there is no green line. Instead the #eval is underlined with a blue curly line. Any ideas what I could try?

What does the tooltip say when you hover over it?
It could be that the blue curly line is the right behavior now, and the instructions are just out of date.

[Notification Bot]

ming has marked this topic as resolved.

[Notification Bot]

ming has marked this topic as unresolved.

[Yaël Dillies]

Green and blue are supposed to be the same, yeah.

[Alexander Kurz]

Chris Wong said:

Alexander Kurz said:

... The instructions say "A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." but there is no green line. Instead the #eval is underlined with a blue curly line. Any ideas what I could try?

What does the tooltip say when you hover over it?
It could be that the blue curly line is the right behavior now, and the instructions are just out of date.

Thanks for the question. When I hover I do see the correct answer 2. The "PROBLEMS" pane in vscode flags a problem albeit without anything specific about what the problem could be.

[Alexander Kurz]

Yaël Dillies said:

Green and blue are supposed to be the same, yeah.

What I see is also not a line ... it is this twiggle shape that is used by IDEs to indicate an error of some kind.

[Yaël Dillies]

That's completely expected. A squiggly line is a line.

[Kevin Buzzard]

Can anyone who is still having problems in this thread post a screenshot? I've never seen a green squiggly line in my life. Blue sounds fine.

[Yaël Dillies]

It's all green or blue or turquoise. I suspect whoever wrote that documentation simply had slightly different color boundaries in mind.

[Ruben Van de Velde]

Should look like one of these:
dark
light

[josedeodo]

josedeodo 发言道：

I suppose that I have installed lean4,but when I type source ~/.bash_profile in the terminal, it shows that no such file or directory.so how can I deal with it?

截屏2023-09-29-21.08.42.png
so what's going on in this terminal? I feel this speed is rather slow...

[Alex J. Best]

I can't think of anything lean specific that would slow this down, maybe your connection is just slow at the moment

[Alex J. Best]

This can be an issue as lean versions are released regularly, so you may want to only download the one you actually need for whatever project you are running

[josedeodo]

“Failed to connect to raw.githubusercontent.com port 443 after 8 ms: Couldn't connect to server”，is there any problems with my internet? I thought I should have climb up THE WALL.