toast.yml

image: ubuntu:24.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

  # 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 Coq
      # - curl            - Used for installing Tagref
      # - libgmp3-dev     - Used by opam to build Coq
      # - opam            - Used to install OCaml and Coq
      # - pkg-config      - Used by opam to build Coq
      # - 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_coq:
    description: Install Coq.
    dependencies:
      - create_user
      - install_packages
    user: user
    command: |
      # Install Coq via opam.
      opam init --disable-sandboxing --yes
      eval "$(opam env)"
      opam switch create 5.2.0 --yes
      eval "$(opam env)"
      opam pin add coq 8.20.1 --yes

  install_tools:
    description: Install the tools needed to verify the Coq proofs.
    dependencies:
      - install_coq
      - install_tagref

  verify:
    description: Run Coq on the proof scripts.
    dependencies:
      - install_tools
    input_paths:
      - Makefile
      - _CoqProject
      - proofs
    user: user
    command: |
      # Run Coq on the proof scripts.
      make clean
      make

  lint:
    description: Run the linters.
    dependencies:
      - verify
    input_paths:
      - linters
    user: user
    command: |
      # Make sure the `LANG` environment variable is set for Ruby.
      source ~/.profile

      # Check references with Tagref.
      tagref

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