Strange error in "Lint mathlib" check

Stream: new members

[Sebastian Monnet]

I tried replacing some lemma/def arguments with variables in PR #13307, and it seems to have broken something, since the Lint mathlib check is failing. I don't understand the error message, though. It says:

Run set -o pipefail
info: downloading installer
curl: (22) The requested URL returned error: 404
elan: command failed: curl -sSfL https://github.com/leanprover/elan/releases/download//elan-x86_64-unknown-linux-gnu.tar.gz -o /tmp/tmp.B0Iqdr9jt0/elan-init.tar.gz
Error: Process completed with exit code 1.

Does anyone know what this means, or how I can fix it?

[Eric Wieser]

You need to merge master to get some fixes to the CI setup

[Sebastian Monnet]

@Eric Wieser I tried merging from master in VSCode and then syncing, but it doesn't seem to have done anything. I'm not sure whether I did it wrong or not

[Eric Wieser]

The error message is from github not vscode

[Eric Wieser]

You'll need to push after merging and wait to see if it fixes github

[Sebastian Monnet]

Right yeah, I made a new commit after trying to merge from master and it still failed

[Bryan Gin-ge Chen]

I don't see a merge commit on the PR page? Are you sure you pushed the merge commit to GitHub? https://github.com/leanprover-community/mathlib/pull/13307

[Sebastian Monnet]

Bryan Gin-ge Chen said:

I don't see a merge commit on the PR page? Are you sure you pushed the merge commit to GitHub? https://github.com/leanprover-community/mathlib/pull/13307

I am very unsure. What I did was: clicked on the little ... in the "Source Control" of VSCode, went to Branch -> Merge Branch, selected the branch origin/master, made some trivial change to my code so that it let me make a new commit, and then committed it

[Bryan Gin-ge Chen]

Was it this commit? https://github.com/leanprover-community/mathlib/pull/13307/commits/b453a429dce7169742096b202842fd2596c15ca3

If so, it doesn't look like it contains a merge with the latest master. You might have to fetch the latest version of master before merging. git fetch && git merge origin/master is what I usually run from the command line.

[Sebastian Monnet]

It worked! Thank you both