name: lean
on: [push, pull_request]
jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: README inventory of Lean files
        run: sh scripts/check_inventory.sh
      - name: Install elan
        run: |
          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o elan-init.sh
          sh elan-init.sh -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
      - name: Build
        run: lake build
      - name: Forbidden constructs
        run: |
          if grep -rnE '\bsorry\b|\badmit\b|native_decide|^\s*axiom ' formal word-ir forth bcpl wolfram backend --include='*.lean'; then exit 1; fi
      - name: Axiom audit
        run: lake env lean formal/Audit.lean
      - name: Native x86-64 execution check
        run: .lake/build/bin/wordc check 300
      - name: Forth source files (x86-64)
        run: for f in examples/forth/*.fs; do .lake/build/bin/wordc forth "$f" || exit 1; done
      - name: Install wasmtime
        run: |
          curl -sSfL -o wasmtime.tar.xz https://github.com/bytecodealliance/wasmtime/releases/download/v30.0.2/wasmtime-v30.0.2-x86_64-linux.tar.xz
          tar xf wasmtime.tar.xz
          echo "$PWD/wasmtime-v30.0.2-x86_64-linux" >> "$GITHUB_PATH"
      - name: WebAssembly execution check
        run: .lake/build/bin/wasmw check 300
      - name: Forth source files (WebAssembly)
        run: for f in examples/forth/*.fs; do .lake/build/bin/wasmw forth "$f" || exit 1; done
      - name: Install AArch64/RISC-V toolchain and emulators (user mode, the bare RV32 board and the Cortex-M boards)
        run: sudo apt-get update && sudo apt-get install -y clang lld llvm qemu-user qemu-system-misc qemu-system-arm
      - name: AArch64 execution check (qemu)
        run: .lake/build/bin/a64c check 300
      - name: Forth source files (AArch64)
        run: for f in examples/forth/*.fs; do .lake/build/bin/a64c forth "$f" || exit 1; done
      - name: RISC-V execution check (qemu)
        run: .lake/build/bin/rv64c check 300
      - name: Forth source files (RISC-V)
        run: for f in examples/forth/*.fs; do .lake/build/bin/rv64c forth "$f" || exit 1; done
      - name: RV32 microcontroller profile check (bare-metal qemu virt board)
        run: .lake/build/bin/rv32c check 300
      - name: Forth source files (RV32, 32-bit words)
        run: for f in examples/forth/*.fs; do .lake/build/bin/rv32c forth "$f" || exit 1; done
      - name: Cortex-M profile check (bare-metal Cortex-M3 booting from flash, qemu lm3s6965evb)
        run: .lake/build/bin/cmc check 300
      - name: Forth source files (Cortex-M, 32-bit words)
        run: for f in examples/forth/*.fs; do .lake/build/bin/cmc forth "$f" || exit 1; done
      - name: Cortex-M0 profile check (bare-metal Cortex-M0, qemu microbit)
        run: .lake/build/bin/cm0c check 300
      - name: Forth source files (Cortex-M0, 32-bit words)
        run: for f in examples/forth/*.fs; do .lake/build/bin/cm0c forth "$f" || exit 1; done
      - name: Without the depth certificates (--no-opt keeps every guard)
        run: |
          for t in cm0c cmc rv32c; do
            for f in examples/forth/*.fs; do .lake/build/bin/$t forth "$f" --no-opt || exit 1; done
          done
      - name: Guard elimination shrinks the microcontroller code
        run: |
          mkdir -p /tmp/size && cd /tmp/size
          for spec in cm0c:thumbv6m-none-eabi:-mcpu=cortex-m0 cmc:thumbv7m-none-eabi:-mcpu=cortex-m3 rv32c:riscv32-unknown-elf:-march=rv32im; do
            t=${spec%%:*}; rest=${spec#*:}; tgt=${rest%%:*}; fl=${rest#*:}
            for f in $GITHUB_WORKSPACE/examples/forth/*.fs; do
              n=$(basename "$f" .fs)
              $GITHUB_WORKSPACE/.lake/build/bin/$t emit-forth "$f" > "$t-$n-opt.s"
              $GITHUB_WORKSPACE/.lake/build/bin/$t emit-forth "$f" --no-opt > "$t-$n-all.s"
              for v in opt all; do clang --target=$tgt $fl -c -o "$t-$n-$v.o" "$t-$n-$v.s" || exit 1; done
              a=$(llvm-size "$t-$n-all.o" | awk 'NR==2{print $1}'); b=$(llvm-size "$t-$n-opt.o" | awk 'NR==2{print $1}')
              echo "$t $n: $a -> $b bytes of code"
              [ "$b" -le "$a" ] || exit 1
            done
          done
      - name: Board images (image, run on the emulated boards, verify the serial log)
        run: |
          mkdir -p /tmp/board && cd /tmp/board
          # Microchip SAM D21 Curiosity Nano: not emulated; build every example's image (it must
          # assemble, link into 128 KiB of flash and convert to Intel HEX)
          for f in $GITHUB_WORKSPACE/examples/forth/*.fs; do $GITHUB_WORKSPACE/.lake/build/bin/cm0c image "$f" --board samd21-cnano || exit 1; done
          for t in cm0c cmc; do $GITHUB_WORKSPACE/.lake/build/bin/$t image $GITHUB_WORKSPACE/examples/forth/fib.fs || exit 1; done
          (timeout 10 qemu-system-arm -M microbit -kernel fib-microbit-v1.elf -display none -serial stdio -monitor none || true) > v1.log
          (timeout 10 qemu-system-arm -M lm3s6965evb -kernel fib.elf -display none -serial stdio -monitor none || true) > lm3s.log
          $GITHUB_WORKSPACE/.lake/build/bin/cm0c verify $GITHUB_WORKSPACE/examples/forth/fib.fs v1.log
          $GITHUB_WORKSPACE/.lake/build/bin/cmc verify $GITHUB_WORKSPACE/examples/forth/fib.fs lm3s.log