doc: initialize a user-facing mdbook #4
Workflow file for this run
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
| name: Build Aeneas user docs and test them | |
| on: [push, pull_request] | |
| jobs: | |
| test: | |
| name: Test Aeneas user docs | |
| runs-on: [self-hosted, linux, nix] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Build the book | |
| run: nix build '.?dir=docs/user'#book | |
| # TODO: test the Lean examples code via nix build '.?dir=docs/user'#test or something similar. |