Add a mdbook #concept macro

[VojtechStep]

Usage: The {{#concept "concept name" Agda=concept-definition WDID=wikidata-id WD="Foobar"}} is a foobar over quxs.; the Agda, WDID and WD fields are optional.

---

OLD INFORMATION, see #884 (comment) for latest implementation.

Currently it generates an invisible anchor so that we can get a link to that part of the webpage by appending #wikidata-id to the URL, and makes the text bold. The text isn't a link to anything and we don't want it to be, because it can itself contain a link (e.g. cocones over spans, where spans is a link), and nested links aren't valid HTML.
The anchor is only generated when a wikidata ID is provided.

Scrapers can get all concepts defined on the webpage by querying for the a.wikidata selector.

Additionally the preprocessor also generates a concept_index.json file, which contains information about all concepts in the library. It's an array of objects which look like this:

{
  "name": "concept name without links",
  "text": "raw markdown from the file",
  "wikidata": "wikidata id",
  "link": "link to the concept, relative to the agda-unimath homepage"
}

The wikidata and link fields are optional, since we want to be able to use this macro also for concepts without a WD id, for consistency.

[VojtechStep]

Example of the generated concept index:

[
  {
    "name": "acyclic undirected graph",
    "text": "acyclic undirected graph",
    "wikidata": "Q3115453",
    "link": "graph-theory.acyclic-undirected-graphs.html#Q3115453"
  },
  {
    "name": "circuit",
    "text": "circuit",
    "wikidata": "Q245595",
    "link": "graph-theory.circuits-undirected-graphs.html#Q245595"
  },
  {
    "name": "cocone under a span",
    "text": "cocone under a [span](foundation.spans.md)"
  }
]

[EgbertRijke]

Can you make it so that “NA” is an accepted wikidata identifier? This way we can record somewhere that we checked for it and didn’t find any suitable identifier. Perhaps in some cases we also want to provide secondary identifiers.

[VojtechStep]

Sure

[andrejbauer]

Why write NA? Just leave out the WD field, it's optional.

[EgbertRijke]

Is this PR ready to be merged, or did you want to work on it some more?

[VojtechStep]

Oh right - I'd like to also generate the link in External links and tweak the visuals a little. I'm marking this PR as a draft and whatever gets done by tonight is what I'd stick with for the moment.

[EgbertRijke]

Alright! Take your time. I won’t be able to put much work in today, because I’m getting ready for my trip to Pittsburgh. I’m flying at 6am tomorrow.

[VojtechStep]

I'd like to bikeshed the way we should present the information - I included everything I can do in the attached screenshot: the source page starts with

A {{#concept "circuit" Agda=circuit-Undirected-Graph WD="Cycle" WDID=Q245595}} in an ...

The metadata represent:

• first string in quotation marks is the name of the concept
• Agda=<agda name> is the name of a relevant Agda definition
• WD="label" is the display name of the concept on WikiData
• WDID=Q... is the WikiData ID

It produces the following entry in concept_index.json:

  {
    "name": "circuit",
    "text": "circuit",
    "wikidata": "Q245595",
    "link": "graph-theory.circuits-undirected-graphs.html#Q245595",
    "definition": "graph-theory.circuits-undirected-graphs.html#1010"
  },

and automatically generates

• the ¶ link, which links to its location; this one is generated when either WDID or Agda metadata are provided
• The [AG] link, which links to the definition in Agda code; caveat: the definition must be found on the same page. A warning is printed during website building if the corresponding definitions isn't found
• The [WD] link, which links to Katja's current implementation of mathswitch (base URL is configurable in book.toml)
• Links to mathswitch and wikidata under the ## External links section, which is created if it doesn't exist; these are only created if the WD field is provided

I personally think that we shouldn't show everything; I'd keep only the ¶ self-link and the link to mathswitch in External links. My reasoning is that otherwise the prose starts getting very busy and I can't think of a way to make it less intrusive in this PoC.

[VojtechStep]

Why write NA? Just leave out the WD field, it's optional.

To record the discussion from the Discord - the NA would indicate that the author checked WikiData for an appropriate identifier and didn't find any. I think that's a desirable feature, because we don't want to always burden contributors with checking wikidata, in which case the WD meta would be empty, and every once in a while we could get a dump of unidentified concepts and try to find appropriate IDs.

The current implementation accepts WD=NA and operationally treats it as if it wasn't included at all.

[VojtechStep]

This is the current "cleaner" version

[VojtechStep]

With the latest revision, all concepts get an identifier, and it's assigned in a way to maximize stability across changes; however it's still expected that the id of an entry will change from time to time.

The current index looks like this:

[
  {
    "name": "acyclic undirected graph",
    "text": "acyclic undirected graph",
    "wikidata": "Q3115453",
    "link": "graph-theory.acyclic-undirected-graphs.html#Q3115453",
    "id": "graph-theory.acyclic-undirected-graphs.html#Q3115453"
  },
  {
    "name": "circuit",
    "text": "circuit",
    "wikidata": "Q245595",
    "definition": "graph-theory.circuits-undirected-graphs.html#1010",
    "link": "graph-theory.circuits-undirected-graphs.html#concept-circuit-Undirected-Graph",
    "id": "graph-theory.circuits-undirected-graphs.html#concept-circuit-Undirected-Graph"
  },
  {
    "name": "cocone under a span",
    "text": "cocone under a [span](foundation.spans.md)",
    "link": "synthetic-homotopy-theory.cocones-under-spans.html#concept-cocone-under-a-span",
    "id": "synthetic-homotopy-theory.cocones-under-spans.html#concept-cocone-under-a-span"
  }
]

The fields id, link, name and text are always present. id should be treated as an opaque identifier. link can be appended to the root URL https://unimath.github.io/agda-unimath/ to get the URL of the concept definition in prose. Similarly, definition (when present) can be used to get a link to the concept definition in code.

[andrejbauer]

I suspect the definition fields would be more useful if it specified an interval in the file where the definition is (rathr than just the starting line). This way one could extract the relevant snippet of the code.

[VojtechStep]

This might be a misunderstanding - the definition field isn't a line number, it's a link to that definition on the website. When Agda processes the .lagda.md files, it assigns a number to every definition site and creates an HTML anchor, so e.g. visiting https://unimath.github.io/agda-unimath/graph-theory.circuits-undirected-graphs.html#945 will take you to the definition circuit-Undirected-Graph. Are you suggesting that I should add information about the source .lagda.md file that exists somewhere on GitHub? I think that would be a lot more work than I'm currently comfortable signing up for, since right now the preprocessor is working with the markdown/HTML mix that Agda generates by replacing agda code blocks with raw HTML, and it doesn't interact at all with the original sources.

[VojtechStep]

@andrejbauer is there anything else I can do at the moment? I think we can merge this implementation and come back if it turns out that we need to change something. I won't be adding docs since it's still an experiment.

[VojtechStep]

This is a pretty low-impact PR, so if there aren't any immediate objections from @EgbertRijke or @fredrik-bakke I'll merge it so that Katja has something to work with.

[fredrik-bakke]

Should I begin using this macro in my contributions? If so, how?

[fredrik-bakke]

I had a quick look, and I don't have any objections.

[VojtechStep]

Should I begin using this macro in my contributions? If so, how?

That wasn't my intention for now, the two examples included in this PR are apparently enough. I'd say the macro is still experimental and subject to change, since it's not completely clear what information we want to provide. That's also why I didn't add anything to the contributors guide.