Zulip Chat Archive

Stream: FLT-regular

Topic: Mathlib PRs

Andrew Yang (Nov 17 2023 at 17:58):

#8464 moves multiset-relating lemmas by Ruben

Ruben Van de Velde (Nov 17 2023 at 22:32):

And #8486 for UFDs

Riccardo Brasca (Nov 18 2023 at 00:40):

I will have a look at this tomorrow if it still open.

Riccardo Brasca (Nov 18 2023 at 00:41):

BTW @Chris Birkbeck we have a red X on github about "build documentation". Is this the blueprint?

Chris Birkbeck (Nov 18 2023 at 08:47):

Hmm yeah it is. The blueprint still seems to be working, but I will have a look and see if I can figure out what the problem is.

Andrew Yang (Nov 18 2023 at 08:49):

I might have removed the proof of 5.1 in that PR. This might be the problem?

Chris Birkbeck (Nov 18 2023 at 08:50):

I don't see why that would be a problem, but who knows.

Ruben Van de Velde (Nov 18 2023 at 10:14):

Does the blueprint verify that the lean statements you link to actually exist?

Chris Birkbeck (Nov 18 2023 at 10:16):

Good question. I used to not do that, but maybe now with the doc-gen thing it does.

Chris Birkbeck (Nov 20 2023 at 10:31):

I can't quite figure out what the problem is. I tried undoing the change to the blueprint, but it didn't work. Maybe @Utensil Song can spot what the problem is? It seems to be breaking while building the documentation see here

Mauricio Collares (Nov 20 2023 at 10:36):

You need to bump the doc-gen4 dependency (just running lake update and committing the manifest changes should be enough)

Mauricio Collares (Nov 20 2023 at 10:36):

This was fixed in leanprover/doc-gen4#164 (yes, there are "fix: " commits there too)

Chris Birkbeck (Nov 20 2023 at 10:40):

Ok great, I'll try that, thank you!

Chris Birkbeck (Nov 20 2023 at 11:18):

hmm ok now it failed further along. During the copy documentation step, saying mv: cannot stat 'build/doc': No such file or directory.

Mauricio Collares (Nov 20 2023 at 11:20):

I guess build/doc is now .lake/build/doc

Mauricio Collares (Nov 20 2023 at 11:21):

(in push.yml)

Chris Birkbeck (Nov 20 2023 at 11:22):

oh ok, let me try that now :)

Riccardo Brasca (Nov 20 2023 at 12:08):

It worked, thanks!

Chris Birkbeck (Nov 20 2023 at 12:09):

oh great! thank you!

Yaël Dillies (Nov 20 2023 at 12:15):

If you need any help with your blueprint, I'm here as well.

Andrew Yang (Nov 27 2023 at 19:50):

List of currently open Mathlib PRs:
#8625 (delegated)
#8639 (needs fix)
#8641
#8645
#8651
#8653
#8654
#8657

Riccardo Brasca (Nov 27 2023 at 20:36):

I've left a couple of comments.

Ruben Van de Velde (Nov 28 2023 at 10:16):

I'll push a bump in a few minutes

Last updated: Dec 20 2023 at 11:08 UTC