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

Run fstardoc (with some modifications) over standard library #14

Open
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

mgritter
Copy link

@mgritter mgritter commented Nov 7, 2021

This PR refreshes the standard library documentation using fstardoc.

Instead of using pandoc (and writing a syntax highlighting grammar in the format it understands) my revised script uses the GitHub service to render markdown -> html, so we get the syntax highlighting that GitHub performs.

The script used to generate this is a work in progress at
https://github.com/mgritter/FStar/blob/mgritter/script_html_conversion/.scripts/fstardoc/generate-ulib.py

Additions:

  • Index page includes the first sentence in the module documentation, if it can be found.
  • Instead of showing the code for open or module X = Y or include, the document translates those dependencies into a bulleted list with hyperlinks.
  • Language annotation on code blocks is FStar not fstar

Diffs to fstardoc can be seen here: FStarLang/FStar@master...mgritter:mgritter/script_html_conversion

@ghost
Copy link

ghost commented Nov 7, 2021

CLA assistant check
All CLA requirements met.

@mgritter
Copy link
Author

mgritter commented Nov 7, 2021

I broke the CSS for syntax highlighting... will fix.

@mgritter mgritter marked this pull request as draft November 7, 2021 23:18
@mgritter mgritter marked this pull request as ready for review November 8, 2021 00:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant