Eric Wieser

It's not clear to me whether ignoring errors is deliberate here.

This is not a feature request, merely a comment to document what seems like undocumented API. I found I was able to set the "points" manually (instead of actually using...

This doesn't actually work yet, but contains enough to debug the renderer on the latex.md file Blocked by https://github.com/executablebooks/mdit-py-plugins/pull/46

The docs for `list` render as:  However, if we run that code: ```lean inductive {u} my_list (T : Type u) : Type u | nil : Π {T :...

Convert to an installable python package

3

This isn't a full conversion, but should still work after this restructure. The motivation here is to try and separate out "things specific to mathlib" from "things other lean projects...

Add a link to the import graph viewer

5

Example: https://eric-wieser.github.io/mathlib-import-graph/?highlight=core:data.dlist&docs_url=https://leanprover-community.github.io/mathlib_docs/

minisearch webworker is terminated on page reloads

1

I've found the startup time for the search to be very painful, especially since when I click a search result and find its the wrong one, I have to start...

Do not write json to stdout

6

Otherwise it can't be used with projects that emit diagnostics