stacks tags

Stream: general

[Johan Commelin]

Top 35, with labels

00DV 119 algebra-lemma-NAK
01ZM 69 limits-lemma-descend-finite-presentation
02KH 64 coherent-lemma-flat-base-change-cohomology
06Z0 61 perfect-lemma-affine-compare-bounded
03H4 57 spaces-properties-lemma-points-cartesian
01XB 48 coherent-lemma-quasi-coherent-affine-cohomology-zero
00NX 47 algebra-lemma-finite-projective
01UA 46 morphisms-lemma-fppf-open
0149 41 derived-lemma-representable-homological
00DS 41 algebra-lemma-silly
01LC 40 schemes-lemma-push-forward-quasi-coherent
00E0 40 algebra-lemma-Zariski-topology
00MB 39 algebra-lemma-completion-flat
00EU 37 algebra-lemma-minimal-prime-reduced-ring
01T6 36 morphisms-lemma-finite-type-noetherian
00XR 36 sites-lemma-when-shriek
00U2 36 algebra-lemma-etale
03H6 34 spaces-properties-lemma-quasi-compact-affine-cover
01W6 34 morphisms-lemma-image-proper-scheme-closed
00NQ 34 algebra-lemma-regular-ring-CM
01Z4 33 limits-lemma-descend-opens
00HN 32 algebra-lemma-characterize-zero-local
001P 32 categories-lemma-yoneda
08J5 31 derived-remark-truncation-distinguished-triangle
01T2 31 morphisms-lemma-locally-finite-type-characterize
00KW 31 algebra-lemma-one-equation
07SK 29 spaces-limits-lemma-descend-finite-presentation
01WM 29 morphisms-lemma-integral-universally-closed
01U9 29 morphisms-lemma-base-change-flat
015J 29 derived-lemma-two-ss-complex-functor
04XB 28 stacks-properties-section-properties-morphisms
04KF 28 spaces-properties-lemma-describe-etale-local-ring
01WN 28 morphisms-lemma-finite-proper
00HL 28 algebra-lemma-flat-tor-zero
00HI 28 algebra-lemma-flat-base-change

[Johan Commelin]

A brief glance, we have NAKayama, yoneda, Zariski-topology. Most of the rest seems quite far away.

[Rob Lewis]

Johan Commelin said:

I think the chance that old tags rot is very small. So the main issue is that new things should get tagged. This will have to be a community effort. But I think it's ok if we do it in bursts.

But like you said there are a lot of stacks tags, and there are a lot of contributors here who don't know the project. How do these bursts work? Read all the stacks tags and remember what's been added to mathlib since the last iteration? Or look at a month of mathlib commits and see which ones might have corresponding tags?

[Rob Lewis]

Is there any chance of a new stacks tag that corresponds to something already in mathlib?

[Johan Commelin]

I think the latter chance is very small (but increasing?!)

[Johan Commelin]

Those bursts would have to be done by the algebraists in our community. Look through ring_theory/ and algebraic_geometry/ for lemmas that don't have @[stacks] but for which you expect that SP will have a tag for it.

[Rob Lewis]

Johan Commelin said:

I think the latter chance is very small (but increasing?!)

Do old tags ever get split? Like, ABC gets expanded and a lemma becomes DEF? That seems like the more likely way for this to happen.

[Johan Commelin]

They make a very strong effort to never change the statement of a tag (apart from cosmetic changes).

[Johan Commelin]

So if there is a split, my guess is that you'll get two new tags, and the old one will be "deprecated" (but still point to the old result, but not show up in their most rendering of the website)

[Rob Lewis]

Right, so if ABC is in mathlib and gets split into DEF and GHI, then DEF and GHI are new tags that are likely in mathlib

[Rob Lewis]

So you need to track changes on their end as well as ours

[Johan Commelin]

I think they maintain a list of deprecated tags. So part of a "burst" could be to check against that list.

[Johan Commelin]

#003W,categories-equation-fibred-groupoids-commutes
#003X,categories-equation-fibred-groupoids-commutes2
#Taken out as an exact duplicate of 00CR
#00DU,algebra-lemma-localize-colimit
#This equation was in a second proof 00EE which we removed
#00EL,algebra-equation-idempotent-exact-sequence
#Replaced proof by a new one avoiding this equation
#013L,derived-equation-new-star
#013M,derived-equation-star-star
#013Z,derived-remark-failure
#014T,derived-section-derived-triangulated
#014U,derived-definition-derived-triangulated
#0155,derived-lemma-ses-injective-ses
# Equations for relations between maps no longer needed because of
# vastly improve proof of Lemma Tag 01A6
#01A7,simplicial-equation-cd
#01A8,simplicial-equation-cs
# Changed coherent-remark-base-complex into lemma
# Changed coherent-remark-hypercoverings into lemma
#The following tag referred to a technical question whose answer is now in the
#stacks project, namely, it is answered by (the new version of) 01ZH
#01ZI,limits-remark-question-finite-type-necessary
# This section got moved to properies.tex
# This affects tags 01ZU, 01ZV, 01ZW, 01ZX, 01ZY

[Johan Commelin]

All the commented out tags are deprecated. :up: is the first chunk of about 100 such lines that grep found for me in tags/tags

[Rob Lewis]

So I'm not saying "don't do this," just trying to emphasize that this is a sustained maintenance effort that needs someone to lead the charge. Otherwise infrastructure will be built and forgotten and there will be a bunch of incomplete and outdated noise floating around.

[Kevin Buzzard]

OK I'll do it.

[Kevin Buzzard]

Stacks is becoming a canonical reference for commutative algebra for the young -- even the "standard" textbooks like Matsumura and Atiyah-Macdonald seem to be going out of fashion, because Stacks is online and looks beautiful, much better than the dodgy illegal pdfs (sometimes not even OCR'ed) which the UGs have of the classic books.

For me, moving into commutative algebra is a very natural next step for mathlib. Avigad has always pointed out how Lean is really dominating when it comes to algebra. Isabelle is still way ahead on analysis and of course Coq has the odd order theorem, however the odd order theorem is tons of lemmas about finite groups and some basic undergraduate representation theory, and this does not really add new users. If you look at what is coming out way, it's mathematicians appearing out of nowhere saying things like "let's do regular rings" or "let's do flat modules". Stacks is a perfect blueprint for this stuff.

I know the material well enough to even start breaking stuff up into "mini-projects", and I can probably be trusted to be diligent enough to make sure that things aren't broken. Disadvantages: I can't do any computer things. But I think that if the buck stops with me then this will be good enough for me to at least take responsibility for problems.

[Rob Lewis]

Another thing I mentioned when we talked about this a while back. This is a big human-curated formal-informal alignment, the ML people here should be drooling at the idea. It would probably be helpful to have a story for things that don't align perfectly -- humans can adapt easily enough, maybe machines could use something systematic?

[Johan Commelin]

I agree that we could try to at least have a bool that tracks whether things "obviously don't line up perfectly". But as you point out, since the definition of $\mathbb{N}$ doesn't line up, that basically means that almost everything that follows is infected by that virus.

[Johan Commelin]

So that bool should be applied with a bit of human wisdom...

[Kevin Buzzard]

One issue which I discovered recently is that when Bhavik was working on sheaves taking values in a general category, he had to cite things like "Stacks, remark between tag X and tag Y". For me the natural number thing is right now just noise. I know this sounds weird but actually the natural numbers in some sense do not show up much in this kind of mathematics. I took a good look through stacks when this convention was pointed out a few months back, and most of the uses of naturals just seemed to be as an arbitrary countably infinite index set. One of the few times naturals do show up as as dimensions of schemes, and certainly there are 0-dimensional schemes, so all that will be happening is that Stacks will sometimes say Z_{>=0}. We can translate this, as long as I'm overseeing stuff.

[Johan Commelin]

I guess we can make PRs to Stacks that add labels to "remark between tag X and tag Y", or rewrite that part of stacks to make things slightly more explicit. My guess is that Johan will be happy to receive such PRs.

[Kevin Buzzard]

I think we need to talk to Pieter Belmans about this (he's at Bonn, the same place as Scholze, so this is cool).

[Kevin Buzzard]

I had rather hoped that this term would be a bit quieter, but preparing my course has taken a lot of my time. It's over in three weeks though.

[Patrick Massot]

It reminds me: did we settle the crazy $\pi_0$ issue? I don't care what the Stacks project thinks here, there is now way we can keep the notation and name $\pi_0$ for something related but different from what the whole universe but the Stacks project calls $\pi_0$.

[Johan Commelin]

@Patrick Massot yes, that got fixed

[Johan Commelin]

It's now called connected_components

[Pieter Belmans]

Kevin Buzzard said:

I think we need to talk to Pieter Belmans about this (he's at Bonn, the same place as Scholze, so this is cool).

I'm now here! And my only interactions with Peter have been when I was in his way to the coffee machine, or he was in my way to the tea kettle, so don't read my association to Bonn in any way :)

[Kevin Buzzard]

So we think we have enough commutative algebra and category theory now to start thinking more seriously about integration of mathlib with the stacks project.

[Kevin Buzzard]

We've needed to do a bunch of category theory to get the definition of a condensed abelian group, and people followed the stacks project to do some of this; also commutative algebra is slowly but surely appearing (e.g. we have lots of facts about Jacobson rings and the NSS, with more in the pipeline) so maybe it's time to think about how to actually do this.

[Kevin Buzzard]

Right now at our end we are considering adding a stacks project attribute which we can attach to definitions and lemmas, pointing people to the corresponding stacks project tag.

[Johan Commelin]

and documentation tools could use the attribute to generate a dictionary json or such

[Kevin Buzzard]

One issue that showed up is this, a reference to a diagram here which didn't have a tag.

[Pieter Belmans]

it's really easy to assign a new tag to a useful equation which currently does not have one, and we should be able to convince Johan of this

[Kevin Buzzard]

If we are going to start doing something at our end, I guess it would be good to know whether you think it might be useful at your end, or at least usable if you want to use it in some way. I guess the dictionary could e.g. relate stacks tags to links to the mathlib API. Is there any particular thing which you want want to see or hope to see or whatever?

[Pieter Belmans]

that's not so much a question for me per se, but more for Johan: I don't know what kind of mathlib integration he foresees

[Pieter Belmans]

when I say Johan, I mean not this Johan, but the other Johan

[Pieter Belmans]

but I think having a visual clue about which tags have been formalised, and having a link to the mathlib documentation, seems like a good thing that I hope I can convince the other Johan of

[Pieter Belmans]

I don't quite know what the analogue of a tag is in mathlib, but having a uniform way of saying "this thing here corresponds to tag 0000" should be enough to allow for scraping the source code, and then we can set up a dictionary from that

[Rob Lewis]

The easy (from our end at least) kind of "integration" is just cross referencing. For various reasons it seems simpler to store the correspondences on the mathlib side, and then it's very simple to generate a map from mathlib declarations (or files, or locations in the docs) to stacks tags.

[Johan Commelin]

Yes, that's exactly what those attributes will do. Although it will quite likely be a many-to-one dictionary. With 5 mathlib declarations working together to get one Stacks tag.

[Rob Lewis]

I don't know if the correspondences are one-to-one or many-to-many or what.

[Johan Commelin]

For example "The following are equivalent" are typically broken into pieces in mathlib.

[Pieter Belmans]

yes, exactly, I think mathlib is the more unstable thing, and the arity of the correspondence is I guess the major thing to understand

[Pieter Belmans]

so the Stacks project website (or some overlay, or some separate website) could do several things:

• show that there is some kind of relationship between tags and mathlib code, without a serious commitment
• really commit to showing certain results

[Rob Lewis]

We have a reasonable API right now for getting a "display version" of a theorem statement. See https://leanprover-community.github.io/100.html , that's generated from https://github.com/leanprover-community/mathlib/blob/master/docs/100.yaml

[Rob Lewis]

So if you wanted to really display the formal statements (on the main website or another, whatever), it's easy to set up.

[Pieter Belmans]

here (or rather on some place like https://leanprover-community.github.io/mathlib_docs/ring_theory/nullstellensatz.html) you could easily add a link to the Stacks project website I guess, based on some decoration of the code, that is one thing

[Pieter Belmans]

I don't know whether Johan wants to display anything more than just a link on the Stacks project website

[Rob Lewis]

Right, we would definitely do that and it's pretty trivial to set up.

[Pieter Belmans]

one issue from the Stacks project POV is synchronisation: how and when will the website update, when updates to mathlib happen

[Pieter Belmans]

but I guess with some continuous integration magic (that you seem to have set up anyway) you can create say a JSON file with the up-to-date information, and that can be read by the Stacks project infrastructure

[Pieter Belmans]

so I'm imagining a single file giving a tag and then a file + line number + method name, and that would be the first thing for mathlib integration in the Stacks project website

[Pieter Belmans]

in the table of contents (see e.g. https://stacks.math.columbia.edu/tag/073W and expand) we can add an icon, indicating that there is a mathlib implementation (see the indication of a slogan on tag 074W)
on the page of a tag (see e.g. https://stacks.math.columbia.edu/tag/074W) we can have the precise link to mathlib

[Rob Lewis]

Pieter Belmans said:

so I'm imagining a single file giving a tag and then a file + line number + method name, and that would be the first thing for mathlib integration in the Stacks project website

Probably a list of files + line numbers + declaration names, but yeah! How often do you see the Stacks project infrastructure retrieving the database from our end?

[Pieter Belmans]

right now we are loading and caching an RSS file for the blog posts and GitHub commits once every hour or day

[Pieter Belmans]

I can check the precise caching settings, but I'd imagine something similar here: hitting it for every request is nonsense :)

[Pieter Belmans]

RSS cache is cleared once per hour

[Rob Lewis]

If the name of a tagged declaration in mathlib changes, links to the mathlib docs will break until you resync. But I guess this won't happen too often? We can handle declarations that move to a new file but keep the same name.

[Rob Lewis]

Links to the source code on github can point to a specific commit, so those can be stable.

[Pieter Belmans]

but any such change would trigger a rebuild of that particular file (i.e. the dictionary file), no?

[Rob Lewis]

Right, but links will be broken until you pull the new dictionary.

[Rob Lewis]

It's a rare event and the broken links won't last long so I'm not too worried about it.

[Pieter Belmans]

we'd only cache that for an hour or so, so I don't worry about those things being out of sync; the Stacks project is popular, but not _that_ popular that there'd be many confused people

[Rob Lewis]

@Johan Commelin @Kevin Buzzard is the mathlib-stacks correspondence many-to-one or many-to-many?

[Rob Lewis]

And is it necessary to have tags in module docs? Or only declarations?

[Rob Lewis]

If it's only declarations, I think it's probably better to use an @[stacks "ABC"] attribute to avoid making up and parsing new markdown syntax.

[Kevin Buzzard]

Sorry, I'm about to start a meeting. We could force it to be one-to-one but this would probably be a bad idea. One of the lemmas we formalised when doing schemes was a lemma about basic ring theory which had 22 parts (which became 22 lemmas in our project) and then said "..." afterwards!

[Kevin Buzzard]

On the other hand I am struggling to think of one definition or theorem in mathlib which could genuinely be tagged with more than one tag.

[Bryan Gin-ge Chen]

I think we will end up mentioning Stacks tags in module docs and docstrings even if we have the attributes, so we should have some convention for those citations too.

[Bhavik Mehta]

Kevin Buzzard said:

On the other hand I am struggling to think of one definition or theorem in mathlib which could genuinely be tagged with more than one tag.

The closest which comes to mind for me is this lemma, which is a generalisation of both https://stacks.math.columbia.edu/tag/0073 and https://stacks.math.columbia.edu/tag/00YR (a), in particular the former talks about sheaves on a space taking values in a nice concrete category, and the latter talks about sheaves on a site taking values in the same nice concrete category but with an extra assumption on it; whereas the Lean version talks about sheaves on a site taking values in a concrete category without the extra assumption

[Ruben Van de Velde]

So should the generalization get its own stacks tag?

[Pieter Belmans]

I don't think it makes sense to modify the Stacks project in such a way, based on a quickly developing formalisation project
it makes sense to take certain cues (e.g. to make referencing easier, adding tags for equations and informal discussions), but anything beyond that you will have a very hard time convincing Johan of

[Bhavik Mehta]

Yeah, I think for the sake of exposition the way Stacks does it right now is sensible - https://stacks.math.columbia.edu/tag/0073 is in the context of talking about sheaves on a space, and the part of https://stacks.math.columbia.edu/tag/00YR which is relevant is the first part in a series of six statements, where only the first doesn't need the extra assumption

[Kevin Buzzard]

I certainly agree that asking de Jong to change any of the exposition would be a very bad idea. "Can you please split this lemma into two because of some formaliser people" means having to go through everywhere where the lemma is used and understanding the mathematics again and then deciding how to rephrase stuff. I think that we have the flexibility to write our own library so that the correspondence is a simple one-tag-to-many-defs/theorems.

[Kevin Buzzard]

Here is tag 00E0 -- this should definitely not be one lemma in Lean!

[Kevin Buzzard]

Kenny proved all 17 statements though in our preliminary formalisation of the definition of a scheme.

[Pieter Belmans]

some of the issues you encounter here, such as this monstrosity lemma with 17 parts, are only happening at the beginning of the Stacks project: the stuff that an algebraic geometer likes to get away with in order to get cracking with the geometry

[Pieter Belmans]

(I have no idea how Stacks-aware people are, if I'm stating too many obvious things in my desire to explain the Stacks project, please tell!)

[Kevin Buzzard]

there are people here ranging from professional algebraic geometers to people doing post-docs in computer science topics who know a lot about mathlib documentation but have probably never even been to the stacks project website and don't know any alg geom at all, so feel free to say obvious-to-some-people things.

[Damiano Testa]

Would it make sense to prove lemmas in mathlib style, and, once a literal stacks statement can be proved, simply add that result in? In the 17 example above, after the 17 lemmas, prove another one that is simply the conjunction of the previous 17? This way, we can keep a 1-1 correspondence to something stable...

[Kevin Buzzard]

This is another possibility but, just as the stacks people will not want to change their 1 lemma into 17 lemmas because of the mathlib people, I don't think that the mathlib people will want a conjunction of 17 lemmas just because of the stacks people. Both communities are right now extremely successful in their own ways and one reason I believe for this is the extremely high level of attention which everything gets -- as you will know if you ever tried to PR one lemma and had about 5 people suggesting alternative proofs, putting it in a different namespace, a different file, adding three more lemmas, and actually perhaps completely refactoring something else so your lemma would not be necessary. I think it's best to not try and change either side of things and instead just do the best we can to show that they are doing related things.

[Kevin Buzzard]

An alternative approach is to start a new repo stacks-in-lean which does have these horrendous conjunctions in and has mathlib as a dependency, but for me this seems to be a far more painful solution -- it will need constant maintenance, for example, and in practice if someone wants to see a lemma which really _is_ directly in mathlib (and of course this sort of thing will happen a lot) they don't really want to be sent to some random other repo with mathlib as a dependency.

My gut feeling is that actually one should be liberal here. If there is a tag X in stacks which is mathematically trivially covered by e.g. the union of three lemmas in mathlib then those lemmas should get given the @[stacks X] attribute and also probably docstrings saying what they do in a way which a mathematician would understand.

[Kevin Buzzard]

@Rob Lewis I can envisage the following situation: stacks tag X proves lemma L assuming some ultimately superfluous extra hypothesis, and then using lemma L it proves in tag X' the correct lemma L' without the superfluous hypotheses. Mathlib uses a totally different approach so doesn't need to go via L. Nobody wants to see L in mathlib because there is no point. So now we want to tag our lemma L' with both stacks tag X and X', and perhaps explain in a comment or docstring why tag X leads to a proof which is strictly stronger than what is stated in X.

Also it is kind of clear that not all tags need to be formalised in mathlib. There might be useless intermediate lemmas proved in Stacks which are never used again other than in the proof of a bigger theorem, and the mathlib proof of the bigger theorem is different and doesn't go via the lemma. So a naive "we're not done until all the tags are formalised" approach is not right.

For me the main aim is not getting an AI to learn stacks via mathlib, and my impression is that AI stuff is happy to be sloppy anyway (cf Szegedy's comment that he doesn't care at all that the naturals start at 1 in stacks and 0 in Lean because it's all heuristics anyway). For me the aim is to see if this helps with search in stacks, which to be honest I find very poor. Example : where is the definition of an affine scheme? . But maybe this is a lousy example because affine schemes are probably everywhere in stacks.

[Damiano Testa]

Kevin, I agree. I think that being liberal in the referencing is perfectly ok and in fact, desirable. If a mathlib statement proves a commutative algebra assuming comm_semiring, while the one in stacks is about a comm_ring, I think that it is more than fair that they get the same tag!

[Damiano Testa]

In fact, should we call these... "stags"?

[Scott Morrison]

It sounds like we came to the conclusion that it is pretty close to a many(mathlib)-to-one(stacks), relationship, but possibly with some exceptions.

[Scott Morrison]

I remember in the elementary category theory stuff finding quite a few cases of misalignments, often when mathlib proved "the main part" of a stacks tag but omitted some minor point.

[Scott Morrison]

I'd propose that we be open to including these as cross references. Ideally on the mathlib side there will be a link back to the stacks tag along with a note "we don't do part e" or similar.

[Bryan Gin-ge Chen]

After the current doc-gen PR is merged, I'm planning to collect all the Stacks tag URLs / other tag-like patterns in docstrings and display those in a special section of the references page.

As I said above, even if we have attributes, we'll still be mentioning Stacks tags in the docstrings, so this effort should be complementary to whatever we decide for the stacks attribute.

[Mario Carneiro]

Why not something like @[stacks "01AB" "part (a,b,c)"] if we really want to keep track of sub-tag tracking in a machine readable way, and

/-- Foos the bar. Stacks project 01AB, part (a,b,c) -/
@[stacks "01AB"]
def ...

otherwise

[Damiano Testa]

In line with this stream, I updated one of my files to add an explicit reference to the Stacks Project. This is another one of those cases where I proved a part of the statement, but not the whole lemma.

PR #6322

[Pieter Belmans]

@Kevin Buzzard to find the definition of an affine scheme using the search, it is but a small thing to search for 'affine scheme definition' and limit yourself to statements (see https://stacks.math.columbia.edu/search?query=affine+scheme+definition&radius=statements): the name of the LaTeX environment is also being used in the plaintext search, and now the first result is indeed the definition of an affine scheme :)

[Kevin Buzzard]

I think that we still need to do some thinking about exactly what data we want to be collecting here. Right now I like Mario's suggestion. I also think that perhaps I was hasty yesterday saying "who cares about the machine learning people, let's just try and make killer search for theorems". I need to spend some time looking at all the examples we have, also also things we don't have but which I would see as minor success stories (e.g. proving some standard theorem about schemes which all alg geometers know, even if it's a standard basic one) and trying to imagine what the mathlib version would actually look like. So my gut feeling right now is just to start off with some detailed notes about what the actual correspondence between the two databases looks like. I am unlikely to find the time to do this before teaching finishes, which is in just under three weeks. @Scott Morrison I think you might have already tried something like this. Is there even some branch, which perhaps was already mentioned?

[Ruben Van de Velde]

A bit of a tangential thought: it might be interesting to generate a list of stacks tags that are not formalized, while all the tags they depend on are formalized

[Kevin Buzzard]

Yes, the "boundary" of what is done. One could imagine Patrick's flowchart tool thing being helpful here.

[Scott Morrison]

Kevin Buzzard said:

Scott Morrison I think you might have already tried something like this. Is there even some branch, which perhaps was already mentioned?

All the actual tagging done in the branch#stacks using @[stacks 01AB] has since been incorporated into mathlib using full URLs in doc-strings.

What that branch does still have it a script that scrapes all those doc-strings and produces a yaml file, ready for consumption by the stacks build process.

[Bryan Gin-ge Chen]

scripts/stacks_tags.lean and meta/stacks.lean get data from the stacks attribute, not the doc strings, right?

[Kim Morrison]

We're about to revive this ancient thread, to continue discussion about Stacks project tagging, given there is a sudden influx of interest in doing this.

[Kim Morrison]

Proposal:

Someone implements an attribute that looks like:

@[stacks 044Q "Our definition of a quotient stack differs from the Stacks definition, because it is much more fun."]

i.e. that requires a tag as the first argument, and takes an optional string to contains any notes about the alignment.

[Kim Morrison]

(Note that the discussion above also talks about a @[stacks] tag, but then does not currently exist in Mathlib4.)

[Jiang Jiedong]

Hi, @Kim Morrison I strongly support this multiple (mathlib) to one (stacks project) attribute. I have two minor related questions:

1. Is there a possibility that a mathlib theorem corresponds to multiple stacks project theorem together? (e.g. by using TFAE) If so, shall we decompose the theorem in mathlib? or make multiple tags?
2. Do you think we should have a way to record that some tags in stacks are NOT in mathlib and are in the TODO list?

[Kim Morrison]

1. I think it should be possible to write @[stacks ABC, stacks XYZ], to achieve many-to-many tagging. I think it's probably best not to decompose a big theorem to match Stacks. However I think that will generally be very rare.

[Kim Morrison]

Let's aim initially to just be adding tags, but I think if this gets some traction will also find ourselves writing corollaries of mathlib lemmas to more exactly match something in stacks, and generally that should be fine?

[Kim Morrison]

Regarding TODO lists, it would be amazing if the "prerequisites" of a stacks tag were reliable enough that we could auto generate a list of all stacks tags which are not in Mathlib, but whose prerequisites are. I suspect that Stacks very often uses some much earlier fact without explicitly linking to the tag, however.

[Kim Morrison]

It would be great to experiment however. (And the stacks project is probably willing to help here are bit, if we can tell them about missing prerequisites!)

[Jannis Limperg]

Here's a stub for the attribute:

import Lean

open Lean

syntax (name := stacksAttr) "stacks " ident (str)? : attr

initialize registerBuiltinAttribute {
  name := `stacksAttr
  descr := "Register a Stacks tag for a theorem or definition"
  add := λ _decl _stx _attrKind => return ()
}

Then in a different (!) file:

import StacksAttr -- or whatever filename you chose above

@[stacks foo "hello"]
axiom foo : True

The Stacks tag grammar may not be a subset of Lean's ident grammar. In that case, one could use str instead of ident in the attribute syntax, then write the tags as "044Q" with quotes. Alternatively, one could implement a dedicated Stacks tag parser.

This definition of the attribute doesn't do anything, but code can be added to collect all the Stacks tags in a hash map, for example.

[Damiano Testa]

Oh, I started #16179 that also allows tags to start with a digit.

[Damiano Testa]

It is lacking a little "strictness" in not allowing spaces and probably no lowercase either, though.

[Jannis Limperg]

Ah, cool. I see you've already spent much more brainpower on this than my "waiting for Lean to compile" attempt. :)

[Damiano Testa]

The attribute at #16179 now checks that the "tag" is a 4-character string consisting of digits and uppercase letters only. The tag is mandatory, the comment is optional.

[Damiano Testa]

As usual, I am surprised by how many mistakes there were in the initial implementation of something so simple, but hopefully this works as intended now! :smile:

[Damiano Testa]

A good follow up would be to actually check that the tag exists in the Stacks project, e.g. making sure that

https://stacks.math.columbia.edu/tag/<myTag>

is an existing webpage. I would rather not include that in this PR, though.

[Matthew Ballard]

I think you need to parse this file: https://github.com/stacks/stacks-project/blob/master/tags/tags But, later yes

[Johan Commelin]

a PR that adds a 100 stacks tags (and nothing else) would benefit quite a bit from an explicit export (as json, or csv) of pairs (lean name, stacks tag in the attribute).
Because then we can query the stacks project for all the statements of those tags, and quickly skim whether the corresponding lean name makes sense.

I think we shouldn't over-engineer this yet. But also, it would be good to have a little bit of tooling to help streamline the reviews.

[Eric Wieser]

While we're over-engineering: how about a widget that shows an iframe for the stacks lemma when your cursor is on the id?

[Adam Topaz]

And even more over-engineering: it could show the pretty printed type of the lean declaration as well (this is for the list Johan suggested)

[Damiano Testa]

Recycling quite a bit from the assert_not_exists extension and command, I implemented a more sophisticated tagging system at #16191.

[Damiano Testa]

You can take a look at the test file of #16191 for what it adds. Briefly, #stacks_tags retrieves all declarations that have the stacks attribute.

For each found declaration, it prints a line

'declaration_name' corresponds to tag 'declaration_tag'.

The variant #stacks_tags! also adds the theorem statement after each summary line.

[Matthew Ballard]

Did you push?

[Damiano Testa]

I did not, but I should have done so now! :smile:

[Kevin Buzzard]

@Pieter Belmans looks like we're finally getting serious!

[Johan Commelin]

Shall we merge #16191? I think we can iterate on the design as we start using it.

[Yongle Hu]

I am trying to tag theorems with the corresponding Tags from the Stacks Project using @[stacks], but when I write @[stacks 0BR2], it gives an error saying "binary number." However, when I write @[stacks 08R2] or @[stacks 02R2], it does not report any errors. Could you please advise me on how to solve this problem? Thanks a lot!

[Mario Carneiro]

@Damiano Testa this is an issue using num+ident as the parser - 0BR2 is treated as a (malformed) binary number with 0B prefix instead of 0 and then the ident BR2

[Mario Carneiro]

I think it needs a custom parser

[Damiano Testa]

Oh, does 0B mean something, then?

[Damiano Testa]

Mario Carneiro said:

I think it needs a custom parser

Ok, that should be straightforward anyway: it should accept any sequence of digits and uppercase letters.

[Damiano Testa]

I'm not sure that I'll have time to do it today: I'm about to catch a plane and will have a busy day until later this evening.

[Mario Carneiro]

0b11010 is syntax for binary numbers, like 0x012abc

[Damiano Testa]

Oh, I see.

[Damiano Testa]

If it is of any temporary use, #16211 allows to write @[stacks «0BR8»] in the situations where the current parsing would fail.

[Yongle Hu]

Thank you very much!

Moreover, I think @[stacks 044Q "Our definition of a quotient stack differs from the Stacks definition, because it is much more fun"] should generate a line at the end of the annotation in the form [Stacks: Definition 044Q, Our definition of a quotient stack differs from the Stacks definition, because it is much more fun](https://stacks.math.columbia.edu/tag/044Q). This would make it easier for us to view the Stacks tags in the documentation webpage.

[Damiano Testa]

Oh, you mean adding the link to the webpage? That is a good idea and it will not require a hack, but I'm now on the plane! I'll do it later today.

[Damiano Testa]

To be completely clear: this is what you want the #stacks_tags to report, right?

[Jiang Jiedong]

Thank you for this @[stacks ...]!

[Yongle Hu]

Damiano Testa said:

To be completely clear: this is what you want the #stacks_tags to report, right?

I think it will be more helpful if, say, a link to 044Q and a documentation "our defintion ...." is rendered on the mathlib4 documentation pages, i.e. here

[Jiang Jiedong]

I have a PR-splitting question. Since we are currently working on adding tags, we are also trying to add a natural language description (mostly by copy from the stacks project) to the theorem's comment if there is not one already. Shall we split it into 2 PRs? one for tag only and one for these copied descriptions. Or a single PR is OK? Splitting or not, this PR will be purely modifying comments, no declarations will be harmed. :octopus:

[Pieter Belmans]

I'm the Stacks project infrastructure maintainer, checking in on what's going on after Kevin pinged me. I'll read up more on things later, but one thing I want to point out is that there is an API that gives you the HTML of just a statement, which might be something you could use here? I see word iframe being dropped, and I think a much better solution can be obtained via this API :).

[Ruben Van de Velde]

Is copy/pasting allowed, strictly speaking, under the GFDL?

[Eric Wieser]

The reason I suggested an iframe is that in the short term it saves us having to load KaTeX within the widget, for which we have a bunch of prototypes but nothing in mathlib.

[Eric Wieser]

Ruben's comment sounds like reason enough to do tags and docstrings separately

[Damiano Testa]

An update:

• #16225 makes #stacks_tags print the url of the corresponding tags (although the links are not clickable);
• #16211 is a hacky way of "solving" the binary issue (via  @[stacks «0BR8»]);
• #16230 is a more principled way of solving the binary issue (via @[stacks 0BR8]), but may require more careful review, since I never wrote a parser before.

[Kim Morrison]

I merged #16225. Eric has left a suggestion on #16230. Let's just close #16211 as I think #16230 can converge quickly enough.

[Mario Carneiro]

I think the parser should also accept a string literal, which avoids the thorny parser issues

[Eric Wieser]

Are there thorny issues here? This seems like a very simple parser

[Eric Wieser]

One thing I'm puzzled by is why the parser is using logWarning rather than throwError or even producing a parse error.

[Damiano Testa]

I don't like the parse error, since the message is confusing: stacks 0i44 suggests to close a square bracket rather than capitalising the i.

[Damiano Testa]

I'm happy to do logWarning or throwError, though for final code that is irrelevant.

[Damiano Testa]

Mario Carneiro said:

I think the parser should also accept a string literal, which avoids the thorny parser issues

Doees this apply to the old (num)? (ident)? trick? Or to the current custom parser?

[Mario Carneiro]

both...

[Matthew Ballard]

Sorry to bother but Mario can you expand?

[Damiano Testa]

With Eric's and Matt's suggestions, the parser now accepts only a 4-character long sequence of digits and uppercase letters, throwing meaningful errors otherwise.

[Damiano Testa]

For this reason, allowing it to alternatively parse also a string may not be necessary, unless Mario has some other reason for wanting to allow that.

[Matthew Ballard]

While we wait for any other feedback, please feel free to try out the changes at #16230 and report back any issues @Yongle Hu @Jiang Jiedong @Yuyang Zhao and others

[Damiano Testa]

Also, @Wojciech Nawrocki implemented clickable links to modules for #find_home here. Maybe something similar could be done for making the hardcoded URLs here also live and clickable!

(Sorry for pinging you directly Wojciech, feel free to ignore! :smile: )

[Jiang Jiedong]

What would happen when the comment "xxx" in @[stacks 09HH "xxx"] is longer than 100 characters?

[Damiano Testa]

You should be able to use

"a very long \
string"

[Damiano Testa]

After the \ (that you should probably type by pressing twice \), there has to be a line break and the subsequent spaces are ignored.

[Damiano Testa]

So,

"a very long \
string"

and

"a very long string"

and

"a very long \
                              string"

should render the same.

[Kim Morrison]

Perhaps the 100 character linter warning should include this advice?

[Damiano Testa]

That's a good idea! Should I add this as a blanket comment to all overflowing lines, or just to lines that contain a "? Or maybe only if there is a " past the 100 character limit! :smile:

[Damiano Testa]

The beauty of a syntax linter is that you can have very granular bike-shedding.

[Damiano Testa]

#16652

[Damiano Testa]

I could not find a place to reference for usage example of string gaps, though.

[Johan Commelin]

We now have > 10 stacks tags in mathlib :tada: It took us ~ 4 years after the idea was first mentioned :rofl:

[Junyan Xu]

There are in fact many more lemmas labeled [Stacks: ...]. Should we made a PR to switch them all to @[stacks ...]?

[Johan Commelin]

Yes please!

[Johan Commelin]

And I think there are also many other refs to stacks, that link to the full website

[Damiano Testa]

Here is a gist that Johan orchestrated and suggested that I should post here.

[Jiang Jiedong]

There is a PR #16105 with ～100 new stacks tag in the field theory before the infinite Galois theory. It will be ready for review in 1-2 hours.

[Yaël Dillies]

Andrew and I have proved a few things from Stacks and I will open a PR with stacks-annotated lemmas soon

[Patrick Massot]

If people are suddenly enthusiastic about linking Mathlib to the real world, can I remind that we have a nice Mathlib overview page that is full of holes and that editing it is simply done by editing https://github.com/leanprover-community/mathlib4/blob/master/docs/overview.yaml?

[Yaël Dillies]

Grepping on that page for '' yields no (true) positive. What do you mean by a "hole"? How can I determine what holes there are?

[Johan Commelin]

Maybe Patrick meant https://github.com/leanprover-community/mathlib4/blob/master/docs/undergrad.yaml

[Patrick Massot]

I mean whole areas of maths that are covered in Mathlib but not mentioned at all on this page.

[Patrick Massot]

@Yaël Dillies Let’s think of something you like. Say someone wants to know what kind of combinatorics is in Mathlib, and get some entry points to explore this area. Do you think this page will help them?

[Yaël Dillies]

Hmm, not if they do additive combinatorics, no :grinning:

[Yaël Dillies]

Is one big result per file too detailed, or is that okay?

[Bhavik Mehta]

We should probably have some of the set family stuff, and regularity lemma there too

[Jiang Jiedong]

From the PR review of #16105, I realized that many results in the Stacks Project are claimed in untagged paragraphs.

[Jiang Jiedong]

Is it meaningful that we also find some way of linking these results (in the untagged paragraphs) to mathlib theorems?

[Jiang Jiedong]

There are also some cases where two similar statements in the Stacks Project correspond to the same mathlib theorem. The current solution is write in the comments @[stacks ABCD "See also XYZW."]

[Andrew Yang]

I think mathlib isn't striving to be a formalization of stacks project and it should be fine if there are many-to-one or one-to-none correspondences.

[Matthew Ballard]

Many to many is allowed by the syntax last I checked

[Notification Bot]

7 messages were moved from this topic to #general > mathlib overview by Johan Commelin.

[Yaël Dillies]

Two easy Stacks attributes: #18920

[Johan Commelin]

Nov 11: ~ 10 @[stacks]
Nov 13: ~120 @[stacks]

[Damiano Testa]

Should #stacks_tags report also how many it found?

[Damiano Testa]

Maybe it should also have an optional string input to filter them.

[Johan Commelin]

Mwah, I think it's fine for now we can start worrying about that when we have 2000 of them

[Kim Morrison]

There are still lots of direct links to stacks in doc strings, if anyone would like to convert some to tags.

[Damiano Testa]

I do not know how to get clickable links to webpages, but #18955 adds hover and go-to-definition for the stacks/kerodon reports.

[Jz Pan]

Is it possible to get the info of stacks tags using doc-gen4? Maybe I'll working on it.

[Johan Commelin]

@Jz Pan What do you mean exactly? What kind of info would you like?

[Eric Wieser]

I think the answer here is "no, because doc-gen is not allowed to know about mathlib extensions"

[Eric Wieser]

But maybe doc-gen could have an extension point for custom renderers for attributes

[Damiano Testa]

Also, would you like to see the attribute on the declaration, or would seeing the output of #stacks_tags with import Mathlib be closer to what you want?

[Damiano Testa]

E.g. a link to a page with a list of all the declarations that have a stacks tag, for instance?

[Jz Pan]

What I want is if a theorem has stack tags, then Stacks: ... (link) ... will be automatically inserted to the docstring when generating doc pages. Otherwise you can't see anything about stacks on online doc pages.

[Jz Pan]

E.g. a link to a page with a list of all the declarations that have a stacks tag, for instance?

I haven't think of this yet; maybe it is unnecessary.

[Jz Pan]

If stacks mathlib extension can inject docstring automatically, then we don't need to change the code of doc-gen4.

[Jz Pan]

If stacks mathlib extension can inject docstring automatically

Maybe it's possible? Just like alias which will inject docstring automatically.

[Damiano Testa]

This is a good idea: if the stacks tag added text to the doc-string, it could include a link to the stacks project and hovers are clickable!

[Damiano Testa]

Very primitive, but here is goes!

#19131

[Jz Pan]

Could you run a test on, for example, https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/SeparableDegree.html ? Current code looks good, except for the comments, etc. in a wrong position.

[Jz Pan]

(Maybe I can try by myself later.)

[Junyan Xu]

https://stacks.math.columbia.edu/ has apparently be down for more than one day.

[Kevin Buzzard]

It was down for me earlier but it looks like it's working again now

[Yaël Dillies]

I've just opened #21046 to turn all links to Stacks in docstrings into stacks tags

[Damiano Testa]

I can't go through the PR carefully right now, but this is great, thank you very much!

[Damiano Testa]

I wonder if we should also make sure that there are no links to the stacks projects that could be stacks tag (with some thought about how to make it work in practice), to avoid similar PRs in the future.

[Yaël Dillies]

I think it would be hard. I can imagine one would want to link to Stacks for information rather than authoritatively saying "This is the entry corresponding to that declaration"

[Johan Commelin]

I think that once there are many @[stacks] in the library, future contributors will stumble upon them and use the same pattern. So I don't think we need to take any action to prevent this.

[Damiano Testa]

#21048 contains the first 2 Kerodon tags, as far as I can tell!

[Yaël Dillies]

Here's a second, more manual, PR: #21135

[Damiano Testa]

Yaël's PR exposed that there are already Stacks tags referring to sections, rather than specific lemmas (see this example).

Should we add a #stacks <tag> ("optional string") command that adds the <tag> as a section to the Stacks environment extension?

[Johan Commelin]

How common is this? My gut feeling is we should wait slightly longer

[Damiano Testa]

Probably not very common, I agree.

[Yaël Dillies]

I would say there are roughly 50 module docs referring to Stacks, not all to a section of Stacks

[Damiano Testa]

For references to lemmas in module-docs, I would say that they do not need special treatment: if the lemma is later proved, it is the lemma that should get the attribute.

[Damiano Testa]

Thinking about this again, I probably think that aligning section via the same mechanism is probably not a good approach.

[Damiano Testa]

It may be useful to do it, but it would probably be in a broader context of formalising all of the Stacks project, rather than establishing a direct connection between statements there and in mathlib.

[Yaël Dillies]

What! Formalising all of Stacks is not our end goal? :scream: (/j)

[Damiano Testa]

Of course it is, but for the moment it is a secret.