Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Most of the hyperlinks on this page are broken: https://leanprover-community.github.io/theories/category_theory.html

Steps to Reproduce

1. Just try them.

Expected behavior: [What you expect to happen]

Not 404.

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Reliably

Versions

Version 3 community, online.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

docs/naming.md has entire sections of nearly duplicate text. Just search for “Sometimes” and you'll find it.

I removed the following chunk from templates/contribute/doc.md. A replacement should eventually be restored...

## Tactic doc entries

Interactive tactics, user commands, hole commands and user attributes should have doc strings
explaining how they can be used. The `add_tactic_doc` command should be invoked afterwards to add a
doc entry to the appropriate page in the online docs.

Example:
```lean
/--
describe what the command does here
-/
add_tactic_doc
{ name := "display name of the tactic",
  category := cat,
  decl_names := [`dcl_1, `dcl_2],
  tags := ["tag_1", "tag_2"]
}

The argument to add_tactic_doc is a structure of type tactic_doc_entry.

• name refers to the display name of the tactic; it is used as the header of the doc entry.
• cat refers to the category of doc entry.
  Options: doc_category.tactic, doc_category.cmd, doc_category.hole_cmd, doc_category.attr
• decl_names is a list of the declarations associated with this doc. For instance,
  the entry for linarith would set decl_names := [`tactic.interactive.linarith].
  Some entries may cover multiple declarations.
  It is only necessary to list the interactive versions of tactics.
• tags is an optional list of strings used to categorize entries.
• The doc string is the body of the entry. It can be formatted with markdown.
  What you are reading now is taken from the description of add_tactic_doc.

If only one related declaration is listed in decl_names and if this
invocation of add_tactic_doc does not have a doc string, the doc string of
that declaration will become the body of the tactic doc entry. If there are
multiple declarations, you can select the one to be used by passing a name to
the inherit_description_from field.

If you prefer a tactic to have a doc string that is different then the doc entry, then between
the /-- -/ markers, write the desired doc string first, then --- surrounded by new lines,
and then the doc entry.

Note that providing a badly formed tactic_doc_entry to the command can result in strange error
messages.

In the install/macos page, I found it odd that a simple brew install lean isn't mentioned, since the formula is indeed available. Is there a reason this hasn't been mentioned there?

No time at the moment to do it myself, but just wanted to leave a public message that the 100 theorems links can be simplified. No need to store the directory, the random .html#, etc. Just the declaration name (e.g. complex.exists_root) will be enough. The generation can create links like

https://leanprover-community.github.io/mathlib_docs/find/complex.exists_root
https://leanprover-community.github.io/mathlib_docs/find/complex.exists_root/src

(Of course this only works for things in mathlib, but so does the current scheme, and this is more robust to refactorings.)

@alexpeattie added a nice feature on the docs pages that makes them look pretty on Twitter: leanprover-community/doc-gen#71

We should port that to the main site in some way.

https://leanprover-community.github.io/contribute/naming.html

It renders fine on github: https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/contribute/naming.md

This looks like different markdown parsing rules for mistletoe and github.

Consequently the link to "hygienic macro expansion" on https://leanprover-community.github.io/papers.html is broken, it contains an extra slash that shouldn't be there.

Somewhere in the tex->html conversion in make_site we should handle that _ must be written as \_ in a tex url, around line 300 https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/make_site.py#L300

We should put @fpvandoorn's "100 theorems" list on the website.

Right now, the <title>s of all the pages just say Lean community, which isn't brilliant when a user may have multiple pages open at the same time, or if they want to search for something, as they'll have to look at the URL to find what they want.

Also it might help when people are looking for things using a search engine? Although right now Google is the only search engine that even finds any of the install pages, and it's smart enough to pull in the <h1>.

It might make more sense to use the markdown titles for the HTML <title> tags.

All this means you need a Lean project manager. Your download at the very beginning does include such a tool, at bin/leanpkg. That one is written in Lean (you can see all the code in lib/lean/leanpkg/), so you already have all the required dependencies. However Lean, at least in its current series Lean 3.X.X, is not convenient at all to build a powerful project manager. So the Lean user community has build a more powerful project manager written in python: leanproject.

https://leanprover-community.github.io/toolchain.html#handling-dependencies

Hey, I run the Zulip project, and I was wondering if you folks would be interested in helping migrate your data import tool to something that lives in https://github.com/zulip/python-zulip-api that we document as generally available to other projects that want a public archive?

If so, I'd love to have some of our core contributors collaborate with the author to integrate it there (and then you can just use our project as a pip dependency here).

We have plans for a more built-in experience in Zulip, but I was realizing even if we provide that, this sort of "generate HTML" thing is both more customizable and maybe a cleaner approach for a final public archive of a Zulip organization being closed down, so we probably want something of this form available as a tool to use with Zulip anyway.

The title of the page at https://leanprover-community.github.io/install/windows.html is "Get Python", but presumably it should be "Installing Lean and mathlib on Windows".

These terms and acronyms could be difficult for newcomers depending on their background:

• HoTT: Homotopy Type Theory
• UH: Unification Hints
• TC: Type Classes
• fbip: Functional But In Place
• dot notation: field notation: generalized structure projection
• API: Application Programming Interface

The text For a faster paced and broader dive, you can get the [tutorials project](https://github.com/leanprover-community/tutorials). shows up in https://leanprover-community.github.io/learn.html but not https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/learn.md and links to the non-existent page https://github.com/leanprover-community/tutorials). Links which are not immediately followed by . do not suffer this problem.

in https://leanprover-community.github.io/install/project.html, there is a line

• If you have not logged in since you installed Lean and mathlib, then you may need to first type source ~/.profile or source ~/.bash_profile depending on your OS.

Someone just asked about this in the Xena Discord, about an error on Windows, which was bash: /c/Users/<their username>/.profile: No such file or directory. I told them to just close Git Bash and reopen it, which should do the same thing. Weirdly, if I do ls -a in Git Bash on my computer, I do see ~/.profile.

It might be worth mentioning explicitly what to do/expect on each OS, since right now it's expecting users to already be familiar with the command line. I would make a PR but it's been years since I last used Mac/Linux, and Windows behaviour seems to vary?

Cf. leanprover/lean4#267

We're telling staticjinja that every .md file is a jinja2 template, so if one of them contains {{ (e.g. when talking about "weakly implicit" arguments in Lean, (usually written ⦃ in unicode)), jinja2 will be unable to parse the file and then complain:

jinja2.exceptions.TemplateSyntaxError: unexpected char 'XX' at YY

This came up when testing templates/latex.md in #165.

@EdAyers wrote some nice explanations of various aspects of Lean 3 in his "edlib" repo, including e.g. an explanation of unicode in Lean and a series of articles on meta code.

On Zulip he gave his permission for us to do what we like with them.

Could someone point me to the code that is responsible for generating https://leanprover-community.github.io/archive/ ?

https://leanprover-community.github.io/100.html and https://leanprover-community.github.io/overview.html should have toggles to show/hide items that are todo/done.

On this page the following are broken (some appear multiple times in the page):

• algebra.module
• algebra.pi_instances
• smul_eq_mul
• linear_algebra.matrix
• linear_algebra.nonsingular_inverse
• antiautomorphism
• bilin_form.to_quadratic_form f
• linear_algebra.quadratic_form

may I open a PR?

see: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20tactics.20list.3F/near/433066915

Pages like https://leanprover-community.github.io/theories/category_theory.html should have their source hosted in mathlib, so that it is easy to check for deadlinks during CI.

At https://leanprover-community.github.io/100.html we format and linkify each declaration using info from doc-gen. But it seems the format of this info has changed since mathlib3 and now has relative links, so these links are broken: e.g. irrational_sqrt_2 links to https://leanprover-community.github.io/Mathlib/Data/Real/Irrational.html#irrational_sqrt_two

We could add a <base> tag to this page (and check that none of the other links are relative), or find some other solution.

In the overview, measure_theory.measure_theory.measure_space no longer exists. https://github.com/leanprover-community/leanprover-community.github.io/runs/960815811

In the section "Hilbert spaces" of the undergrad.yaml file, there are two entries called "its completeness". It makes sense in context:

...
dual space: 'normed_space.dual.normed_space'
Riesz representation theorem: 'inner_product_space.to_dual'
inner product space $l^2$: 'lp.inner_product_space'
its completeness: 'lp.complete_space'
inner product space $L^2$: 'measure_theory.L2.inner_product_space'
its completeness: 'measure_theory.Lp.complete_space'
...

On the current display of the website, the first "its completeness" links to entry for the second "its completeness", and the second "its completeness" does not appear at all.

https://leanprover-community.github.io/theories/linear_algebra.html doesn't mention semilinear maps.

Pygments 2.7.0 was released so we should figure out how to syntax-highlight pages like https://leanprover-community.github.io/extras/calc.html

The section on variable conventions in our style doc should be expanded to include e.g. fields, rings, categories, etc.

There is a broken link in this section, it gives a 404 error: https://leanprover-community.github.io/ci.html.

See Zulip thread. (Though perhaps there's still more to discuss.)

A first start provided by @Vierkantor :
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/big.20ops/near/195941698

when deciding how to pretty-print an expression,
Lean looks up the notations associated to the head of the expression (e.g. `finset.sum`).
It tries them one by one, until it finds a notation that matches the expression,
then uses that to pretty-print.
The order in which they are tried is the order in which they are stored in the environment structure,
which in this case is the order in which they are defined.
Apparently the priority information is thrown away
(typically it would be highest-priority first, then by order of definition).
This is why the order matters.

A notation definition is associated to the head of the expression it expands to, so
```lean
notation ∑ binders ,  r:(scoped f, finset.sum finset.univ f) := r
```
is associated to the head of the expansion of `r`,
which is the head of `finset.sum finset.univ f`, which is `finset.sum`.
But `finset.univ.sum` doesn't get expanded to `finset.sum finset.univ` at that point,
so you have to write `finset.sum finset.univ` instead of `finset.univ.sum`.