Hax home page using mkdocs #1225
Merged
+657
−4,181
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
franziskuskiefer
requested changes
Jan 13, 2025
There was a problem hiding this comment.
Thanks!
Let's drop everything that's not properly populated yet.
- Manual > Examples look empty
- RFCs we could drop. But I'm fine keeping it as is.
- Engine and Frontend should maybe only link to the rust/odocs for now? Those graphs there don't make much sense 😉
- Keep the blog but drop my test entry there.
- It looks like you dropped the default mkdocs page from dev. But it also had some useful information on how to use mkdocs and dependencies that I think we should keep.
Oh and on this I'm not sure what that means. I don't see interaction options. I'm fine with dropping them for now and adding them back later. But we should make clear what's working and what not. |
|
👍 For the interactions, you don't see any "Play" buttons on the right corner of code blocks in e.g. "Tutorial > Panic freedom"? 
|
3 tasks
W95Psp
force-pushed
the
franziskus/docs-setup
branch
from
c5785c6 to
505cd4f
Compare
W95Psp
force-pushed
the
franziskus/docs-setup
branch
from
53d755f to
bf7624a
Compare
|
Running the deployment action to try it out: https://github.com/hacspec/hax/actions/runs/12765732261 |
franziskuskiefer
approved these changes
Jan 14, 2025
There was a problem hiding this comment.
lgtm with the few nits addressed.
I'm seeing warnings
WARNING - Doc file 'engine/index.md' contains a link './docs/hax-engine/index.html', but the
target 'engine/docs/hax-engine/index.html' is not found among documentation files.
WARNING - Doc file 'frontend/index.md' contains a link
'./docs/hax_frontend_exporter/index.html', but the target
'frontend/docs/hax_frontend_exporter/index.html' is not found among documentation
files.
Co-authored-by: Franziskus Kiefer <[email protected]>
Co-authored-by: Franziskus Kiefer <[email protected]>
|
The warnings are because those paths are generated via rustdoc and odoc: this happens only in the CI |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR drops the mdbook book in favor of a unique entry point website, generated using mkdocs.
This PR:
I fixed some broken links and broken contents, but I suspect there is more!
Also, there is a number of TODO left (let's see if we want those in this PR or not):