Zulip Chat Archive

Stream: lean4

Topic: Lean should update flake.lock file


view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Apr 08 2021 at 07:32):

Unfortunately there seems to be some linking issue when building Lean against current nixpkgs-unstable

view this post on Zulip 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

view this post on Zulip 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