[ doc ] Adding tutorials

.editorconfig

@@ -48,3 +48,18 @@ max_line_length = off
 
 [*.py]
 indent_size = 4
+
+# See: https://stackoverflow.com/a/40348831/2572373
+[**{.build,docs/build,linters/build}**]
+charset = unset
+end_of_line = unset
+insert_final_newline = unset
+trim_trailing_whitespace = unset
+indent_style = unset
+indent_size = unset
+max_line_length = unset
+
+# Auto-generated file
+[.idrisCommit]
+insert_final_newline = unset
+

.github/workflows/ci-super-linter.yml

@@ -42,20 +42,13 @@ jobs:
           fetch-depth: 0
           persist-credentials: false # https://docs.zizmor.sh/audits/#artipacked
 
+      - name: Load super-linter configuration
+        # Use grep inverse matching to exclude eventual comments in the .env file
+        # because the GitHub Actions command to set environment variables doesn't
+        # support comments.
+        run: grep -v '^#' .github/linters/super-linter.env >> "$GITHUB_ENV"
+
       - name: Lint Code Base
         uses: super-linter/super-linter/slim@v8
         env:
-          DEFAULT_BRANCH: master
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-          IGNORE_GENERATED_FILES: true
-          SAVE_SUPER_LINTER_SUMMARY: true # Required for generating linting reports in PR
-
-          VALIDATE_PYTHON_BLACK: false # Avoid conflict: Ruff is preferred
-          VALIDATE_GIT_COMMITLINT: false
-
-          VALIDATE_MARKDOWN_PRETTIER: false # We use markdownlint
-          VALIDATE_YAML_PRETTIER: false # We use yamllint
-
-          # Disable Biome
-          VALIDATE_BIOME_FORMAT: false
-          VALIDATE_BIOME_LINT: false

.linters/super-linter-fix.ipkg

@@ -0,0 +1,3 @@
+package super-linter-fix
+
+prebuild = "FIX_MARKDOWN=true FIX_NATURAL_LANGUAGE=true FIX_SPELL_CODESPELL=true ./super-linter.sh"

.linters/super-linter-local.env

@@ -0,0 +1,2 @@
+# Disable stuff which may not work for local run
+VALIDATE_CHECKOV=false

.linters/super-linter-run.ipkg

@@ -0,0 +1,3 @@
+package super-linter-run
+
+prebuild = "./super-linter.sh"

.linters/super-linter.env

@@ -0,0 +1,17 @@
+DEFAULT_BRANCH=master
+IGNORE_GENERATED_FILES=true
+# Required for generating linting reports in PR
+SAVE_SUPER_LINTER_SUMMARY=true
+
+# Avoid conflict: Ruff is preferred
+VALIDATE_GIT_COMMITLINT=false
+VALIDATE_PYTHON_BLACK=false
+
+# We use markdownlint
+VALIDATE_MARKDOWN_PRETTIER=false
+# We use yamllint
+VALIDATE_YAML_PRETTIER=false
+
+# Disable Biome
+VALIDATE_BIOME_FORMAT=false
+VALIDATE_BIOME_LINT=false

.linters/super-linter.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+# See: https://github.com/super-linter/super-linter/blob/dd82ec5c927bff0fecc98865b0be8aa6ef849001/docs/run-linter-locally.md
+docker run --platform linux/amd64 \
+  --env-file "$(pwd)/../.github/linters/super-linter.env" \
+  --env-file "$(pwd)/../.github/linters/super-linter-local.env" \
+  -e LOG_LEVEL=NOTICE \
+  -e RUN_LOCAL=true \
+  -e FIX_MARKDOWN="${FIX_MARKDOWN:-false}" \
+  -e FIX_NATURAL_LANGUAGE="${FIX_NATURAL_LANGUAGE:-false}" \
+  -e FIX_SPELL_CODESPELL="${FIX_SPELL_CODESPELL:-false}" \
+  -v "$(pwd)/../":/tmp/lint \
+  ghcr.io/super-linter/super-linter:latest

docs/source/tutorials.rst

@@ -14,6 +14,14 @@ You can read more in the `original framework <https://diataxis.fr/tutorials/>`_
   :maxdepth: 1
   :caption: Choose what to learn
 
-  tutorials/test-function
-  tutorials/generators
-  tutorials/derivation
+  tutorials/t00-installation-and-setup
+  tutorials/t01-generator-monad
+  tutorials/t02-handling-emptiness
+  tutorials/t03-measuring-test-coverage
+  tutorials/t04-automatic-generator-derivation
+  tutorials/t05-derivegen-signatures
+  tutorials/t06-mixing-manual-and-automatic
+  tutorials/t07-beyond-fuel
+  tutorials/t08-generating-gadts-with-proofs
+  tutorials/t09-toy-example
+  tutorials/t10-derivation-tuning

docs/source/tutorials/t00-installation-and-setup.md

@@ -0,0 +1,186 @@
+# Installation and First Steps
+
+Welcome to DepTyCheck! This tutorial will guide you through installing Idris 2 and DepTyCheck, creating your first project, and running a simple
+generator.
+
+## Our Goal
+
+In this tutorial, you will:
+
+1. Install Idris 2 and the DepTyCheck library
+2. Create a project configured with DepTyCheck
+3. Write and run a generator that produces random `TrafficLight` values
+
+By the end, you will see output like:
+
+```text
+Red : TrafficLight
+```
+
+---
+
+## Step 1: Install Idris 2
+
+First, you need to install Idris 2. We recommend using [`pack`](https://github.com/stefan-hoeck/idris2-pack/), which manages both the compiler
+and library dependencies.
+
+Follow its [installation script](https://github.com/stefan-hoeck/idris2-pack/?tab=readme-ov-file#quick-installation).
+
+**Verify your installation:**
+
+```bash
+idris2 --version
+```
+
+Sample output:
+
+```text
+Idris 2, version 0.8.0-80fd5e4d7
+```
+
+```{note}
+You need Idris 2 version **0.8.0 or newer** for DepTyCheck to work.
+```
+
+---
+
+## Step 2: Create Your First Project
+
+### Create a project directory
+
+```bash
+mkdir deptycheck-tutorial
+cd deptycheck-tutorial
+```
+
+### Create a project file named `tutorial.ipkg`
+
+```text
+package tutorial
+
+version = 0.0.1
+langversion >= 0.8.0
+
+sourcedir = "."
+builddir = ".build"
+
+modules = Main
+main = Main
+executable = tutorial
+
+depends = deptycheck
+```
+
+```{note}
+The `depends = deptycheck` line tells Idris to use the DepTyCheck library.
+```
+
+---
+
+## Step 3: Write Your First Generator
+
+### Create a file `Main.idr` with the following code
+
+```idris
+import Deriving.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+
+data TrafficLight = Red | Yellow | Green
+
+Show TrafficLight where
+  show Red = "Red"
+  show Yellow = "Yellow"
+  show Green = "Green"
+
+genTrafficLight : Fuel -> Gen MaybeEmpty TrafficLight
+genTrafficLight = deriveGen
+
+main : IO ()
+main = do
+  Just light <- pick (genTrafficLight (limit 0))
+    | Nothing => putStrLn "Generation failed"
+  printLn light
+```
+
+```{note}
+- `%language ElabReflection` enables the metaprogramming features needed for `deriveGen`
+- `deriveGen` automatically creates a generator for `TrafficLight`
+- `pick` runs the generator and extracts one value
+```
+
+---
+
+## Step 4: Build and Run
+
+### Build the project
+
+```bash
+pack build
+```
+
+`pack` will download and build all dependencies automatically along with source code of the module.
+
+### Run the executable
+
+```bash
+pack run tutorial.ipkg
+```
+
+Expected output (your result will vary):
+
+```text
+Yellow
+```
+
+```{note}
+Run the command multiple times to see different results (Yellow, Green, Red).
+```
+
+---
+
+## Step 4: Try It in the REPL (Optional)
+
+You can also test your generator interactively.
+
+### Start the REPL
+
+Pass the Main module name to preload it:
+
+```bash
+rlwrap pack repl ./Main.idr
+```
+
+```{note}
+- `%language ElabReflection` enables the metaprogramming features needed for `deriveGen`
+- `deriveGen` automatically creates a generator for `TrafficLight`
+- `pick` runs the generator and extracts one value
+```
+
+### Run the generator
+
+```text
+:exec printLn =<< pick (genTrafficLight (limit 0))
+```
+
+Expected output:
+
+```text
+Just Green
+```
+
+### Run it multiple times to see different colors
+
+### Exit the REPL
+
+```text
+:quit
+```
+
+---
+
+## Next Steps
+
+Now that you have a working setup, you are ready to learn the fundamentals of generator creation:
+
+- **Continue to Tutorial 1:** [The Generator Monad](t01-generator-monad.md) to learn how to create generators manually using `pure`, `elements`,
+  `choose`, and other combinators.