windows nightly link broken

Stream: general

[Kevin Buzzard]

https://ci.appveyor.com/api/projects/leodemoura/lean/artifacts/build/lean-nightly-windows.zip?branch=master (the usual link to lean nightly windows) doesn't work currently -- I mean the link doens't work, rather than the zip file not compiling.

[Kevin Buzzard]

There are issues with the Windows build infrastructure (as spotted by one of my students last night who was hoping to get the new non-leaky Lean). https://github.com/leanprover/lean reports the build as passing in the readme, the link in the readme seems to report it as failing, and the link at https://leanprover.github.io/download/ to the windows nightly is still failing with the error {"message":"\"job\" parameter must be specified if build contains multiple jobs.\r\nParameter name: job"}

[Sebastian Ullrich]

The new link is https://ci.appveyor.com/api/projects/leodemoura/lean/artifacts/build/lean-nightly-windows.zip?branch=master&job=Environment%3A%20CFG%3DMINGW64. Hopefully I can deploy the new nightly infrastructure in the next few days so that this won't matter.

[Kevin Buzzard]

I know Lean is a project not a product, but the link to Windows nightlies on the official download page https://leanprover.github.io/download/ currently doesn't work for me. I think Sebastian once told me how to fix this but I forgot. The issue is that I simply don't know where any windows nightlies are any more. At https://github.com/leanprover/lean-nightly/releases there seems to be no Windows nightlies either. Where, if anywhere, is the current Windows nightly?

[Kevin Buzzard]

I just told someone about Lean and they said "it's crap, the windows download doesn't even work". Nice.

[Sebastian Ullrich]

@Kevin Buzzard I updated the nightlies link to the new releases page... which doesn't help for Windows until AppVeyor get their shit together and enable cron builds for us :angry:

[Sebastian Ullrich]

Okay, I've manually triggered a Windows build of the latest nightly

[Simon Hudon]

I don't understand why you need cron for that. Doesn't the commit trigger a build on AppVeyor?

[Kevin Buzzard]

That is a fine fix Sebastian. Thanks!

[Kevin Buzzard]

And we're back to having downloads for all three of the OS's supported by Lean. Hooray!

[Sebastian Ullrich]

@Simon Hudon Sure, but we don't want a release for every single commit

[Simon Hudon]

Ah so you have a daily build that creates the daily, is that it? What do you do if there haven't been any commits since the last time?

[Sebastian Ullrich]

Not pushing a build, obviously :smile: . We already need to compare against the previous build for the change log anyway.

[Simon Hudon]

Cool :)