Skip to content

Latest commit

 

History

History
40 lines (24 loc) · 1012 Bytes

README.md

File metadata and controls

40 lines (24 loc) · 1012 Bytes

Mathlib Documentation

Reading the Manual

The latest release of this Mathlib manual can be read here.

Code origin / Installation

This is mostly adapted code from the Lean Language Reference. You should check there for installation instructions.

Any problems beyond the content itself are probably carried over from there, and might need fixing there.

Building the Reference Manual Locally

To build the manual, run the following command:

lake exe generate-manual --depth 2

Then run a local web server on its output:

python3 -m http.server 8880 --directory _out/html-multi

Then open http://localhost:8880 in your browser.

Development

In theory, one should be able to update this by calling a simple

lake update

However, this requires Verso to be compatible with the Lean version Mathlib uses.

Contributing

We happily accept content!