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

Easier Development #14

Closed
OliverKillane opened this issue Jul 30, 2023 · 0 comments · Fixed by #15
Closed

Easier Development #14

OliverKillane opened this issue Jul 30, 2023 · 0 comments · Fixed by #15
Assignees
Labels
Needs Improvement Confusing or poorly detailed content or diagrams Suggestion A suggestion to improve the notes

Comments

@OliverKillane
Copy link
Owner

OliverKillane commented Jul 30, 2023

Goals

  • Make it easier to develop notes
  • Need to make an image / devcontainer setup to make it possible to work on these notes:
  • Linting check as part of the CI, or a lint as a precommit hook

Maybe Goals?

  • Separating built pdfs from repo, and building in the CI [Problem: How to review pdfs from pull requests?]
  • Better helper scripts [Move to python, nicer messages, simple commands for build, maybe? - icn build, icn check etc]

Required Changes

  • Docker image built in repo and published to ghcr
  • added as .devcontainer with vscode settings & extensions setup

Needs to include:

  • Latex distribution + packages + latexindent
  • Language support for C++, elixir, haskell, rust, TLA, python
  • Pygments (+ add TLA highlighting for distributed notes)
  • Inkscape

Required Test

  • To be able to edit code, latex & diagrams from github codespaces by just opening the repo in codespaces / no setup required.
@OliverKillane OliverKillane added the Needs Improvement Confusing or poorly detailed content or diagrams label Jul 30, 2023
@OliverKillane OliverKillane self-assigned this Jul 30, 2023
@OliverKillane OliverKillane changed the title Docker Image Easier Development Sep 10, 2023
@OliverKillane OliverKillane added the Suggestion A suggestion to improve the notes label Sep 10, 2023
@OliverKillane OliverKillane linked a pull request Sep 27, 2023 that will close this issue
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Needs Improvement Confusing or poorly detailed content or diagrams Suggestion A suggestion to improve the notes
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant