Idris 2 Community Tutorial

This project is an mdbook based off of Stefan Höck's idris2-tutorial. At present, it's largely just a direct port, but will evolve as the community maintains it.

This book is rendered automatically from the main branch with GitHub pages, which can be viewed at https://idris-community.github.io/idris2-tutorial/. The summary page can also be used as a table of contents for direct viewing in GitHub, though the rendered version is much preferable.

Contributing

Please see CONTRIBUTING.md for style and formatting guidance before submitting a PR.

Dependencies and Building

Building this mdbook is slightly complicated, as highlight.js has no support for idris, we are using katla to perform the highlighting, and injecting that highlighting into the Markdown before mdbook has a chance to see it using the build-book Raku script.

Idris Dependencies

This project requires pack and katla to build.

After either installing pack from your distro's package manager or following the quick installation directions in pack's readme, you can install katla with:

pack install-app katla

Raku Dependencies

This project requires Raku and the File::Temp, Shell::Command, and paths modules to build.

I recommend installing raku and zef through your distro's package manger. If your package manger has lacks either zef or raku, installation through rakubrew is an option, and if your package manager has raku but lacks zef, zef can be quite easily installed from source.

Once you have zef up and running, the dependencies for this project can be installed with:

zef install File::Temp Shell::Command paths

mdbook

Many distros have mdbook in their package manager, this is the recommended way to install it. If your distro lacks mdbook, or if the version it packages proves to be too old to build this project, after setting up a Rust toolchain with rustup, you can install mdbook from source with:

cargo install mdbook

Building

Once you have all the dependencies in place, simply run:

Important

The build-book script assumes that the Idris code in the project has already been built, and will not function properly if the Idris build directory is not populated, as the build files are required by katla to provide syntax highlighting.

Run pack build after a clean checkout or making any changes to Idris files to ensure that the build directory is up to date before running the build-book script.

./scripts/build-book

from this project's root directory, and the rendered book will be available in the book directory. I recommend using a simple static file server such as python -m http.serverto view the rendered book in your browser, simply opening the files directly in your browser is unlikely to work.

Formatting

This project uses mdformat to ensure consistency in Markdown formatting. While this is not strictly necessary to have locally, it is linted against in CI.

The mdformat configuration used in CI can be replicated by running the following commmand from the base directory of the project:

mdformat --wrap=no --number **/*.md