leanprover
Downloading Lean toolchains manually
I have a poor internet connection, and elan fails to download files from releases.lean-lang.org. It there a way to tell elan to instead use files I downloaded manually?
I too have Transferred a partial file -> Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Transferred a partial file", code: 18, extra: Some("end of response with 59606407 bytes missing") }), backtrace: InternalBacktrace { backtrace: None } })
I can't download toolchain file by elan either. I download it by my browser and then set up a https server as a mirror. While the mirror running, I can use elan to install lean toolchain. I wrote a script for it, If you can read chinese, maybe it will be helpful for you: https://github.com/Acomage/elan-wrapper
That is quite some work you did ! I haven't took the time to make it work on Windows, I received this answer on Zulip though :
Creating new projects with a specific toolchain that isn't the most recent stable toolchain (as set by leanprover/lean4:stable) unfortunately currently isn't supported by the VS Code extension, but you should be able to use the command-line to create the project instead. First confirm that your custom Lean version is correctly set up by running lean --version. Then, run lake init in the directory where you want your project to be created (or lake new
if you want to create a new project directory).
That is quite some work you did ! I haven't took the time to make it work on Windows, I received this answer on Zulip though :
Creating new projects with a specific toolchain that isn't the most recent stable toolchain (as set by leanprover/lean4:stable) unfortunately currently isn't supported by the VS Code extension, but you should be able to use the command-line to create the project instead. First confirm that your custom Lean version is correctly set up by running lean --version. Then, run lake init in the directory where you want your project to be created (or lake new if you want to create a new project directory).
My script cannot work on Windows, because handling the hosts file and trust store is different between Windows and GNU/Linux. On Windows, you can manually edit your hosts file (usually located at C:\Windows\System32\drivers\etc\hosts) and manage the trust store (maybe you need openssl to do this). After that, you can set up a mirror server. An easier option might be to use WSL.
I don’t use the VS Code extension to manage my toolchain. Do you want to use a specific toolchain? If so, is your goal to work with an existing Lean project that uses a specific toolchain, or to create a new one yourself?
If you want to use someone else’s project, look for a file named lean-toolchain in the project’s root directory. It will tell you which toolchain version you need. Install that version, then run lake build in the project directory.
If you want to create a new Lean project with a specific toolchain, you need to know which Lean version you want to use. Install it, set it as default with elan default <toolchain>, and then run elan new <projectName>.
My goal was to create a new Lean project through the VSCode extension, as failing to do so would mean the extension wasn't linked correctly to elan or something (basically would not work) but its all working now. For setting up a local mirror I tried to use https://github.com/mitmproxy/mitmproxy but it asked about a revocation server being offline and I abandoned from there lol but thank you nonetheless !
@suhr I was also having the same issue, I think the problem is elan downloads the toolchain from github and connection gets closed by github randomly when you download from a slow network for performance reasons. And elan doesn't retry the connection. It would be great if this feature is added, rustup already supports this.
Coming to the solution, i was also forced to install the toolchain manually. The solution below is only for Linux, but i guess you only need to change some directory names.
This are the steps i used
- Manually downloaded the toolchain. in my example here i am downloading v4.23.0, you need to run this command repeatedly until it downloads the full file. The
-C -argument is the important one, it tells it resume from the partially downloaded file when running the command again.
curl -L -C - https://releases.lean-lang.org/lean4/v4.23.0/lean-4.23.0-linux.tar.zst --output lean-4.23.0-linux.tar.zst
- Then create ~/.elan/toolchains directory if it is not already
mkdir ~/.elan/toolchains
- Then decompress to the following directory
~/.elan/toolchains/leanprover--lean4---v4.23.0like this
tar --use-compress-program=unzstd -xvf lean-4.23.0-linux.tar.zst --strip-components=1 -C ~/.elan/toolchains/leanprover--lean4---v4.23.0
You can check if it worked by running elan show and you will see it listed there.
The reason is:
wget https://releases.lean-lang.org/lean4/v4.23.0/lean-4.23.0-linux.tar.zst --2025-09-17 16:47:07-- https://releases.lean-lang.org/lean4/v4.23.0/lean-4.23.0-linux.tar.zst Resolving releases.lean-lang.org (releases.lean-lang.org)... 65.21.197.56, 216.239.38.108, 216.239.32.108, ... Connecting to releases.lean-lang.org (releases.lean-lang.org)|65.21.197.56|:443... connected. HTTP request sent, awaiting response... 302 Moved Temporarily Location: https://github.com/leanprover/lean4/releases/download/v4.23.0/lean-4.23.0-linux.tar.zst [following] --2025-09-17 16:47:07-- https://github.com/leanprover/lean4/releases/download/v4.23.0/lean-4.23.0-linux.tar.zst Resolving github.com (github.com)... 20.217.135.5, 198.51.44.8, 198.51.45.8, ... Connecting to github.com (github.com)|20.217.135.5|:443... connected. HTTP request sent, awaiting response... 302 Found Location: https://release-assets.githubusercontent.com/github-production-release-asset/129571436/f49b721f-f4dd-4d02-a474-6de64a12b6a6?sp=r&sv=2018-11-09&sr=b&spr=https&se=2025-09-17T14%3A23%3A16Z&rscd=attachment%3B+filename%3Dlean-4.23.0-linux.tar.zst&rsct=application%2Foctet-stream&skoid=96c2d410-5711-43a1-aedd-ab1947aa7ab0&sktid=398a6654-997b-47e9-b12b-9515b896b4de&skt=2025-09-17T13%3A22%3A53Z&ske=2025-09-17T14%3A23%3A16Z&sks=b&skv=2018-11-09&sig=QA4%2B2jA%2Btso6VoRlWzxgdgn00rlpGMov47wkh6EEvbU%3D&jwt=eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmVsZWFzZS1hc3NldHMuZ2l0aHVidXNlcmNvbnRlbnQuY29tIiwia2V5Ijoia2V5MSIsImV4cCI6MTc1ODExNzEyOSwibmJmIjoxNzU4MTE2ODI5LCJwYXRoIjoicmVsZWFzZWFzc2V0cHJvZHVjdGlvbi5ibG9iLmNvcmUud2luZG93cy5uZXQifQ.X0hui6Npl66lSagmPV1Yd3uUiPQuoaqE2wFNoZmAogI&response-content-disposition=attachment%3B%20filename%3Dlean-4.23.0-linux.tar.zst&response-content-type=application%2Foctet-stream [following] --2025-09-17 16:47:08-- https://release-assets.githubusercontent.com/github-production-release-asset/129571436/f49b721f-f4dd-4d02-a474-6de64a12b6a6?sp=r&sv=2018-11-09&sr=b&spr=https&se=2025-09-17T14%3A23%3A16Z&rscd=attachment%3B+filename%3Dlean-4.23.0-linux.tar.zst&rsct=application%2Foctet-stream&skoid=96c2d410-5711-43a1-aedd-ab1947aa7ab0&sktid=398a6654-997b-47e9-b12b-9515b896b4de&skt=2025-09-17T13%3A22%3A53Z&ske=2025-09-17T14%3A23%3A16Z&sks=b&skv=2018-11-09&sig=QA4%2B2jA%2Btso6VoRlWzxgdgn00rlpGMov47wkh6EEvbU%3D&jwt=eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmVsZWFzZS1hc3NldHMuZ2l0aHVidXNlcmNvbnRlbnQuY29tIiwia2V5Ijoia2V5MSIsImV4cCI6MTc1ODExNzEyOSwibmJmIjoxNzU4MTE2ODI5LCJwYXRoIjoicmVsZWFzZWFzc2V0cHJvZHVjdGlvbi5ibG9iLmNvcmUud2luZG93cy5uZXQifQ.X0hui6Npl66lSagmPV1Yd3uUiPQuoaqE2wFNoZmAogI&response-content-disposition=attachment%3B%20filename%3Dlean-4.23.0-linux.tar.zst&response-content-type=application%2Foctet-stream Resolving release-assets.githubusercontent.com (release-assets.githubusercontent.com)... 185.199.110.133, 185.199.108.133, 185.199.109.133, ... Connecting to release-assets.githubusercontent.com (release-assets.githubusercontent.com)|185.199.110.133|:443... connected. HTTP request sent, awaiting response... 200 OK Length: 436396005 (416M) [application/octet-stream] Saving to: ‘lean-4.23.0-linux.tar.zst’
lean-4.23.0-linux.tar.zst 79%[=================================================================> ] 330.00M 1.09MB/s in 5m 10s
2025-09-17 16:52:18 (1.07 MB/s) - Connection closed at byte 346030080. Retrying.
--2025-09-17 16:52:19-- (try: 2) https://release-assets.githubusercontent.com/github-production-release-asset/129571436/f49b721f-f4dd-4d02-a474-6de64a12b6a6?sp=r&sv=2018-11-09&sr=b&spr=https&se=2025-09-17T14%3A23%3A16Z&rscd=attachment%3B+filename%3Dlean-4.23.0-linux.tar.zst&rsct=application%2Foctet-stream&skoid=96c2d410-5711-43a1-aedd-ab1947aa7ab0&sktid=398a6654-997b-47e9-b12b-9515b896b4de&skt=2025-09-17T13%3A22%3A53Z&ske=2025-09-17T14%3A23%3A16Z&sks=b&skv=2018-11-09&sig=QA4%2B2jA%2Btso6VoRlWzxgdgn00rlpGMov47wkh6EEvbU%3D&jwt=eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmVsZWFzZS1hc3NldHMuZ2l0aHVidXNlcmNvbnRlbnQuY29tIiwia2V5Ijoia2V5MSIsImV4cCI6MTc1ODExNzEyOSwibmJmIjoxNzU4MTE2ODI5LCJwYXRoIjoicmVsZWFzZWFzc2V0cHJvZHVjdGlvbi5ibG9iLmNvcmUud2luZG93cy5uZXQifQ.X0hui6Npl66lSagmPV1Yd3uUiPQuoaqE2wFNoZmAogI&response-content-disposition=attachment%3B%20filename%3Dlean-4.23.0-linux.tar.zst&response-content-type=application%2Foctet-stream Connecting to release-assets.githubusercontent.com (release-assets.githubusercontent.com)|185.199.110.133|:443... connected. HTTP request sent, awaiting response... 618 jwt:expired 2025-09-17 16:52:19 ERROR 618: jwt:expired.
token is expired.
