Building the website without Agda #187
Assignees
Labels
web
For issues/pull requests relating to the 1lab website itself.
Comments
plt-amy
added
the
web
plt-amy
added a commit
that referenced
this issue
Feb 24, 2023
Closes #187. Currently [Agda code being embedded in code blocks](https://user-images.githubusercontent.com/4346137/217057817-b10648a1-9419-4f2a-969c-9a2ad9efc323.png) - I don't know if we want to add a special class to these, so they don't have a border? This is implemented by avoiding any build steps which would cause an Agda compile (specifically `_build/all-pages.json`). The alternative would be to rely on staler versions of those files, and simply not rebuild them. I think what I'm doing here is the correct thing to do. It keeps us honest with our task dependencies, and means `--skip-agda` works from a clean build directory. It does mean some site features (namely `agda://` links) won't work. Co-authored-by: Amélia <me@amelia.how>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Knee-deep in the #186 refactor, getting all of the Agda to check would be a nightmare. But I still want to make sure my diagrams, TeX, etc look right!
Would it be possible to have a "mode" (like
-w) which builds only the Literate Agda pages, directly from the Markdown source?The text was updated successfully, but these errors were encountered: