References in QuadraticForm and CliffordAlgebra.Contraction

Stream: mathlib4

[Utensil Song]

There are a few empty references in docs#QuadraticForm and docs#CliffordAlgebra.contractLeft , namely:

• [izhakian2016][], which seems to be [Zur Izhakian et al., *Quadratic and symmetric bilinear forms on modules with unique base over a semiring*, Documenta Mathematica 21 (2016): 773-808.][izhakian2016]
• [grinberg_clifford_2016][], which seems to be [Darij Grinberg, *The Clifford algebra and the Chevalley map - a computational approach*][grinberg_clifford_2016]
• [bourbaki2007][], which seems to be [N. Bourbaki, *Elements de Mathematique: Algebre*, Chapitre 9 , Springer 2007][bourbaki2007]

I have 4 questions:

1. Is it better to fill in these references? (I can PR them)
2. Is the style above consistent with Mathlib4's convention about it? (I've tried to be consistent with existing references in Mathlib)
3. Is the raw render of references intended? (This format is not exactly Markdown, so it doesn't render to links, footnotes or anything, just raw brackets with full title and the shot ref)
4. Since the render is raw, what if I wish to add links, particularly for [grinberg_clifford_2016], how should I do it? (Found no precedent in Mathlib)

Sorry for the nitpick, but I always wished for good references in Mathlib, although the actual implementation usually deviates from references in a non-trivial manner (sometimes worthy of a new paper).

CC @Anne Baanen , as the first one is yours.

CC @Eric Wieser, as the last 2 are yours.

[Andrew Yang]

They should be added to the bibfile I think.

[Utensil Song]

Thanks for the pointer, I see, but it seems that the bibfile is not used by doc-gen4 to render the references while doc-gen3 does.

[Ruben Van de Velde]

Yeah, it would be great if Someone(tm) fixed that :)

[Eric Wieser]

I think the idea was that [refname][] would be expanded to the full name by doc-gen4, but obviously that isn't the case

[Eric Wieser]

I'm pretty sure this is actually legal markdown, in the presence of an eventual [refname]: url or similar.

[Utensil Song]

Related: leanprover/doc-gen4#147

It seems not too difficult to adapt the doc-gen3 python script for the purpose, but eventually it needs to generate a Lean file for doc-gen4 to consume.

The more tricky parts would be:

1. to include into doc-gen4, it's preferable to not use Python (doc-gen4 is pure Lean) but only CLI tools and Lean, such adaptation can't reuse the Python script
2. for an outline and referencing, maybe every entry need to be a definition in the Lean file, not just some markdown in comments
3. refer by something like [refname][] could be parsed similar to what's done inextendAnchoror autoLink in DocString
4. doc-gen3 has support for back-referencing, which would need to collect the files/declarations referring to a bib entry.

[Ruben Van de Velde]

Looks like pybtex can convert to yaml. Is there a yaml parser in lean already?

[Utensil Song]

Not that I can find (searched Zulip and Github).

Compared to depending on parsing YAML (likely a FFI to libyaml which is an event-based low-level parser, or simply using parsec as doc-gen4 did with simple xml) or bibfile (many quirks), generating Markdown by pybtex then parse with CMark is more immediately feasible if we only need the list of refnames as metadata.

[Utensil Song]

But if already using pytex, better just choose to depend on the old Python script for now.