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

Build Latex Documents in CI #331

Closed
Tracked by #56
Shoeboxam opened this issue Sep 23, 2021 · 0 comments · Fixed by #518 or #530
Closed
Tracked by #56

Build Latex Documents in CI #331

Shoeboxam opened this issue Sep 23, 2021 · 0 comments · Fixed by #518 or #530

Comments

@Shoeboxam
Copy link
Member

Shoeboxam commented Sep 23, 2021

We need a system for building latex documents as part of the build process for the documentation.
This would allow us to deploy the proofs alongside the library documentation.

Depends on #56, but development on this issue is not blocked.

A few comments:

  • it should run as a separate script from make html or make versions, to make local doc builds easier
  • for CI we could use a build server or cloud service to build the latex
  • this could be useful: https://github.com/aslushnikov/latex-online#api
@andrewvyrros andrewvyrros added this to Needs Discussion in OpenDP Development via automation Sep 28, 2021
@andrewvyrros andrewvyrros moved this from Needs Discussion to Up Next in OpenDP Development Oct 12, 2021
@andrewvyrros andrewvyrros moved this from Up Next to Ready for Development in OpenDP Development Feb 14, 2022
OpenDP Development automation moved this from Ready for Development to Done Aug 23, 2022
@Shoeboxam Shoeboxam reopened this Aug 23, 2022
OpenDP Development automation moved this from Done to In Progress Aug 23, 2022
OpenDP Development automation moved this from In Progress to Done Aug 23, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Archived in project
Development

Successfully merging a pull request may close this issue.

2 participants