Zulip Chat Archive

Stream: new members

Topic: Making Sphinx notes


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...).

view this post on Zulip Johan Commelin (Nov 12 2019 at 10:30):

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

view this post on Zulip Johan Commelin (Nov 12 2019 at 10:30):

Then it wouldn't load

view this post on Zulip Johan Commelin (Nov 12 2019 at 10:31):

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

view this post on Zulip Johan Commelin (Nov 12 2019 at 10:31):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gihan Marasingha (Nov 12 2019 at 14:43):

Thanks for letting me know.

view this post on Zulip Gihan Marasingha (Nov 12 2019 at 14:43):

(deleted)


Last updated: May 08 2021 at 04:14 UTC