command 'lean4. displayGoal' not found

Stream: lean4

[blackxv]

When I use Lean4 to view the goal via the buton "Infoview: Dispaly Goal", the error message --command 'lean4. displayGoal' not found-- pops, who can help me, thank you!

[Scott Morrison]

Usually one would never need to click such a button --- the goal just appears in the infoview when your cursor is in a relevant spot in the editor.

Do you have anything working? Which instructions for getting started did you follow?

[blackxv]

Extension lean4 is already installed in VSCode, but Elan and lean cannot be automatically installed. When manually installing, the following message appears:

---

info: syncing channel updates for 'nightly'
thread 'main' panicked at 'called Result::unwrap() on an Err value: Error { description: "SSL connect error", code: 35, extra: Some("schannel: next InitializeSecurityContext failed: Unknown error (0x80092012)") }', src\elan-utils\src\utils.rs:514:32
note: run with RUST_BACKTRACE=1 environment variable to display a backtrace
Elan failed with error code 101
1

---

thank you.

[Scott Morrison]

When you say "when manually installing", you mean you are running the command

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

from the instructions at https://github.com/leanprover/elan?

[Scott Morrison]

Are you behind a corporate or state firewall? Can you usually access github repositories?

[blackxv]

Yes, I can access github repositories.

[Scott Morrison]

What about my first question?

[Scott Morrison]

The error is about an "SSL connect error", so it is most likely a problem with your network connection, or a transient github failure. Can you try from another device/network to see if that helps?

[blackxv]

Thank you very much. I think I have installed lean4 now after rebooting my computer.

---

E:\foo>lean -v
Lean (version 4.0.0-nightly-2023-08-26, commit 0b64c1e3301f, Release)

---

But Lean4 also doesn't work as before :broken_heart:

---

图片.png

---

[Alex J. Best]

Can you try to clone an existing lean project (e.g. https://leanprover-community.github.io/install/project.html#working-on-an-existing-project) and open that folder in vscode and see if that works?

[blackxv]

sorry, I think there is also an error about "SSL connect error". I don't know how to slove it

---

mathematics_in_lean>lake exe cache get
info: downloading component 'lean'
Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "SSL connect error", code: 35, extra: Some("schannel: next InitializeSecurityContext failed: Unknown error (0x80092012)") }), backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/leanprover/lean4-nightly/releases/expanded_assets/nightly-2023-08-23' to '.....\.elan\tmp\t76u0iy48ylt9e55_file'
info: caused by: error during download
info: caused by: [35] SSL connect error (schannel: next InitializeSecurityContext failed: Unknown error (0x80092012))

[Scott Morrison]

Yes, as I said above, this is not something specific to Lean, but instead that you are having trouble with SSL connections. Could you answer my question from above: "Are you behind a corporate or state firewall?"

[blackxv]

I don't think I am behind a firewall because lean3 was installed successfully before . Futhermore, I think rebooting doesn't help if the state firewall blocks me.
I live in Chinese Mainland.

[Scott Morrison]

Can you see if the SSL errors persist when using a VPN? (Sorry if this isn't possible.) I'm pretty confident that the problem you are experiencing is just a network connectivity problem, and nothing to do with Lean itself, unfortunately.

[blackxv]

I don't think that is because of VPN although my computer uses VPN occasionally indeed. In fact the error exists when VPN is not running. Anyway, thank you very much.

[Scott Morrison]

No, I was hoping that using the VPN would help, because someone (probably the Chinese firewall?) is messing with your SSL connection.

[blackxv]

oh! I misunderstood you. The VPN in my computer wouldn't help me because it is is used to access some resources of my working organization. I also know that lean4 doesn't work for me properly is not a problem with lean4 itself. I hope that lean4 could have a package version "trylean4_windows.zip" similar to lean3.

[Scott Morrison]

@MohanadAhmed what is the status of your windows bundle? It seems we need it here! (And my apologies that I flaked on testing it for you.)

[Alex J. Best]

There is a proposal for new trylean bundles for lean 4, but it is still being developed. You could try https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/trylean.20bundle.20for.20lean4/near/383326160

[MohanadAhmed]

@Scott Morrison
The bundle seems to work for me and Miguel Marco.

Hello @blackxv

The steps are quite straight forward :

1. Download the file https://drive.google.com/file/d/1Ws7-t185QXL262-S7MPGu3wm_ZzAwwha/view?usp=sharing

2. Run it to unzip the pack folder.

3. Double click on the RunLean.bat file. It will take a bit but eventually you should see VSCodium with a DemoProj open.

4. On the File Explorer in VSCodium open the file DemoProj.lean and try the comands you tried earlier like #eval Lean.versionString #eval 1 + 1 and so on

[MohanadAhmed]

Please let me know how it goes and if you need help

[MohanadAhmed]

Hello @blackxv
How did it go?

[blackxv]

图片.png

[blackxv]

DemoProj works well. Thank you.