## Stream: new members

### Topic: Making Sphinx notes

#### Gihan Marasingha (Nov 11 2019 at 11:35):

Is there an idiot's guide to making (and publishing) one's own Sphinx lecture notes? Is it easy to set up a server? Is there a community-hosted server?

#### Kevin Buzzard (Nov 11 2019 at 15:08):

Stuff like this

http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/ch1_and_or_props/prop_exercises.html

I wrote by just copying Theorem Proving In Lean. I want the links to go to a more modern version of online Lean, but this should be possible (Bryan Gin-Ge Chen showed me how to do it). Or do you want something else?

#### Jeremy Avigad (Nov 11 2019 at 17:04):

There are two routes to get there. Conceptually, creating TPIL went something like this:

- install Sphinx
- run sphinx-quickstart to create the directory structure
- customize a few things: tinker with the settings in config.py, add Gabriel Ebner's lean_sphinx.py to enable the Try it! button and testing, and change the Makefile accordingly. (I also modified the template slightly with the file _templates/navigation_without_header.html.) IIRC, I also had to modify the Latex template to get fonts and unicode working right.

So, one option is to do the same: do sphinx-quickstart, compare the resulting directory side-by-side with TPIL, and make the same or similar changes, as appropriate.

Alternatively, installing Sphinx, copying TPIL, and replacing the content with your own should have the same effect. That is easier. The only advantage to the first approach is that it will give you a better sense of how you can configure things on your own.

#### Gihan Marasingha (Nov 12 2019 at 10:21):

Thanks very much! On a side note, is anyone else having issues with the web editor? Currently, it doesn't seem to move past (running...).

#### Johan Commelin (Nov 12 2019 at 10:30):

I've had issues with running the web editor in "Private browsing mode" by mistake

#### Johan Commelin (Nov 12 2019 at 10:31):

Otherwise, it should take a while to get started, but after that be fairly responsive.

#### Johan Commelin (Nov 12 2019 at 10:31):

But @Bryan Gin-ge Chen is the expert. I can't help beyond simple cargo culting (-;

#### Gihan Marasingha (Nov 12 2019 at 10:40):

It could be my browser or browser settings. It seems to load after a couple of minutes with Chrome, but I'm still getting nothing with Safari.

#### Bryan Gin-ge Chen (Nov 12 2019 at 14:02):

Unfortunately, Safari currently has issues with many WebAssembly programs. On my macbook, both the community lean-web-editor and the "old" Lean web editor display the following error in the JS console: Unhandled Promise Rejection: RangeError: Maximum call stack size exceeded.. I also saw a similar issue on github for sql.js, an unrelated program.

It seems to be something recent (from the past few months). One thing I should do is see if I can add more informative error messages to the UI.

#### Gihan Marasingha (Nov 12 2019 at 14:43):

Thanks for letting me know.

#### Gihan Marasingha (Nov 12 2019 at 14:43):

(deleted)

Last updated: May 08 2021 at 04:14 UTC