suppress linter during release

Stream: lean4

[Matthew Ballard]

I am testing a version of Lean whose only purpose is to benchmark against mathlib. I would like the GitHub CI to release a toolchain for this modified version.

It expectedly trips the unused variable linter causing the stage 2 portion of the Linux build to fail. This can be fixed but would take a bit more effort. I would like to see if such effort would be worth it, in terms of speed improvements to mathlib, before undertaking it.

Is there a way to suppress the error from this and complete the release process?

[Scott Morrison]

I would like this too, but it would be a substantial refactor of the CI.

[Scott Morrison]

I'm guessing you want speedcenter results here, and can't do your benchmarking with an elan override toolchain (which is much quicker to obtain, and doesn't care about the tests).

[Matthew Ballard]

I took the brutish approach to ci.yml but then noticed there were switches to turn off stage 3 and the benchmarking for the linux build.

I would love to be able to know how to use elan override with the benchmarking server. Due to my MacOS woes, I have been using a tiny linux box with elan override for quicker iterations. But I was not aware of being able to point the benchmark server to an overriding toolchain