Run sage doc server for jupyterlab

[kwankyu]

Reopen #35139 because of the renewed interest: https://groups.google.com/g/sage-devel/c/kzSWB8ps7VA

New environment variables added to sage.env:

SAGE_DOC_SERVER_URL = var("SAGE_DOC_SERVER_URL")
SAGE_DOC_LOCAL_PORT = var("SAGE_DOC_LOCAL_PORT", "0")

When Jupyter notebook launches,

• If SAGE_DOC_SERVER_URL is set, the url is used;
• else if local sage documentation is installed, a doc http server with port SAGE_DOC_LOCAL_PORT starts. If the port is 0 (the default), then a random port is selected by the system and stored to the environment variable;
• else the online official documentation website https://doc.sagemath.org is used

for the help menu of the Jupyter notebook.

Fixes #34794.

:memo: Checklist

• [x] The title is concise and informative.
• [x] The description explains in detail what this PR is about.
• [ ] I have linked a relevant issue or discussion.
• [ ] I have created tests covering the changes.
• [ ] I have updated the documentation and checked the documentation preview.

:hourglass: Dependencies

[github-actions[bot]]

Documentation preview for this PR (built with commit 1617269f35b9ffd90fb92433f7d5275560fb5f0c; changes) is ready! :tada: This preview will update shortly after each push to this PR.

[kwankyu]

Why do you use 8000 for the default port? That is the http port > 1024 which is most likely to be used by another local http server. If you use 0 as the default port then the system will assign a random unused port > 1024. That way you won't have to worry about port conflicts.

But then how can I know the port randomly assigned?

[kwankyu]

More precisely, how kernel.py finds the port number?

[kwankyu]

server.server_address[-1] gives the port. Then I need to figure out how to pass this number to kernel.py...

[kwankyu]

Why do you use 8000 for the default port? That is the http port > 1024 which is most likely to be used by another local http server. If you use 0 as the default port then the system will assign a random unused port > 1024. That way you won't have to worry about port conflicts.

I also would recommend using 127.0.0.1 in the url, rather than localhost. The reason is that a (rogue) DNS nameserver could, in principle, assign an arbitrary IP address to the name localhost. But the IP address 127.0.0.1 always refers to the loopback interface and would never trigger a DNS lookup.

Done. Thanks for the tips!

[kwankyu]

ping @culler @nbruin @mkoeppe

[mkoeppe]

Looks like a reasonable approach. After #36730, one might discuss if the doc server should be the responsibility of the sagemath_doc_html distribution, but for now this looks good.

[kwankyu]

Thanks!!

[kwankyu]

Bump up priority since the original poster of the issue regards it as a bug.