correcting typo in mathlib4 (and 3?)

Stream: new members

[Malvin Gattinger]

I noticed a broken documentation link in Mathlib.Data.List.BigOperators.Basic in both mathlib 3 and 4. I would like to use the occasion to learn how to contribute. Should I make a single PR to mathlib4 or do I need to make one for mathlib3 as well?

[Eric Wieser]

There is no need to make one for mathlib3 unless you really want to

[Eric Wieser]

Mathlib 3 is effectively frozen

[Malvin Gattinger]

ok, thanks :)

[Notification Bot]

Malvin Gattinger has marked this topic as resolved.

[Anatole Dedecker]

@Malvin Gattinger do you already have push access to non-master branches of mathlib4? If not, that will be required for the PR process.

[Malvin Gattinger]

Oh. I don't know and therefore probably don't have it ;) I realise now I should have read https://leanprover-community.github.io/contribute/index.html before creating https://github.com/leanprover-community/mathlib4/pull/7350

[Anatole Dedecker]

I just sent you an invitation (sorry for the delay). Indeed you have to open the PR again from a mathlib branch so that CI can run.

[Yaël Dillies]

Does it really matter if CI runs given that this is a docs-only PR?

[Anatole Dedecker]

I think "CI" in my sentence above includes bors, so unless we bypass it completely it's probably better to open a PR from a branch

[Yaël Dillies]

I'd be highly surprised if bors can't be run on fork PRs. After all, that's the model most non-mathlib projects use.

[Anatole Dedecker]

Yes but I think you have to explicitly enable that, and I think we haven't. But I'm no expert so we can try :shrug:

[Yaël Dillies]

I also think we could just merge right away here. There's little risk we mess up the syntax.

[Ruben Van de Velde]

Bors should support it fine

[Anatole Dedecker]

We want to run bors in any case in order to generate a cache right? Or is cache smart enough to work around that for documentation commits?

[Yaël Dillies]

Uh actually I don't know. I'd have expected CI to run anyway, just not through bors first.

[Malvin Gattinger]

Uh, sorry for causing the confusion, and thanks @Anatole Dedecker for the permissions! As for the suggestions by @Yaël Dillies , do you know for sure that relative links/paths will work? Is there a way to run the HTML generator locally to try it out?

[Yaël Dillies]

Yes, I've made relative paths work before. Or rather I made them work with doc-gen, not doc-gen4.

[Yaël Dillies]

There exists a doc-gen visualiser, but I'm pretty sure it doesn't support doc-gen4 yet.

[Malvin Gattinger]

Ok, I adopted the suggestions. Should I still move it to a branch in leanprover-community instead of my own fork or do you want to merge it like this? (Would the CI run also provide a preview of the docs?)

[Yaël Dillies]

I'm happy to merge like this.

[Notification Bot]

Malvin Gattinger has marked this topic as unresolved.

[Malvin Gattinger]

I fear the relative paths still don't work. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/BigOperators/Basic.html now has a link with Defs instead of defs, but doc-gen4 seems to turn the ./Defs into ../../../../././Defs which is https://leanprover-community.github.io/mathlib4_docs/Defs and 404.

[Eric Wieser]

Arguably this is now a doc-gen problem not a mathlib problem

[Malvin Gattinger]

Ah. Nice occasion to read some code. I guess this is the place that converts module names to HTML links, and it will always add getRoot to make the path absolute? https://github.com/leanprover/doc-gen4/blob/96870507c50b43fc5ad744914f9718307fe7724a/DocGen4/Output/Base.lean#L115

[Ruben Van de Velde]

Fwiw, just Mathlib/Foo/Bar.lean is now linked automatically

[Eric Wieser]

The logic is here

[Eric Wieser]

So this is deliberate but it's not clear it's desirable