Lean 4 installation issues

Stream: lean4

[Mario Carneiro]

what did you do?

[Isaia Nisoli]

I followed the instructions on the Lean4 Manual: tried once with the Basic setup, did not work, ran "elan self uninstall" and ran the Quickstart setup from the same manual but I have the same problems, both with stable and nightly.
When I call leanpkg from the command line I get an uncaught exception message and vscode gives an error message, he cannot start lean in server mode

[Mario Carneiro]

Please post the error messages and the commands you ran

[Isaia Nisoli]

isaia@aiace-laptop:~/Isabelle/Isabelle2021$ leanpkg
uncaught exception: Lean package manager, version 4.0.0

Usage: leanpkg <command>

init <name> create a Lean package in the current directory
configure download and build dependencies
build [<args>] configure and build *.olean files

See leanpkg help <command> for more information on a specific command.

[Isaia Nisoli]

In VSCode I get a Server has stopped with error code

[Isaia Nisoli]

And leanpkg.path does not exist

[Isaia Nisoli]

the OS is Ubuntu 20.10

[Mario Carneiro]

As the error message says, leanpkg requires a subcommand like leanpkg init MyProject or leanpkg build

[Mario Carneiro]

I think lean 4 doesn't use leanpkg.path anymore, that's a lean 3 thing

[Isaia Nisoli]

I will check now if there is amismatch in the VSCode extension

[Isaia Nisoli]

ok, it seems like I installed the old lean extension instead of the lean4 extension

[Mario Carneiro]

Are you using elan?

[Mario Carneiro]

https://github.com/leanprover/elan

[Isaia Nisoli]

yes, I installed everything through elan

[Isaia Nisoli]

I will try to restart vscode, it gave me an error, "The Lean 4 server crashed 5 times in the last 3 minutes. The server will not be restarted."

[Mario Carneiro]

what does lean --version at the console give?

[Mario Carneiro]

If it says lean 3, try elan override set leanprover/lean4:nightly

[Isaia Nisoli]

Lean (version 4.0.0-m2, commit 26dda3f63d88, Release)

[Mario Carneiro]

you might still want to use nightly in case there is some bug that's been fixed

[Isaia Nisoli]

VSCode is giving this output and then crashes
Watchdog error: Got unknown document URI (file:///home/isaia/lean/my_playground/gatto.lean)
[Info - 6:32:39 PM] Connection to server got closed. Server will restart.
[Error - 6:32:39 PM] Request textDocument/documentSymbol failed.
Error: Connection got disposed.
at Object.dispose (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:145943)
at Object.dispose (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:226115)
at C.handleConnectionClosed (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:226328)
at C.handleConnectionClosed (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:286716)
at t (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:224417)
at invoke (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:147556)
at o.fire (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:148317)
at Y (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:135201)
at invoke (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:147556)
at o.fire (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:148317)
at g.fireClose (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:156198)
at Socket.<anonymous> (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:157783)
at Socket.emit (events.js:327:22)
at Pipe.<anonymous> (net.js:673:12)

[Isaia Nisoli]

I will try the nightly

[Chris B]

Yeah, you need to use nightly: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/vscode-lean4.20Doesn't.20Work.20When.20I.20Switch.20Files/near/232024638

[Chris B]

For now at least.

[Isaia Nisoli]

ah, perfect! Now it seems to work! Thank you so much!

[Jürgen Uhl]

After installing Git (Windows 11), the lean4 VSCode extension and having that install elan / lean, I get the error "Watchdog error: no such file or directory (error code: 2)". Any idea, what I did wrong?

[Shreyas Srinivas]

Jürgen Uhl said:

After installing Git (Windows 11), the lean4 VSCode extension and having that install elan / lean, I get the error "Watchdog error: no such file or directory (error code: 2)". Any idea, what I did wrong?

What's your directory tree like (suitably anonymised ofc)?

[Jürgen Uhl]

which directory tree?

[Shreyas Srinivas]

where you have opened vscode

[Jürgen Uhl]

well, i open vsc from the startup icon and then select the working directory. The WD is D:\Develop\VSCode\Lean

[Jürgen Uhl]

How would I find out the startup directory?

[Shreyas Srinivas]

okay, let me start a few step earlier

[Shreyas Srinivas]

are commands like elan --version and lake version showing some output?

[Jürgen Uhl]

elan 3.0.0 (cdb40bff5 2023-09-08)

[Jürgen Uhl]

Lake version 5.0.0-a832f39 (Lean version 4.1.0)

[Shreyas Srinivas]

okay perfect. Now Please follow the steps I suggest below to create a new lean project and open it in vscode

[Shreyas Srinivas]

cd <folder where you want to create your project>

[Shreyas Srinivas]

lake new <project name>

[Shreyas Srinivas]

cd <project name>

[Shreyas Srinivas]

code .

[Jürgen Uhl]

error

[Shreyas Srinivas]

which step?
what error?

[Jürgen Uhl]

oh, should I have run that in VS Code console or windows consloe or powershell or what?

[Shreyas Srinivas]

usually use powershell (or even better for convenience, use the terminal that windows comes with these days)

[Jürgen Uhl]

I ran in vs console and the last "code ." gave an error

[Shreyas Srinivas]

vs console? Inside vscode?

[Jürgen Uhl]

yes

[Scott Morrison]

What is the error?

[Jürgen Uhl]

code : Die Benennung "code" wurde nicht als Name eines Cmdlet, einer Funktion, einer Skriptdatei oder eines ausführbaren Programms erkannt.
Überprüfen Sie die Schreibweise des Namens, oder ob der Pfad korrekt ist (sofern enthalten), und wiederholen Sie den Vorgang.
In Zeile:1 Zeichen:1

• code .
• ~~~~
  + CategoryInfo : ObjectNotFound: (code:String) [], CommandNotFoundException
  + FullyQualifiedErrorId : CommandNotFoundException

[Jürgen Uhl]

you understand that or should i translate?

[Shreyas Srinivas]

THat's because you are running the command in the cmd shell

[Jürgen Uhl]

so where should I run it?

[Shreyas Srinivas]

On windows 11 you should have an app called terminal

[Jürgen Uhl]

but that does not know "code", apparently

[Jürgen Uhl]

maybe when installing vscode i did not add the path

[Shreyas Srinivas]

wait. Once you open the terminal, windows adds extra steps

[Shreyas Srinivas]

okay that's possible.

[Shreyas Srinivas]

Please check the PATH variable first.

[Jürgen Uhl]

okay, started it with explicit path.

[Jürgen Uhl]

says "Waiting for Lean Server to start..."

[Shreyas Srinivas]

Is your toolchain on your PATH variable?

[Shreyas Srinivas]

And did it start?

[Jürgen Uhl]

Seems to work now.

[Shreyas Srinivas]

Awesome

[Jürgen Uhl]

Sorry, what is "toolchain"

[Shreyas Srinivas]

the collection of lean the compiler, lake the build tool, and some basic libraries (not Mathlib)

[Jürgen Uhl]

and where would I find that?

[Shreyas Srinivas]

cd ~/.elan

[Shreyas Srinivas]

In powershell. AFAIK, windows cmd doesn't know the command cd

[Shreyas Srinivas]

For simplicity you might want to make powershell your default terminal in your windows settings

[Jürgen Uhl]

ah, found it. And that should go into the Windows PATH, correct?

[Jürgen Uhl]

Well, anyway, seems to be working now. Thanks a lot! (Could I have found that by myself from the docs, btw.?)

[Shreyas Srinivas]

I would not recommend tinkering with a working setup. If vscode can find the lean extension and you are able to execute commands like elan --version and lake --version you should already have the correct PATH variable

[Shreyas Srinivas]

I was on autopilot when asking you about the lean toolchain being on path question

[Shreyas Srinivas]

Jürgen Uhl said:

Well, anyway, seems to be working now. Thanks a lot! (Could I have found that by myself from the docs, btw.?)

Good question. I think yes, but the docs are split between multiple places at the moment. There is an ongoing effort to rationalise and reorganise all this.

[Anotherpieceofmyhead]

Hello guys, Im new here, sorry If my issue is misplaced.
Mac M1, I cant build project with mathlib included (I even cant build the pre-existed project, I tried mathematics_in_lean as was suggested), the error is "unknown package 'Mathlib'", Is this a common issue or is this me?:)

[Scott Morrison]

It's probably you not following the instructions exactly. :-)

[Scott Morrison]

Did you open the correct folder in VSCode? (it's essential that you use "open folder", rather than opening an individual file, and you must open the folder containing the lakefile.lean).

[Scott Morrison]

@Anotherpieceofmyhead

[Anotherpieceofmyhead]

well, that makes me sad, but thats possible:)
Yes, i was opening a folder.
To be honest I thought that it might be my mistake, but after failing to build the https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf I was wondering if this is something common

[Anotherpieceofmyhead]

Nah, I figured it out, you were right about the folders and I feel ashamed :D

Thanks a lot

[Anotherpieceofmyhead]

I was opening the broader folder all the time, and lean didnt like it

[Michael Stoll]

One of my students reports the following problem. After following the first steps of these instructions (install VSCode, install git, install the Lean4 extension, set up a text file), after clicking the Install Lean using Elan button, an error message appears (sorry for the German)

(prompt)> Start-BitsTransfer -Source
 "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1"
 -Destination "elan-init.ps1"
 Die Benennung "Start-BitsTransfer" wurde nicht als Name eines Cmdlet,
 einer Funktion, einer Skriptdatei oder eines ausführbaren Programms
 erkannt. Überprüfen Sie die Schreibweise des Namens, oder ob der Pfad
 korrekt ist (sofern enthalten), und wiederholen Sie den Vorgang.
 Bei Zeile:1 Zeichen:19
 + Start-BitsTransfer <<<<  -Source
 "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1"
 -Destination "elan-init.ps1"
      + CategoryInfo          : ObjectNotFound:
 (Start-BitsTransfer:String) [], CommandNotFoundException
      + FullyQualifiedErrorId : CommandNotFoundException

To my eyes, it looks like the process tries to run a command Start-BitsTransfer, which does not exist or cannot be found in the PATH. Any ideas? (I'm working with Linux myself and don't know a lot about Windows...)

[Julian Berman]

I don't know anything about Windows either, but searching seems to suggest that error means that the student is on an old Powershell (1.0). What version of Windows is this, do you know?

[Michael Stoll]

I don't know, but I've asked.

[Julian Berman]

Assuming I can interpret the page I'm reading I believe the answer will be "quite old", as I think this is saying Powershell 2.0 is present already even in Windows 7. But let's see.

[Julian Berman]

Regardless, it might be asking them to follow https://learn.microsoft.com/en-us/powershell/scripting/install/installing-powershell-on-windows?view=powershell-7.3 is going might be the next step.

[Michael Stoll]

I'm still waiting for an answer regarding the Windows version. Going to bed now...

[René Schoof]

following the instructions on
https://leanprover-community.github.io/install/macos.html
to install lean4 on my Mac (Sonoma 14.2.1) I got an error message:
/usr/local/Library/Homebrew/version.rb:186:in `initialize': Version value must be a string (TypeError)
What can I do about this?

[Julian Berman]

That sounds like your Homebrew is possibly very old or very broken.

[Julian Berman]

Try running brew update

[René Schoof]

Thanks for the hint. But I get the same error message:

 brew update
/usr/local/Library/Homebrew/version.rb:186:in `initialize': Version value must be a string (TypeError)
    from /usr/local/Library/Homebrew/os/mac/version.rb:25:in `initialize'
    from /usr/local/Library/Homebrew/os/mac.rb:15:in `new'
    from /usr/local/Library/Homebrew/os/mac.rb:15:in `version'
    from /usr/local/Library/brew.rb:31:in `<main>'

[Kevin Buzzard]

(You can post output like this in between blank lines containing triple backticks ``` (see #backticks for more information). Then it won't look all messed up.)

[Julian Berman]

@René Schoof that's the output you get from brew update? If so I'd recommend reinstalling Homebrew entirely.

[Julian Berman]

Do you have things you know you've installed with it as far as you're aware?

[Julian Berman]

Feel free to ask if you need help doing the reinstall -- otherwise, especially if the answer to the above is "no", you probably want to run https://github.com/homebrew/install#uninstall-homebrew then you can re-run the Lean installation script

[Kevin Buzzard]

Someone suggested purging homebrew completely @René Schoof and then lean might just work immediately.

[Adam Topaz]

I’m not sure about lean itself, but I think the easy macOS install script might work after purging (it attempts to install a fresh homebrew of it can’t find brew in the path). IIRC homebrew has an official uninstall script?

[Julian Berman]

Yes, I linked it :)

[Michael]

Tangential, but the documented way to install lean 4 is a total nightmare from China, where github is a banned domain.

I can download files myself if you'll tell me where they are. I can put them in appropriate locations if you'll tell me where they are supposed to be. But it's an enormous pain to constantly swap back and forth between a configuration that lets me use git to clone git repositories from github and a different, incompatible configuration that lets lake.exe download files from github using normal download protocols, all while having to repeatedly root through error logs for indications of what the magic VSCode script wanted to happen so that I can accomplish the broken part myself, or switch into the opposite 'get things from github' configuration.

[Mario Carneiro]

there was some discussion about lean in china here and here

[Mario Carneiro]

I'd be happy to work with someone in china to figure out how to make elan and cache work better with approved domains; I don't really know how the whole great firewall thing works in practice

[Michael]

how it works in practice is that your traffic gets dropped.

PS C:\Michael\lean\mathematics_in_lean> ping github.com

Pinging github.com [20.205.243.166] with 32 bytes of data:
Request timed out.
Request timed out.
Request timed out.
Request timed out.

Ping statistics for 20.205.243.166:
    Packets: Sent = 4, Received = 0, Lost = 4 (100% loss),

[Mario Carneiro]

No how is it supposed to work

[Mario Carneiro]

I get that the regular methods don't work

[Mario Carneiro]

but what are the non-regular methods that do?

[Mario Carneiro]

how do you access anything from github at all?

[Mario Carneiro]

is it just a matter of replacing occurrences of github.com with github.cn or whatever in the HTTP requests?

[Michael]

well, I can say what I did, but it's all workarounds:

I run a shadowsocks server on a residential IP address in the United States. I run a shadowsocks client here, in China, giving me an encrypted tunnel to the US. Any traffic I can send through that tunnel is fine. I have git configured to proxy connections to github.com through that. (I also have Firefox configured to proxy almost all connections through it.)

But Windows, overall, isn't willing to proxy through it as a general matter. So when elan.exe tries to download from github.com, that fails, because it's making the request to Windows and Windows is too stupid to know how to handle it. The workaround to that is to enable a VPN that forces all outgoing connections to use itself. But this is a very bad solution in general, because the great firewall will quickly pick up on it and block all my connections. (Theoretically, I could probably create something that appears to be such a coercive VPN to windows, but just sends all my traffic through the shadowsocks client, but I don't know how to do that...) Having the VPN enabled, as long as it hasn't yet been blocked, means that elan.exe's attempts to download stuff can succeed.

(Technically, my shadowsocks tunnel appears to be some sort of grandfathered thing. It works without hiccups as long as the connection is coming from my home network. Trying to connect from my cell phone over the cellular network is instantly blocked. I don't know if the rules are different for home broadband vs cellular or what; it can't quite be that my broadband provider knows I'm foreign and gives me looser treatment, because my cell service is part of a bundle with the broadband. Not really relevant to the lean issues, but if someone does know more about this, I'd like to know it too.)

[Michael]

If lean hosted its stuff on a domain that wasn't github, then that domain wouldn't be blocked (assuming it was something specific to lean... any social media domain tends to be blocked) and the current system would work... as well as it's supposed to work.

[Michael]

Mario Carneiro said:

is it just a matter of replacing occurrences of github.com with github.cn or whatever in the HTTP requests?

Replacing github.com with some other URL would work in that the great firewall would not object to that URL and the connection would go through. github.com is on a blacklist. But it wouldn't work, in the sense of installing lean, unless that other URL reached a server somewhere that provided the appropriate files.

(Let me revise that a bit... as the ping showed, I can make a DNS request for github.com just fine. But I can't actually connect to it without a workaround, so what's on a blacklist is probably a set of IP addresses owned by github.)

[Michael]

Mario Carneiro said:

I'd be happy to work with someone in china to figure out how to make elan and cache work better with approved domains; I don't really know how the whole great firewall thing works in practice

So, currently elan automatically reaches out to github.com. The great firewall thinks this is bad and drops the traffic. If it used a different domain that wasn't banned, that would pretty much be the end of things as far as the great firewall is concerned. But that would mean making a couple of changes:

• either elan would be switched from its current strategy of "always use github, no matter what" to "always use lean4.net [for example], no matter what", or there would have to be a way to configure elan to check the URL of the user's choice
• the relevant lean files would have to be made available somewhere other than github.

[Kevin Buzzard]

Wow! Is this what everyone in China has to do to get a reasonable Lean experience? This to me sounds like a problem which the community should be interested in solving. I know that last summer I had a student in China who wanted to work with me but could never get the system installed and I couldn't do anything to help them, I had no idea how to debug and fix the issues they were having, or whether the things I wanted to suggest would even work in China.

[Michael]

My favored solution would be to take some of the magic out of the VSCode installation script, though as has correctly been noted it would also be necessary to take some of the magic out of lake and elan, if that was the approach

[Julian Berman]

Does elan not work even if you set http_proxy / https_proxy env vars to your SOCKS proxy?

[Julian Berman]

I'd expect the rust stdlib should respect those.

[Michael]

The "simple" solution would be for the lean project to stop relying on github for free file hosting, and host its stuff on its own website, but that amounts to me making demands for other people to do work (and incur some expenses); I do not actually feel entitled to make this demand.

[Michael]

Julian Berman said:

Does elan not work even if you set http_proxy / https_proxy env vars to your SOCKS proxy?

I tried to do that, but I don't guarantee that I did it correctly.

[Julian Berman]

It'd take some chasing (of Windows / elan source / Rust docs) to be sure I could tell you the right incantation I think. Maybe someone will know off-hand. To me initially though other than what you say (hosting mirrors of the files elsewhere) that seems like the right avenue to pursue.

[Julian Berman]

I guess first let's see what elan uses to do HTTP.

[Michael]

do you have some example elan commands for me to play with? (to see whether I can get the connection to route properly)

[Julian Berman]

Looks like it has 2 backends, one using curl and the other using reqwest. The latter definitely supports https_proxy, I'm sure curl does too.

[Julian Berman]

export https_proxy=socks5://yourproxy then elan toolchain download nightly maybe

[Michael]

just to be clear, elan toolchain download nightly won't do anything that I wouldn't have wanted?

[Mario Carneiro]

it does nothing damaging to your system or irreversible

[Mario Carneiro]

it downloads an additional lean toolchain that you probably won't be using much

[Julian Berman]

Ah wait, so elan depends on reqwest but doesn't enable the socks feature. So I think that's not going to work on that backend (maybe still using curl though).

[Julian Berman]

I don't know what rust packaging norms are for enabling features of downstream deps but probably that's an easy fix to add.

[Michael]

USAGE:
    elan.exe toolchain <SUBCOMMAND>

FLAGS:
    -h, --help    Prints help information

SUBCOMMANDS:
    list         List installed toolchains
    install      Install or update a given toolchain
    uninstall    Uninstall a toolchain
    link         Create a custom toolchain by symlinking to a directory
    help         Prints this message or the help of the given subcommand(s)

there is no download subcommand

[Julian Berman]

Sorry, install.

[Julian Berman]

elan toolchain install nightly

[Michael]

with no attempt to proxy at all:

PS C:\Users\Michael\.elan\bin> .\elan.exe toolchain install nightly
info: syncing channel updates for 'nightly'
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value:
Error {
  description: "Timeout was reached",
  code: 28,
  extra: Some("Failed to connect to github.com port 443 after 21039 ms: Couldn't connect to server")
}', src\elan-utils\src\utils.rs:514:32

(this is expected; I'm just posting it to be informational)

[Mario Carneiro]

Julian Berman said:

I don't know what rust packaging norms are for enabling features of downstream deps but probably that's an easy fix to add.

Not entirely sure what you are asking here, but I think we can just enable the socks feature in elan releases for everyone

[Julian Berman]

Yeah that sounds nice then (I was asking essentially whether there's a way for end users to add features on install, but of course that makes no sense since install is a single binary in rust)

[Mario Carneiro]

for testing purposes, @Michael could download elan manually and recompile it with that feature enabled, and then hopefully your export trick works

[Julian Berman]

Let's see if it works anyhow with the curl backend I think.

[Mario Carneiro]

what do you mean by that?

[Julian Berman]

Or is which backend is used hardcoded

[Mario Carneiro]

I don't recall elan having any option to switch out the backend

[Julian Berman]

Mario Carneiro said:

what do you mean by that?

(Stop me when I'm saying things you know are totally wrong, I'm sure you've looked at this more than I have)

[Mario Carneiro]

maybe it has one in the code but then that would also require a recompile

[Julian Berman]

OK yeah I just saw...

[Julian Berman]

https://github.com/leanprover/elan/blob/640358e252e6eda100ed4a96a993b2bbb97d0574/src/download/src/lib.rs#L20-L23

[Julian Berman]

But if there's no CLI option to swap then we're out of luck.

[Julian Berman]

It looks liek the default is curl though: https://github.com/leanprover/elan/blob/640358e252e6eda100ed4a96a993b2bbb97d0574/Cargo.toml#L15

[Julian Berman]

@Michael keep going, let's see what happens :)

[Mario Carneiro]

There is an env var ELAN_USE_REQWEST

[Mario Carneiro]

https://github.com/leanprover/elan/blob/640358e252e6eda100ed4a96a993b2bbb97d0574/src/elan-utils/src/utils.rs#L219C65-L219C81

[Julian Berman]

Right I just found that too.

[Michael]

PS C:\Users\Michael\.elan\bin> $env:http_proxy = "http://localhost:9198"
PS C:\Users\Michael\.elan\bin> $env:http_proxy
http://localhost:9198
PS C:\Users\Michael\.elan\bin> .\elan.exe toolchain install nightly
info: syncing channel updates for 'nightly'
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value:
Error {
  description: "Timeout was reached", code: 28,
  extra: Some("Failed to connect to github.com port 443 after 21050 ms: Couldn't connect to server")
}', src\elan-utils\src\utils.rs:514:32
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Same error with proxy given as http://. (I know that's not socks5://, but it works in other contexts; I'm about to try socks5://.)

[Michael]

wait, better news! It appears to work after setting $env:https_proxy = "http://localhost:9198"

[Michael]

I should note that this exact solution is unlikely to work well for actual Chinese people, who will have a harder time using a US residential IP address. Running a shadowsocks tunnel to a major provider like DigitalOcean gets blocked; the residential IP is a load-bearing part of my setup.

[Mario Carneiro]

The other relevant internet-hitting operations:

• git clone https://github.com/leanprover-community/mathlib4
• lake exe cache from mathlib4 folder (which will clone all the dependent repos from github)
• lake exe cache get (which will download the cache files from azure)

[Michael]

(on the other hand, VPN use in Chinese universities is routine; I'd expect professors and students to be aware of workarounds that are available to them?)

[Mario Carneiro]

If this works, I think we will want to document how to set https_proxy but leave it to them to figure out what proxy to supply

[Julian Berman]

Michael said:

wait, better news! It appears to work after setting $env:https_proxy = "http://localhost:9198"

(which syntax you use will have to do with whether you're using Powershell, which it sounds like you are, or git bash, and of course where your proxy is listening on)

But glad it worked!

[Mario Carneiro]

Are there more advanced techniques that need more than just a proxy that we need to prepare for?

[Mario Carneiro]

I don't think it is feasible for us to get off github, because it's not just lean but also the whole package registry that we'd have to host (and handle authentication for...)

[Michael]

you have access controls on your packages? I kind of figured they were available to everyone

[Mario Carneiro]

we have access controls on pushing new content to existing packages

[Mario Carneiro]

or rather, github does, they are just github projects and the owner decides what they want to push

[Michael]

I think a normal workflow would be to keep package creation on github, and have some kind of automatic process that mirrors artifacts over to the lean website -- but again, don't take that as a demand

[Michael]

ok, for git in specific, that works for me based on configuring the git variable http.proxy; the command to set that is git config --global http.proxy http://host:port, where http://host:port is whatever the path to your proxy is. Supposedly there are ways to set proxy variables for specific domains.

[Michael]

don't know whether git will also look for the environment variable; haven't checked

[Michael]

with the https_proxy env variable set, lake.exe exe cache appears to work

[Julian Berman]

Michael said:

don't know whether git will also look for the environment variable; haven't checked

It should. (But I'd leave your git-specific config anyhow).

[Michael]

lake.exe exe cache get also appears to work (with the https_proxy env var set)

[Michael]

However, I have a remaining concern, which is that the documented installation procedure doesn't involve me running these commands. Instead, it says I should install a VSCode addon that runs them for me. The env vars would have to be set within that environment.

(My other complaint about the VSCode-script approach to setup is that, when the installation script breaks, I have to go look at the error log, which is annoying... and if the error log has produced too much output, VSCode truncates it, which is much worse than just being annoying.)

[Michael]

VSCode has its own HTTP proxy setting, but I attempted to use that and it didn't help with the lake commands

[Julian Berman]

I suspect VSCode should respect https_proxy as well, any good HTTP client should AIUI.

[Julian Berman]

I.e. if you run code . after that export hopefully the install works the "normal" way.

[Michael]

Mario Carneiro said:

If this works, I think we will want to document how to set https_proxy but leave it to them to figure out what proxy to supply

this sounds fairly reasonable; summing up what I see as the requirements for this approach:

0. (optional?) "here's how to set git's http.proxy variable"
1. "you'll need to set an environment variable named https_proxy"
2. "here's how to do that on the major platforms"
3. "here's how to set it so that it's visible to the installation script running from VSCode"

It is possible to make a permanent change to the Windows environment variables using a GUI interface that is available in a couple of places, but that's actually something I'd prefer not to do when the variable in question is https_proxy.

[Michael]

Julian Berman said:

I.e. if you run code . after that export hopefully the install works the "normal" way.

this is not knowledge that I have; I had never previously used VSCode. Instructions for how to resume the installation script within VSCode after it breaks (and after manually setting the environment variable) would meet my needs.

[Julian Berman]

(+1 for that list), but I think what you said before is important to consider though, I don't know that everyone who runs into this is going to have a SOCKS proxy.

[Julian Berman]

Michael said:

Julian Berman said:

I.e. if you run code . after that export hopefully the install works the "normal" way.

this is not knowledge that I have; I had never previously used VSCode. Instructions for how to resume the installation script within VSCode after it breaks (and after manually setting the environment variable) would meet my needs.

Right not discounting anything you've said about improving docs of course!

[Michael]

(Though at that point, things are getting pretty hacky and I'm pretty sure there will be people who get frustrated and give up. I have a high tolerance for futzing around with the installation script.)

[Mario Carneiro]

Given the way that people in China are apparently supposed to connect to the internet, it makes me despair for any general solution we can just package up in a script that a child could run

[Michael]

Right, as long as you're seen as a threat (because of your domain), people will need to provide their own solution for getting past the firewall, and mostly what you need to do is allow them to do that.

The current system is painful, in my eyes, because it has several layers, VSCode running an installation script that calls various executables, and providing the proxy at the top layer, the VSCode Http: Proxy setting, didn't work. So I had to peek inside and try to manipulate the stuff in the middle, and in the event I didn't quite know how.

Potentially, the installation script might check the VSCode setting and, if present, supply it as an environment variable when it calls lake and/or git? That still requires the user to have a working proxy, but it centralizes the method of supplying it to the installation process.

[Michael]

And at the very least it makes documenting "if you need to use a proxy, here's the place where you tell the system about it" easier, if it works.

[Michael]

though then again...

[Michael]

The VSCode setting specifically states that, if not set within VSCode, it will inherit from the https_proxy environment variable. So if that is set globally, I guess that sort of amounts to the same thing, except that setting the environment variable is what the script really wants and setting the VSCode variable is what the user wants to have to do instead.

[Michael]

vscode_setting.png

[Michael]

the other approach to a general script, the one that appeals to me personally, is to package things up in a script that doesn't reach out to the internet, and to have the instructions be more along the lines of

1. Download this package. [link]
2. Put it somewhere appropriate.
3. Run this script [link], which assumes you've already downloaded the right stuff.

[Michael]

(another advantage of that approach is that it naturally enables someone who doesn't have a proxy to copy a working lean installation from someone who does)

[Kim Morrison]

Just dropping a link to an elan issue about this https://github.com/leanprover/elan/issues/117, where I noticed that there has been simultaneous (but perhaps disconnected?) discussion.

[Julian Berman]

Well, then I'll also mention for anyone who ends up finding this thread -- on the subject of "how many users is this applicable to" -- if you're behind the firewall, what you really need is any SSH'able host outside the firewall that you can get to, because anything you can SSH to you can also SOCKS proxy through (because SSH is just that good, hooray). The command you need is usually ssh -D 3737 YOURSSHHOST -N (where 3737 can be any port number you like). And then once you run that it will sit there looking like it's not doing anything, but if you open a second terminal you can now set export https_proxy='socks://127.0.0.1:3737' and proceed with the above.

[Kim Morrison]

I doubt this helps windows users, but on linux and mac I have had huge success with sshuttle. It completely seamlessly redirects all your network traffic through an ssh connection, without any per-application proxy configuration.

[Kim Morrison]

Another issue about http_proxy: https://github.com/leanprover/lean4/issues/3211

[Michael]

Julian Berman said:

Well, then I'll also mention for anyone who ends up finding this thread -- on the subject of "how many users is this applicable to" -- if you're behind the firewall, what you really need is any SSH'able host outside the firewall that you can get to, because anything you can SSH to you can also SOCKS proxy through (because SSH is just that good, hooray). The command you need is usually ssh -D 3737 YOURSSHHOST -N (where 3737 can be any port number you like). And then once you run that it will sit there looking like it's not doing anything, but if you open a second terminal you can now set export https_proxy='socks://127.0.0.1:3737' and proceed with the above.

That will work for a while, likely long enough to get lean installed, but it's not stable; a socks-over-ssh tunnel will get blocked within a couple of days.

[Michael]

if it's a machine that you need to access for other reasons, running a socks proxy to it is a good way to get yourself cut off from it for an extended period