Guilherme Silva (Apr 07 2021 at 22:11):
The old Nixpkgs in Lean is making a download in the old link of the visual studio:
I have this error when running
nix build github:leanprover/lean4#vscode-dev
error: builder for '/nix/store/pmhj1v7jz7vkr8iccsq352w57gfhsc3c-VSCode_1.52.1_linux-x64.tar.gz.drv' failed with exit code 1; last 7 log lines: > > trying https://vscode-update.azurewebsites.net/1.52.1/linux-x64/stable > % Total % Received % Xferd Average Speed Time Time Time Current > Dload Upload Total Spent Left Speed > 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 > curl: (22) The requested URL returned error: 404 Not Found > error: cannot download VSCode_1.52.1_linux-x64.tar.gz from any mirror For full logs, run 'nix log /nix/store/pmhj1v7jz7vkr8iccsq352w57gfhsc3c-VSCode_1.52.1_linux-x64.tar.gz.drv'.
I saw that @Sebastian Ullrich was the last that changed this file on GitHub.
I can do a pull request too.
Sebastian Ullrich (Apr 08 2021 at 07:32):
Unfortunately there seems to be some linking issue when building Lean against current nixpkgs-unstable
Guilherme Silva (Apr 08 2021 at 12:50):
I made a pull request fixing this issue:
In my forked version, this command works
nix build github:guilhermehas/lean4#vscode-dev
Sebastian Ullrich (Apr 08 2021 at 13:01):
The PR fails with the same error. It probably only happens when ccache is set up.
Last updated: May 18 2021 at 22:15 UTC