Retry update on empty Lean 3 response in test helper.

Julian / lean.nvim

neovim support for the Lean theorem prover

MIT License

255 stars 25 forks source link

Retry update on empty Lean 3 response in test helper. #255

Closed rish987 closed 2 years ago

rish987 commented 2 years ago

testing...

rish987 commented 2 years ago

Huh, another source of flakiness after this fix is defaulting to no-widget mode (see this run). I think we can just disable widgets in contents_spec.lua?

Julian commented 2 years ago

Sounds fine to me.

rish987 commented 2 years ago

Anyone have an idea why elan isn't downloading in CI anymore?

Julian commented 2 years ago

There's an elan bug that was recently fixed. I didn't read the thread to see what needs happening now for downstream projects, but I suspect it's related. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20install.20elan.20fails.20in.20CI is the thread

Julian commented 2 years ago

Thanks!

rish987 commented 2 years ago

No prob, of course continue to link me to any runs that fail unexpectedly.