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 https://github.com/leanprover/elan/issues/117#issuecomment-1908438378, 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 https://github.com/leanprover/elan/issues/117#issuecomment-1908438378, 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 https://github.com/leanprover/elan/issues/117#issuecomment-1914200787, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAABBQTWJX4L74KUX4AOWGTYQ5ND7AVCNFSM6AAAAABBEYLLKGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMJUGIYDANZYG4 . You are receiving this because you authored the thread.Message ID: @.***>

[semorrison]

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.