Zulip Chat Archive

Stream: general

Topic: mathlib4 links in mathlib3 docs

Yury G. Kudryashov (Jul 02 2023 at 21:54):

@Rob Lewis @Eric Wieser @Gabriel Ebner Is it hard to add mathlib4 links to mathlib3 docs using #aligns?

Anatole Dedecker (Jul 02 2023 at 21:55):

Oh that would be great

Scott Morrison (Jul 02 2023 at 23:25):

Why would this be useful?

Yury G. Kudryashov (Jul 02 2023 at 23:29):

Someone follows an old link pointing to mathlib3 docs and can jump to mathlib4 def/lemma in 1 click.

Scott Morrison (Jul 02 2023 at 23:30):

I see, links from older zulip discussions, I hadn't thought of that.

Henrik Böving (Jul 03 2023 at 05:09):

(deleted)

Henrik Böving (Jul 03 2023 at 05:09):

So you want to parse Lean 4 in the Lean 3 tool now?

Mario Carneiro (Jul 03 2023 at 05:15):

I think it would be most reasonable to have a basic lean4 project which does import Mathlib and exports the #align database as a json file which is imbibed by lean 3 docgen

Johan Commelin (Jul 03 2023 at 05:24):

Even grep could get you 99% there, because 99% of #align statements are flushleft on a single line.

Mario Carneiro (Jul 03 2023 at 05:29):

yeah but that's not bringing us any closer to mathport-lint

Last updated: Dec 20 2023 at 11:08 UTC