verifiers.yml

name: verifiers
on: [push, pull_request, workflow_dispatch]

# Run many verifiers on metamath files.
# We *primarily* check set.mm and iset.mm, but we also run some checks on
# other files (in particular on some HTML files).
#
# Only one verifier is necessary, but using multiple verifiers counters
# the risk that a verifier might have a defect in its implementation.
# With 4 verifiers, all 4 would have to have a defect involving an
# invalid theorem for that invalid theorem to be accepted as valid.
# This is unlikely, because the verifiers are written by different people
# in different languages.  This can be considered extreme peer review, where
# every reviewer is separately checking each step.
# Some of these verifiers also check for style,
# so using multiple verifiers can also detect many different style problems.
#
# Note that one of the checks is scripts/verify.
#
# We report an error if the list of "discouraged" results is unexpected;
# this makes it easy to detect changes (which can then be specially reviewed).
# To regenerate the "discouraged" file, you can run scripts/gen-discouraged
#
# We typically rewrap the file using scripts/rewrap.

# TODO: We aren't caching many old results; add caches
# (e.g., of unchanged compiled programs) to speed things further.

# In each job we download, build, install, and run a verifier.
# NOTE: We generally install programs in $HOME/bin, so ensure that's on the
# PATH (usually it is on any non-Windows system).

jobs:
  ###########################################################
  skip_dups:
    name: Check for duplicate jobs to avoid duplication
    # continue-on-error: true # Uncomment once integration is finished
    runs-on: ubuntu-latest
    # Map a step output to a job output
    outputs:
      should_skip: ${{ steps.skip_check.outputs.should_skip }}
    steps:
      - id: skip_check
        uses: fkirc/skip-duplicate-actions@master
        with:
          github_token: ${{ github.token }}
          paths_ignore: '["**/README.md", "**/docs/**"]'

  ###########################################################
  checkmm:
    name: Verify using checkmm (a C++ verifier by Eric Schmidt)
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    steps:
      # By default checkout fetches a single commit, which is what we want.
      # See: https://github.com/actions/checkout
      - uses: actions/checkout@v3
      - run: echo 'Starting'
      - run: pwd
      - run: ls -l
      - run: g++ --version
      # Get and compile checkmm, a C++ verifier by Eric Schmidt
      - run: wget -N https://github.com/metamath/metamath-website-seed/raw/main/downloads/checkmm.cpp
      - run: g++ -O2 -o checkmm checkmm.cpp
      # Use it to verify set.mm and iset.mm
      - run: ./checkmm set.mm
      - run: ./checkmm iset.mm

  ###########################################################
  metamathexe:
    name: Verify using metamath.exe (original C verifier by Norman Megill)
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    steps:
      - uses: actions/checkout@v3
      # Update first to counter problems installing texlive
      - run: sudo apt-get update --fix-missing
      # Install LaTeX so we can test generated LaTeX. We use extended packages:
      # texlive-extra-utils provides pdflatex
      # texlive-fonts-extra provides phonetic.sty
      # texlive-science provides accents.sty
      - run: sudo apt-get install texlive-latex-extra texlive-extra-utils texlive-fonts-extra texlive-science
      # Here's an eXample of how to install "extra" LaTeX packages. See: 
      # https://tex.stackexchange.com/questions/38978/how-can-i-manually-install-a-latex-package-debian-ubuntu-linux/39259#39259
      # - run: mkdir -p "$HOME/texmf"
      # - run: wget https://mirrors.ctan.org/macros/latex/contrib/accents.zip -o "$HOME/texmf/accents.zip"
      # - run: cd "$HOME/texmf"; unzip -j accents.zip
      # - run: texhash texmf
      # Use GITHUB_PATH to set PATH. For details see:
      # https://docs.github.com/en/free-pro-team@latest/actions/reference/
      # workflow-commands-for-github-actions#setting-an-environment-variable
      - name: Ensure ~/bin is in PATH
        run: |
          echo "$HOME/bin" >> "$GITHUB_PATH"
          mkdir -p "$HOME/bin"
      - name: Get metamath C program and supporting files
        run: scripts/download-metamath
      - name: Record latest version of metamath as env variable
        run: |
          echo "METAMATH_LATEST_VERSION=$(cat metamath/.latest_version)" >> $GITHUB_ENV
      # Note: cache key includes version of metamath in use
      - name: Cache metamathexe
        id: cache-metamathexe
        uses: actions/cache@v3
        env:
          cache-name: cache-metamathexe
        with:
          path: ~/bin/metamath
          key: ${{ runner.os }}-build-${{ env.cache-name }}-${{ env.METAMATH_LATEST_VERSION }}
      - name: Build/install metamath, a C verifier (and more) by Norm Megill
        if: ${{ !steps.cache-metamathexe.outputs.cache-hit }}
        run: |
          gcc --version
          scripts/build-metamath
      # Create mmset.html and mmil.html so we can verify against them.
      - run: metamath 'read set.mm' 'markup mmset.raw.html mmset.html /ALT /CSS' quit
      - run: metamath 'read iset.mm' 'markup mmil.raw.html mmil.html /ALT /CSS' quit
      - run: scripts/verify --top_date_skip --extra 'write bibliography mmbiblio.html' set.mm
      - run: scripts/verify --top_date_skip iset.mm
      - run: ls -1 *.mm | sed -e '/^set\.mm$/d' -e '/^iset\.mm$/d' | while read db; do scripts/verify --top_date_skip --no-verify-markup "$db"; done
      - run: scripts/check-raw-html set.mm mmcomplex.raw.html mmdeduction.raw.html mmnatded.raw.html mmnf.raw.html mmset.raw.html mmzfcnd.raw.html mmfrege.raw.html
      - run: scripts/check-raw-html iset.mm mmil.raw.html
      # Generate HTML from raw files into mpegif-html/ and mpeuni-html/
      - run: scripts/regen-from-raw --force '/HTML' .regened.html
      - run: mkdir -p mpegif-html/
      - run: for f in *.regened.html; do mv $f mpegif-html/${f%.regened.html}.html ; done
      - run: scripts/regen-from-raw --force '/ALT_HTML' .regened.html
      - run: mkdir -p mpeuni-html/
      - run: for f in *.regened.html; do mv $f mpeuni-html/${f%.regened.html}.html ; done
      # Check that set.mm and iset.mm have been rewrapped.
      # We'd probably rather have a bot push up a commit with the rewrapping
      # when a pull request is submitted, but until we set that up,
      # at least check that the rewrapping has been done.
      - run: cp set.mm set-wrapped.mm
      - run: scripts/rewrap set-wrapped.mm
      - run: echo 'Checking for set.mm rewrapping:' && diff -U 0 set.mm set-wrapped.mm
      - run: cp iset.mm iset-wrapped.mm
      - run: scripts/rewrap iset-wrapped.mm
      - run: echo 'Checking for iset.mm rewrapping:' && diff -U 0 iset.mm iset-wrapped.mm
      # The following checks are arbitrarily included in the metamath job.
      - run: echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" set.mm
      - run: echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" iset.mm
      # Check generated LaTeX, to ensure the TeX definitions are okay. set.mm:
      - run: python3 scripts/latex_collector.py set.mm list-set.tex
      - run: pdflatex -halt-on-error list-set.tex 2>&1 | tee ,latex-output
      # Complain if the pdflatex output says something is invalid
      - run: "! grep ' invalid ' ,latex-output"

  ###########################################################
  smetamath-rs:
    name: Verify using smetamath-rs (smm3) (Rust verifier by Stefan O'Rear)
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    steps:
      - uses: actions/checkout@v3
      - name: Cache smm3
        id: cache-smm3
        uses: actions/cache@v3
        env:
          cache-name: cache-smetamath
        with:
          path: ~/.cargo/bin/smetamath
          key: ${{ runner.os }}-build-${{ env.cache-name }}
      - name: Install rust
        if: ${{ !steps.cache-smm3.outputs.cache-hit }}
        uses: hecrj/setup-rust-action@v1
        with:
          rust-version: stable
      - name: Install smm3
        if: ${{ !steps.cache-smm3.outputs.cache-hit }}
        run: cargo install smetamath --vers 3.0.0
      - name: Verify set.mm
        run: |
          ~/.cargo/bin/smetamath --verify --split --jobs 4 --timing ./set.mm 2>&1 | tee smm.log && [ `egrep '(:Error:|:Warning:)' < smm.log; echo $?` -eq 1 ]
      - name: Verify iset.mm
        run: |
          ~/.cargo/bin/smetamath --verify --split --jobs 4 --timing ./iset.mm 2>&1 | tee smm.log && [ `egrep '(:Error:|:Warning:)' < smm.log; echo $?` -eq 1 ]

  ###########################################################
  metamath-knife:
    name: Verify using metamath-knife
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    steps:
      - uses: actions/checkout@v3
      - name: Cache metamath-knife
        id: cache-metamath-knife
        uses: actions/cache@v3
        env:
          cache-name: cache-knife
        with:
          path: ~/.cargo/bin/cache-knife
          key: ${{ runner.os }}-build-${{ env.cache-name }}
      - name: Install rust
        if: ${{ !steps.cache-metamath-knife.outputs.cache-hit }}
        uses: hecrj/setup-rust-action@v1
        with:
          rust-version: stable
      - run: git clone --depth 1 https://github.com/david-a-wheeler/metamath-knife.git
      - run: cd metamath-knife && cargo build --release
      - name: Verify set.mm
        run: |
          metamath-knife/target/release/metamath-knife --verify ./set.mm
      - name: Verify iset.mm
        run: |
          metamath-knife/target/release/metamath-knife --verify ./iset.mm
      - name: Check axiom usage for set.mm
        run: |
          metamath-knife/target/release/metamath-knife --verify-usage ./set.mm
      - name: Check axiom usage for iset.mm
        run: |
          metamath-knife/target/release/metamath-knife --verify-usage ./iset.mm

  ###########################################################
  mmj2:
    name: Verify using mmj2 (Java verifier by Mel L. O'Cat and Mario Carneiro)
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    steps:
      - uses: actions/checkout@v3
      # See: https://github.com/actions/setup-java
      - uses: actions/setup-java@v3
        with:
          distribution: 'zulu' # ('temurin', 'zulu', ...) - required field
          java-version: '11' # The JDK version to make available on the path.
          # java-package: jdk # (jdk, jre, jdk+fx, or jre+fx) - defaults to jdk
          # architecture: x64 # (x86, x64, armv7, aarch64, or ppc64le) - default value derived from the runner machine
      - run: wget -N https://github.com/digama0/mmj2/raw/master/mmj2jar/mmj2.jar
      - run: mkdir macros
      - run: wget -O macros/definitionCheck.js https://github.com/digama0/mmj2/raw/master/mmj2jar/macros/definitionCheck.js
      - run: wget -O macros/init.js https://github.com/digama0/mmj2/raw/master/mmj2jar/macros/init.js
      - run: wget -O macros/showDiscouraged.js https://github.com/digama0/mmj2/raw/master/mmj2jar/macros/showDiscouraged.js
      # Do extra checking and generate the '*discouraged.new' file
      # (the 'printf' lets us insert multiple lines).
      # We use setparser to check that definitions don't create
      # syntax ambiguities
      - run: scripts/verify-mmj2 --setparser 'mmj.verify.LRParser' --extra "$(printf 'RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel\nRunMacro,showDiscouraged,discouraged.new')" set.mm
      - run: scripts/verify-mmj2 --setparser 'mmj.verify.LRParser' --extra "$(printf 'RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel\nRunMacro,showDiscouraged,iset-discouraged.new')" iset.mm
      - run: echo 'Checking discouraged file:' && diff -U 0 discouraged discouraged.new
      - run: echo 'Checking iset-discouraged file:' && diff -U 0 iset-discouraged iset-discouraged.new

  ###########################################################
  mmverifypy-setmm:
    name: Verify set.mm using mmverify.py (Python verifier by Raph Levien)
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    steps:
      - uses: actions/checkout@v3
      # See https://github.com/actions/setup-python
      - uses: actions/setup-python@v4
        with:
          python-version: '>=3.9'
      - run: wget -N https://raw.githubusercontent.com/david-a-wheeler/mmverify.py/master/mmverify.py
      # We can speed up the script by deleting all logging calls, since we do
      # not need them.
      - run: sed -E '/^ *vprint\(/d' mmverify.py > mmverify.faster.py
      - run: chmod a+x mmverify.faster.py
      - run: ./mmverify.faster.py set.mm

  ###########################################################
  mmverifypy-isetmm:
    name: Verify iset.mm using mmverify.py (Python verifier by Raph Levien)
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    steps:
      - uses: actions/checkout@v3
      # See https://github.com/actions/setup-python
      - uses: actions/setup-python@v4
        with:
          python-version: '>=3.9'
      - run: wget -N https://raw.githubusercontent.com/david-a-wheeler/mmverify.py/master/mmverify.py
      # We can speed up the script by deleting all logging calls, since we do
      # not need them.
      - run: sed -E '/^ *vprint\(/d' mmverify.py > mmverify.faster.py
      - run: chmod a+x mmverify.faster.py
      - run: ./mmverify.faster.py iset.mm

  ###########################################################
  check-dates:
    name: Check dates in set.mm
    runs-on: ubuntu-latest
    needs: skip_dups
    if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
    # Check for valid dates (detect nonsense like "June 31")
    # We run scripts/report-changes.py to convert dates to Unix timestamps;
    # this will raise an exception if the conversion can't occur,
    # thus checking that dates are valid. If the conversion is invalid,
    # you'll see the output from the last *valid* date followed by
    # an exception.
    # TODO: Check other .mm files, currently this only checks set.mm.
    steps:
      - uses: actions/checkout@v3
      - run: pip3 install ply
      - run: scripts/report-changes.py --gource > /dev/null

# TODO: Add mm-scala. Something like this:
#     ###########################################################
#     # - # mm-scala, a Scala verifier by Mario Caneiro
#     #   name: mm-scala (Scala)
#     #   language: scala
#     #   install:
#     #     - git clone --depth 1 https://github.com/digama0/mm-scala.git
#     #   script:
#     #     - cd mm-scala; sbt ++$TRAVIS_SCALA_VERSION test
#     #     - ls
#     #     - ls mm-scala
#     #     - mm-scala/mm-scala set.mm
#     ###########################################################