Zulip Chat Archive

Stream: FLT-regular

Topic: gen_dvd_by_frak_p

Riccardo Brasca (Jul 19 2023 at 15:47):

@Chris Birkbeck can you have a look at this issue? Otherwise I will do it tomorrow.

Chris Birkbeck (Jul 19 2023 at 22:40):

Yes there's a typo in the statement of the lemma, I'll try and fix it now :)

Chris Birkbeck (Jul 20 2023 at 02:48):

Ok I need to figure out how to recompile the blueprint again. I tried fixing the github action that did it (copying the fix from LTE) but it didn't work. I'll try again tomorrow or just do it manually.

Riccardo Brasca (Jul 20 2023 at 07:02):

It's not so important, we are switching to Lean 4 soon anyway

Riccardo Brasca (Jul 20 2023 at 07:02):

And I guess everything will be different

Chris Birkbeck (Jul 20 2023 at 12:16):

Thats a good point, will our blueprints link with lean 4? It should be fine I guess.....

Riccardo Brasca (Jul 20 2023 at 14:58):

I have no idea, but I guess something will break. Also CI and stuff like that will break for sure.

Andrew Yang (Sep 26 2023 at 11:58):

Is there anyone working on this lemma now?
If not, I'd like to give it a go.

Eric Rodriguez (Sep 26 2023 at 12:04):

I doubt anyone is working on much stuff right now, I'd just go for it!

Chris Birkbeck (Sep 26 2023 at 12:27):

No go for it. I do plan on updating the blueprint soon, but need to figure out how it'll work with lean 4

Riccardo Brasca (Sep 26 2023 at 14:40):

@Andrew Yang thanks a lot for your PR!! The compilation time is divided by 4 on my computer :tada:

Last updated: Dec 20 2023 at 11:08 UTC