toast.yml

image: ubuntu:26.04
default: verify
user: user
command_prefix: |
  # Make not silently ignore errors.
  set -euo pipefail

  # Load the opam environment, if it exists.
  if [ -d "$HOME/.opam" ]; then
    eval "$(opam env)"
  fi

  # Load the elan environment, if it exists.
  if [ -f "$HOME/.elan/env" ]; then
    source "$HOME/.elan/env"
  fi

  # Make Bash log commands.
  set -x
tasks:
  install_packages:
    description: Install system packages.
    user: root
    command: |
      # Install the following packages:
      #
      # - build-essential - Used by opam to build Rocq
      # - curl            - Used for installing Lean and Tagref
      # - git             - Used for installing Lean dependencies
      # - libgmp3-dev     - Used by opam to build Rocq
      # - opam            - Used to install OCaml and Rocq
      # - pkg-config      - Used by opam to build Rocq
      # - ruby            - Used by the linter scripts
      apt-get update
      apt-get install --yes \
        build-essential \
        curl \
        libgmp3-dev \
        opam \
        pkg-config \
        ruby

  install_tagref:
    description: Install Tagref, a reference checking tool.
    dependencies:
      - install_packages
    user: root
    command: |
      # Install Tagref using the official installer script.
      curl \
        https://raw.githubusercontent.com/stepchowfun/tagref/main/install.sh \
        -LSfs | sh

  create_user:
    description: Create a user who doesn't have root privileges.
    user: root
    command: |
      # Create a user named `user` with a home directory and with Bash as the
      # login shell.
      useradd user --create-home --shell /bin/bash

      # Without this, Ruby will assume files are encoded as ASCII.
      echo 'export LANG="C.UTF-8"' >> /home/user/.profile

  install_lean:
    description: Install Lean.
    dependencies:
      - create_user
      - install_packages
    input_paths:
      - lake-manifest.json
      - lakefile.toml
      - lean-toolchain
    user: user
    command: |
      # Install Lean via the Lean version manager.
      curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
      source "$HOME/.elan/env"
      lake update
      lake exe cache get

  install_rocq:
    description: Install Rocq.
    dependencies:
      - create_user
      - install_packages
    user: user
    command: |
      # Install Rocq via opam.
      opam init --disable-sandboxing --yes
      eval "$(opam env)"
      opam pin add rocq-prover 9.0.0 --yes

  install_tools:
    description: Install the tools needed to verify the Rocq proofs.
    dependencies:
      - install_lean
      - install_rocq
      - install_tagref

  verify:
    description: Run Lean and Rocq on the proof scripts.
    dependencies:
      - install_tools
    input_paths:
      - Makefile
      - _RocqProject
      - proofs_lean
      - proofs_rocq
    user: user
    command: |
      # Run Lean on the proof scripts.
      lake build

      # Run Rocq on the proof scripts.
      make clean
      make

  lint:
    description: Run the linters.
    dependencies:
      - verify
    input_paths:
      - linters
      - toast.yml # To lint the tag references
    user: user
    command: |
      # Make sure the `LANG` environment variable is set for Ruby.
      source "$HOME/.profile"

      # Check references with Tagref.
      tagref
      tagref list-unused --fail-if-any

      # Run the linters.
      ./linters/lint-general.rb $(
        find . -type d \( \
          -path ./.git -o \
          -path ./.lake \
        \) -prune -o \( \
          -name '*.lean' -o \
          -name '*.rb' -o \
          -name '*.sh' -o \
          -name '*.v' -o \
          -name '*.yml' -o \
          -name 'Dockerfile' -o \
          -name 'Makefile' \
        \) -print
      )
      ./linters/lint-imports.rb \
        '^\s*import ' \
        '^\s*import ' \
        "lake env lean ?" \
        $(
          find . -type d \( \
            -path ./.git -o \
            -path ./.lake \
          \) -prune -o \( \
            -name '*.lean' \
          \) -print
        )
      # [ref:flags]
      ./linters/lint-imports.rb \
        '^\s*Require ' \
        '^\s*Require (Import )?(Stdlib|main)\.' \
        "rocq compile \
          -set 'Default Goal Selector=!' \
          -set 'Loose Hint Behavior=Strict' \
          -set 'Primitive Projections' \
          -set 'Printing Projections' \
          -unset 'Printing Primitive Projection Parameters' \
          -Q proofs_rocq main ?" \
        $(
          find . -type d \( \
            -path ./.git -o \
            -path ./.lake \
          \) -prune -o \( \
            -name '*.v' \
          \) -print
        )
      # [ref:flags]
      ./linters/lint-imports.rb \
        '^\s*Import ' \
        '^\s*Import ' \
        "rocq compile \
          -set 'Default Goal Selector=!' \
          -set 'Loose Hint Behavior=Strict' \
          -set 'Primitive Projections' \
          -set 'Printing Projections' \
          -unset 'Printing Primitive Projection Parameters' \
          -Q proofs_rocq main ?" \
        $(
          find . -type d \( \
            -path ./.git -o \
            -path ./.lake \
          \) -prune -o \( \
            -name '*.v' \
          \) -print
        )
      # [dir:proofs_rocq]
      if grep --recursive --line-number --include '*.v' Admitted proofs_rocq
      then
        echo "Error: 'Admitted' found in proofs." 1>&2
        exit 1
      fi
      # [dir:proofs_lean]
      if grep --recursive --line-number --include '*.lean' sorry proofs_lean
      then
        echo "Error: 'sorry' found in proofs." 1>&2
        exit 1
      fi