search

oliver-butterley / lean-update

The action attempts to update Lean and Mathlib. If an update is available then the updated version is tested. This allows for automatic committing of the updated project, opening PRs or opening issues.
MIT License
6 stars 2 forks source link

Exception calling ".ctor" with "1" argument(s): "The input string '' was | not in a correct format." #39

Closed pitmonticone closed 1 month ago

pitmonticone commented 1 month ago

It returns this error in all projects I've adopted lean-update: https://github.com/ImperialCollegeLondon/FLT/actions/runs/11176285474/job/31069319185#step:3:1.

I'll take a more serious look at it in the next days because I really have no time left.

oliver-butterley commented 1 month ago

This appears a duplicate of issue #37

We closed it with the pr earlier today. Can you try running the action again in the problem repos with the new release?

https://github.com/oliver-butterley/lean-update/issues/37

pitmonticone commented 1 month ago

Oh sorry. Didn't notice.

I'll run them and let you know.

pitmonticone commented 1 month ago

It works fine now. Thanks a lot!

oliver-butterley commented 1 month ago

Thank you for all the testing and feedback