Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make coq stdlib html's documentation readable offline #15202

Open
SnarkBoojum opened this issue Nov 16, 2021 · 2 comments
Open

Make coq stdlib html's documentation readable offline #15202

SnarkBoojum opened this issue Nov 16, 2021 · 2 comments
Labels
good first issue Beginners welcome to submit a pull request. help wanted kind: design discussion Discussion about the design of a feature. kind: documentation Additions or improvement to documentation.

Comments

@SnarkBoojum
Copy link
Contributor

In the Debian build script, I build and make the stdlib documentation available using:

        dune build @stdlib-html --display=verbose
	# all the html files point to the same logo - ship it and point to it
	cp ide/coqide/coq.png _build/default/doc/stdlib/html/logo.png
	find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/files/barron_logo.png,logo.png,g"
	# all the html files point to some remote css - but they can be local too
	cp doc/common/styles/html/coqremote/modules/node/node.css _build/default/doc/stdlib/html/
	find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/node/node.css,node.css,g"
	cp doc/common/styles/html/coqremote/modules/system/defaults.css _build/default/doc/stdlib/html/
	find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/system/defaults.css,defaults.css,g"
	cp doc/common/styles/html/coqremote/modules/system/system.css _build/default/doc/stdlib/html/
	find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/system/system.css,system.css,g"
	cp doc/common/styles/html/coqremote/modules/user/user.css _build/default/doc/stdlib/html/
	find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/user/user.css,user.css,g"
	find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/sites/all/themes/coq/coqdoc.css,coqdoc.css,g"
	cp tools/coqdoc/style.css _build/default/doc/stdlib/html/
	find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/sites/all/themes/coq/style.css,style.css,g"

so I put needed files with the html files and make the links use it, so that the docs look right even offline. You'll notice that it isn't a serious patch, but a hack to work around the issue.

In addition, you'll notice that the links I'm fixing look like "//coq.inria.fr/foo/bar/baz", which means they're lacking "https:" -- there must be something fishy about it too.

@Alizter Alizter added kind: design discussion Discussion about the design of a feature. kind: documentation Additions or improvement to documentation. labels Nov 17, 2021
@Alizter Alizter added this to Infrastructure in User documentation May 17, 2022
@Alizter Alizter added this to Documentation in coqdoc May 23, 2022
@Alizter Alizter moved this from Infrastructure to Stdlib in User documentation May 25, 2022
@ejgallego
Copy link
Member

I can reproduce, that's an easy fix for someone willing to dig into the code.

@ejgallego ejgallego added help wanted good first issue Beginners welcome to submit a pull request. labels Jan 20, 2024
@SkySkimmer
Copy link
Contributor

SkySkimmer commented Feb 16, 2024

In addition, you'll notice that the links I'm fixing look like "//coq.inria.fr/foo/bar/baz", which means they're lacking "https:" -- there must be something fishy about it too.

That's the "network-path reference" syntax https://stackoverflow.com/questions/4071117/uri-starting-with-two-slashes-how-do-they-behave
It means use whatever protocol the main page used to load the resource.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
good first issue Beginners welcome to submit a pull request. help wanted kind: design discussion Discussion about the design of a feature. kind: documentation Additions or improvement to documentation.
Projects
Status: No status
coqdoc
  
Documentation
Development

No branches or pull requests

4 participants