Zulip Chat Archive
Stream: FLT-regular
Topic: leanproject up
Riccardo Brasca (Apr 21 2022 at 12:44):
It seems that the script that is supposed to update mathlib stopped working, and leanproject up does nothing, at least for me. :thinking:
Eric Rodriguez (Apr 21 2022 at 12:50):
as far as I can see, flt-regular is on the latest mathlib!
Riccardo Brasca (Apr 21 2022 at 12:52):
Yes, I just manually modified the leanpkg.toml file.
Eric Rodriguez (Apr 21 2022 at 12:52):
oh, I see
Riccardo Brasca (Apr 21 2022 at 12:52):
But the script didn't do anything this night (not even opening an issue), and leanproject up didn't work.
Chris Birkbeck (Apr 21 2022 at 12:54):
Weird, the action did run 9 hours ago and didn't show any errors
Chris Birkbeck (Apr 21 2022 at 12:55):
(if im looking at the right action...)
Riccardo Brasca (Apr 21 2022 at 12:56):
The last commit generated by the script that I see is 7ee90eab68eb772bb6df4fa177e8022e09c60c77, two days ago.
Riccardo Brasca (Apr 21 2022 at 12:56):
This already happened (with leanproject, it was the same for all projects), here
Riccardo Brasca (Apr 21 2022 at 12:56):
But I don't know if it is the same thing
Alex J. Best (Apr 21 2022 at 12:58):
Looks like the same thing to me
Alex J. Best (Apr 21 2022 at 12:58):
Probably this script needs restarting every 2 months or something!
Riccardo Brasca (Dec 26 2022 at 19:42):
This happened again, and I forgot what the solution is...
Riccardo Brasca (Apr 21 2022 at 12:44):
It seems that the script that is supposed to update mathlib stopped working, and leanproject up does nothing, at least for me. :thinking:
Eric Rodriguez (Apr 21 2022 at 12:50):
as far as I can see, flt-regular is on the latest mathlib!
Riccardo Brasca (Apr 21 2022 at 12:52):
Yes, I just manually modified the leanpkg.toml file.
Eric Rodriguez (Apr 21 2022 at 12:52):
oh, I see
Riccardo Brasca (Apr 21 2022 at 12:52):
But the script didn't do anything this night (not even opening an issue), and leanproject up didn't work.
Chris Birkbeck (Apr 21 2022 at 12:54):
Weird, the action did run 9 hours ago and didn't show any errors
Chris Birkbeck (Apr 21 2022 at 12:55):
(if im looking at the right action...)
Riccardo Brasca (Apr 21 2022 at 12:56):
The last commit generated by the script that I see is 7ee90eab68eb772bb6df4fa177e8022e09c60c77, two days ago.
Riccardo Brasca (Apr 21 2022 at 12:56):
This already happened (with leanproject, it was the same for all projects), here
Riccardo Brasca (Apr 21 2022 at 12:56):
But I don't know if it is the same thing
Alex J. Best (Apr 21 2022 at 12:58):
Looks like the same thing to me
Alex J. Best (Apr 21 2022 at 12:58):
Probably this script needs restarting every 2 months or something!
Riccardo Brasca (Dec 26 2022 at 19:42):
This happened again, and I forgot what the solution is...
Last updated: Dec 20 2023 at 11:08 UTC