how do i set http(s) proxy for elan?

[cartazio]

Hello, i'm trying to setup lean on a windows environment where i need to set an http proxy

is there some particular env variables that elan looks for? i dont see any documentations about this

$ elan default stable
info: syncing channel updates for 'stable'
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) - The revocation function was unable to check revocation for the certificate.") }', src\elan-utils\src\utils.rs:514:32
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

is the error i got

[Kha]

Hi, I believe https://rust-lang.github.io/rustup/network-proxies.html should be applicable to elan as well; also note the libcurl note at the end, which elan always uses. Feel free to add this information to the readme if it works.

[cartazio]

So i'm doing that as best as I can discern. The issue i think lies with it being a corporate network proxy and I need to revocation checking! per The revocation function was unable to check revocation for the certificate.") part of the error message, and the rust docs dont seem to mention a way to do that.

libcurl has some flags for running in 'insecure mode', is there any hooks for passing flags into libcurl?

[Kha]

I don't know the first thing about proxies, but why wouldn't that be covered by http_proxy?

libcurl has some flags for running in 'insecure mode', is there any hooks for passing flags into libcurl?

I don't think so, http_proxy is one of the few ones supported out of the box https://curl.se/libcurl/c/libcurl-env.html

[cartazio]

i set both SET CARGO_HTTP_PROXY= and HTTP_PROXY and i'm just seeing a connection time out.

$ elan toolchain install stable
info: syncing channel updates for 'stable'
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 21023 ms: Couldn't connect to server") }', src\elan-utils\src\utils.rs:514:32

[cartazio]

is it possible that using port 443 is hard coded somewhere? this is in an environment where https needs to be proxied over a different port

[cartazio]

ive also tried all the various cargo and curl style config files and no luck there :(

[Kha]

The quick answer is that I have no idea, about any of this. Sorry!

[cartazio]

I’ll see about putting together a patch for this :)

…

On Wed, Jan 24, 2024 at 11:05 AM Sebastian Ullrich ***@***.***> wrote: The quick answer is that I have no idea, about any of this. Sorry! — Reply to this email directly, view it on GitHub <#117 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABBQWWHPLRWDNDAPS4H7TYQEWN3AVCNFSM6AAAAABBEYLLKGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMBYGQZTQMZXHA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[cartazio]

Would a simple patch that adds explicit http proxy support be considered? On Wed, Jan 24, 2024 at 7:25 PM Carter Schonwald ***@***.***> wrote:

…

I’ll see about putting together a patch for this :) On Wed, Jan 24, 2024 at 11:05 AM Sebastian Ullrich < ***@***.***> wrote: > The quick answer is that I have no idea, about any of this. Sorry! > > — > Reply to this email directly, view it on GitHub > <#117 (comment)>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AAABBQWWHPLRWDNDAPS4H7TYQEWN3AVCNFSM6AAAAABBEYLLKGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMBYGQZTQMZXHA> > . > You are receiving this because you authored the thread.Message ID: > ***@***.***> >

[Kha]

If it solves your issue when http_proxy (note the casing!) doesn't, then yes

[cartazio]

Hrmm. I’ll double check that one too before I go full patch :)

…

On Mon, Jan 29, 2024 at 3:33 AM Sebastian Ullrich ***@***.***> wrote: If it solves your issue when http_proxy (note the casing!) doesn't, then yes — Reply to this email directly, view it on GitHub <#117 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABBQTWJX4L74KUX4AOWGTYQ5ND7AVCNFSM6AAAAABBEYLLKGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMJUGIYDANZYG4> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[kim-em]

Just noting that there has been recent discussion on zulip about this issue. I haven't followed the details but if you're interested in this it is probably worth reading.

[tothedistance]

$env:https_proxy = "http://localhost:9198" works

Just noting that there has been recent discussion on zulip about this issue. I haven't followed the details but if you're interested in this it is probably worth reading.

[cartazio]

This was on a windows machine :)

…

On Mon, Jan 20, 2025 at 10:10 PM John Huang ***@***.***> wrote: $env:https_proxy = "http://localhost:9198" works Just noting that there has been recent discussion on zulip <https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.204.20installation.20issues/near/418518096> about this issue. I haven't followed the details but if you're interested in this it is probably worth reading. if host is macOS, then should add https_proxy in ~/.bashrc file, not ~/.zshrc file, I guess rust default use bash not zsh. @cartazio <https://github.com/cartazio> — Reply to this email directly, view it on GitHub <#117 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABBQSCD6BRPYIZBIIPGOT2LW3A3AVCNFSM6AAAAABTFTUFRSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMMBTGUZTGMBVHA> . You are receiving this because you authored the thread.Message ID: ***@***.***>