build.yml

# This file is based on mathlib's `build.yml.in` but we don't use mathlib's `mk_build_yml.sh` so
# you can edit this file directly.

on:
  push:
    branches-ignore:
      # ignore tmp branches used by bors
      - 'staging.tmp*'
      - 'trying.tmp*'
      - 'staging*.tmp'
      - 'nolints'
      # do not build lean-x.y.z branch used by leanpkg
      - 'lean-3.*'
      # ignore staging branch used by bors, this is handled by bors.yml
      - 'staging'

name: continuous integration

jobs:

  # When you push to a branch, we cancel previous runs of jobs in this file on that branch.
  cancel:
    name: 'Cancel previous runs on branch'
    # if: github.ref != 'refs/heads/master'
    runs-on: ubuntu-latest
    # timeout-minutes: 3
    steps:
      - uses: styfle/cancel-workflow-action@0.9.0
        with:
          all_but_latest: true
          access_token: ${{ github.token }}

  build:
    name: Build lean-liquid
    runs-on: liquid
    env:
      # number of commits to check for olean cache
      GIT_HISTORY_DEPTH: 20
    outputs:
      artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
    steps:
      # - name: bump swap space
      #   uses: pierotofy/set-swap-space@master
      #   with:
      #     swap-size-gb: 14

      - uses: actions/checkout@v2
        with:
          fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}

      - name: install elan
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
          echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV

      # - name: install Python
      #   if: ${{ ! 0 }}
      #   uses: actions/setup-python@v1
      #   with:
      #     python-version: 3.8

      - name: install mathlibtools
        run: python -m pip install --upgrade pip mathlibtools

      - name: leanpkg configure
        run: leanpkg configure

      - name: get mathlib cache
        run: leanproject get-mathlib-cache || true

      - name: try to find olean cache
        continue-on-error: true
        run: ./scripts/fetch_olean_cache.sh

      - name: leanpkg build
        id: build
        run: |
          set -o pipefail
          echo "::set-output name=started::true"
          # We record hashes of the oleans for debugging purposes.
          find src -name "*.olean" -exec md5sum {} \; | awk '{print $2,$1}' | sort > olean_hashes_at_start.txt
          echo "Starting build at $(date +'%T')"
          lean --json --make src | python scripts/detect_errors.py
          result_run1=$?
          echo "Run 1 complete at $(date +'%T'); return value $result_run1"
          find src -name "*.olean" -exec md5sum {} \; | awk '{print $2,$1}' | sort > olean_hashes_after_run_1.txt
          lean --json --make src | python scripts/detect_errors.py
          result_run2=$?
          echo "Run 2 complete at $(date +'%T'); return value $result_run2"
          find src -name "*.olean" -exec md5sum {} \; | awk '{print $2,$1}' | sort > olean_hashes_after_run_2.txt
          exit $result_run2

      - name: push release to azure
        if: always() && github.repository == 'leanprover-community/lean-liquid' && steps.build.outputs.started == 'true'
        continue-on-error: true
        run: |
          archive_name="$(git rev-parse HEAD).tar.xz"
          find src/ -name "*.olean" -o -name ".noisy_files" | tar cJf "$archive_name" -T -
          azcopy copy "$archive_name" "https://oleanstorage.blob.core.windows.net/mathlib/lean-liquid/$archive_name${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false

      - name: setup precompiled zip file
        if: always() && steps.build.outputs.started == 'true'
        id: setup_precompiled
        run: |
          touch workspace.tar
          tar -cf workspace.tar --exclude=*.tar* .
          git_hash="$(git log -1 --pretty=format:%h)"
          echo "::set-output name=artifact_name::precompiled-lean-liquid-$short_lean_version-$git_hash"

      - name: upload precompiled lean-liquid zip file
        if: always() && steps.build.outputs.started == 'true'
        uses: actions/upload-artifact@v2
        with:
          name: ${{ steps.setup_precompiled.outputs.artifact_name }}
          path: workspace.tar

  lint:
    name: Lint lean-liquid
    runs-on: liquid
    needs: build

    steps:
      - name: retrieve build
        uses: actions/download-artifact@v2
        with:
          name: ${{ needs.build.outputs.artifact_name }}

      - name: untar build
        run: tar -xf workspace.tar

      - name: install elan
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: lint
        # Uncomment the following line to make the build succeed even if there are linting errors
        # continue-on-error: true
        run: |
          ./scripts/mk_all.sh
          lean --run scripts/lint_project.lean

  test:
    name: Test liquid_tensor_experiment is sorry-free
    runs-on: ubuntu-latest
    needs: build

    steps:
      - name: retrieve build
        uses: actions/download-artifact@v2
        with:
          name: ${{ needs.build.outputs.artifact_name }}

      - name: untar build
        run: tar -xf workspace.tar

      - name: install elan
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: install Python
        if: ${{ ! 0 }}
        uses: actions/setup-python@v1
        with:
          python-version: 3.8

      - name: test liquid_tensor_experiment is sorry free
        run: python scripts/ensure_lte_sorry_free.py

  stats:
    name: Stats for lean-liquid
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v2

      - name: install ripgrep
        run: sudo apt install -y ripgrep

      - name: count lines in src
        run: |
          shopt -s globstar
          wc -l src/**/*.lean

      - name: count lines in for_mathlib
        run: |
          shopt -s globstar
          wc -l src/for_mathlib/**/*.lean

      - name: count sorries
        run: |
          rg --count-matches sorry src | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " total"}'

  update-branch:
    # This should be configured so that failure (which is likely whenever there is a force-push to
    # master) doesn't cause the rest of the build to fail, e.g., by putting it in its own job.
    name: Update lean-3.3x branch
    runs-on: ubuntu-latest
    needs: build
    steps:
    - uses: actions/checkout@v2
      with:
        fetch-depth: 0

    - name: update lean-3.3x branch
      if: github.ref == 'refs/heads/master'
      uses: leanprover-contrib/update-versions-action@master