Making Sphinx notes

Stream: new members

[Gihan Marasingha]

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]

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]

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]

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]

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

[Johan Commelin]

Then it wouldn't load

[Johan Commelin]

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

[Johan Commelin]

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

[Gihan Marasingha]

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]

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]

Thanks for letting me know.

[Gihan Marasingha]

(deleted)