OpenSSL error in Mathlib CI

Stream: mathlib4

[Geoffrey Irving]

This error message on https://github.com/leanprover-community/mathlib4/pull/10562 seems transient. How do I kick things so that CI reruns? Should I add a fake commit?

Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
OpenSSL SSL_connect: Connection reset by peer in connection to lakecache.blob.core.windows.net:443
2 download(s) failed
Error: Process completed with exit code 1.

[Geoffrey Irving]

Very close to landing this PR I started in February, so I'm eager to get through the last hurdles. :)

[Geoffrey Irving]

Here's the CI run link before I do that fake commit: https://github.com/leanprover-community/mathlib4/actions/runs/10273606381/job/28428433331?pr=10562

[Michael Rothgang]

Can you just re-run the workflow? On the workflow page, after logging in you should see a button "re-run workflows" or so.

[Jireh Loreaux]

@Geoffrey Irving thanks for writing this bound tactic by the way!

[Geoffrey Irving]

New CI run looks healthier.

Now it just needs to build 2500 files since this PR touches Order.Field.Basic and such. :)

[Geoffrey Irving]

@Jireh Loreaux CI is clean! Should we merge now, or wait for the two extra reviewers that @Yaël Dillies requested? (They haven't responded in over a week.)

[Yaël Dillies]

(they are on holiday until the 12th, unless I'm confusing names)

[Geoffrey Irving]

I'm on holiday from the 12th on, for two weeks.

[Geoffrey Irving]

To clarify, if they're on holiday until the 12, and I'm on holiday until the 23rd, should we try to get it in now so that the merge conflicts stop or wait until the end of August to resume?

[Ruben Van de Velde]

Test succeeded: ./testTest failed: `lake env lean ./test/Bound/attribute.lean` produced:
Error: ./test/Bound/attribute.lean:18:6: error: unknown identifier 'Bound.declPriority'
Error: ./test/Bound/attribute.lean:17:0: error: ❌ Docstring on `#guard_msgs` does not match generated message:

error: unknown identifier 'Bound.declPriority'
Error: ./test/Bound/attribute.lean:22:6: error: unknown identifier 'Bound.declPriority'
Error: ./test/Bound/attribute.lean:21:0: error: ❌ Docstring on `#guard_msgs` does not match generated message:

error: unknown identifier 'Bound.declPriority'
Error: ./test/Bound/attribute.lean:26:6: error: unknown identifier 'Bound.declPriority'
Error: ./test/Bound/attribute.lean:25:0: error: ❌ Docstring on `#guard_msgs` does not match generated message:

error: unknown identifier 'Bound.declPriority'
Error: ./test/Bound/attribute.lean:30:6: error: unknown identifier 'Bound.declPriority'
Error: ./test/Bound/attribute.lean:29:0: error: ❌ Docstring on `#guard_msgs` does not match generated message:

error: unknown identifier 'Bound.declPriority'

Probably you need to fix this ^

If you mention that you'll be on holiday, they might be willing to fix any last issues themselves

[Geoffrey Irving]

Oops, thank you, I'd missed that. Should be fixed now. I'll flag that I'll be on holiday on the issue.

[Jireh Loreaux]

I think CI is still failing

[Geoffrey Irving]

I think it's still rerunning after my latest push?

[Damiano Testa]

Looks like it is linting: if you've been diligent adding doc strings, it should be ok!

[Geoffrey Irving]

All passed now.

[Jireh Loreaux]

:tada: