coq-windows.yml

name: CI (Coq, Windows)

# Note that we must split up each command into a separate step for Windows, because otherwise we don't get error code
# See also https://github.com/avsm/setup-ocaml/issues/72

on:
  push:
    branches: [ master , sp2019latest , v8.6 , v8.8 , v8.10 ]
  pull_request:
  merge_group:
  workflow_dispatch:
  release:
    types: [published]
  schedule:
    - cron: '0 0 1 * *'

jobs:
  build:

    runs-on: windows-latest
    name: windows

    concurrency:
      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
      cancel-in-progress: true

    env:
      NJOBS: "2"
      COQ_VERSION: "8.18.0" # minimal major version required for bedrock2 components
      COQEXTRAFLAGS: "-async-proofs-j 1"
      COQCHKEXTRAFLAGS: ""
      OPAMYES: "true"
      OPAMCONFIRMLEVEL: "unsafe-yes"

    steps:
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    - name: Setup Python
      uses: actions/setup-python@v5
      with:
        python-version: 3.x
    - name: Set up OCaml
      uses: ocaml/setup-ocaml@v3
      with:
        ocaml-compiler: 4.13.1
    - run: opam install conf-time conf-gcc
    - run: opam install 'ocamlfind>=1.9.7'
    - run: opam pin add --kind=version coq ${{ env.COQ_VERSION }}
    - run: opam install js_of_ocaml
    - name: Work around https://github.com/actions/checkout/issues/766
      run: opam exec -- bash -l -c 'git config --global --add safe.directory "*"'
    - name: echo build params
      run: .\etc\ci\describe-system-config-win.ps1
    - name: deps
      run: opam exec -- bash etc/ci/github-actions-make.sh -j${{ env.NJOBS }} CC=gcc deps
    - name: standalone-ocaml
      run: opam exec -- bash etc/ci/github-actions-make.sh -j${{ env.NJOBS }} standalone-ocaml
    - name: install-standalone-unified-ocaml
      run: opam exec -- bash etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist

    - name: coq
      run: opam exec -- bash etc/ci/github-actions-make.sh -j1 coq
    - name: all-except-generated-and-js-of-ocaml
      run: opam exec -- bash etc/ci/github-actions-make.sh -j1 all-except-generated-and-js-of-ocaml
    - name: standalone-js-of-ocaml
      run: opam exec -- bash etc/ci/github-actions-make.sh -j1 standalone-js-of-ocaml
    - name: install-standalone-js-of-ocaml
      run: opam exec -- bash etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
    - name: c-files lite-generated-files
      run: opam exec -- bash etc/ci/github-actions-make.sh -j${{ env.NJOBS }} c-files lite-generated-files
    - name: only-test-amd64-files-lite
      run: opam exec -- bash etc/ci/github-actions-make.sh -j${{ env.NJOBS }} only-test-amd64-files-lite SLOWEST_FIRST=1
    - name: aggregate timing files for upload
      run: |
        $files = Get-ChildItem -Path . -Filter "*.timing" -Recurse
        $files | ForEach-Object { Write-Output "Adding: $_" }
        $files | Compress-Archive -DestinationPath timing-files.zip -Force
      shell: pwsh
      if: failure()
    - name: upload generated timing files
      uses: actions/upload-artifact@v4
      with:
        name: timing-files-windows
        path: timing-files.zip
      if: failure()
    - name: upload OCaml files
      uses: actions/upload-artifact@v4
      with:
        name: ExtractionOCaml
        path: src/ExtractionOCaml
    - name: upload js_of_ocaml files
      uses: actions/upload-artifact@v4
      with:
        name: ExtractionJsOfOCaml
        path: src/ExtractionJsOfOCaml
    - name: upload standalone files
      uses: actions/upload-artifact@v4
      with:
        name: standalone-windows
        path: dist/fiat_crypto.exe
    - name: upload standalone js files
      uses: actions/upload-artifact@v4
      with:
        name: standalone-html-windows
        path: fiat-html
    - name: install
      run: opam exec -- bash etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
    - name: install-without-bedrock2
      run: opam exec -- bash etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
    - name: install-dev
      run: opam exec -- bash etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
    - name: display timing info
      run: type time-of-build-pretty.log
      shell: cmd
    - name: display per-line timing info
      run: etc/ci/github-actions-display-per-line-timing.sh
      shell: bash
#    - name: upload timing and .vo info
#      uses: actions/upload-artifact@v4
#      with:
#        name: build-outputs
#        path: .
#      if: always ()
#    - name: validate
#      run: |
#        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"'
#      shell: cmd
#      if: github.event_name != 'pull_request'

  test-standalone:
    runs-on: windows-latest
    needs: build
    steps:
    - uses: actions/checkout@v4
    - name: Download standalone Windows
      uses: actions/download-artifact@v4
      with:
        name: standalone-windows
        path: dist/
    - name: List files
      run: Get-ChildItem dist -Name
    - run: .\dist\fiat_crypto.exe  -h
    - run: .\dist\fiat_crypto.exe word-by-word-montgomery -h
    - run: .\dist\fiat_crypto.exe unsaturated-solinas -h
    - run: .\dist\fiat_crypto.exe saturated-solinas -h
    - run: .\dist\fiat_crypto.exe base-conversion -h
    - name: Set up MSVC Environment for dumpbin
      uses: ilammy/msvc-dev-cmd@v1
    - name: Check Executable Dependencies
      run: |
        Write-Host "::group::File Info - fiat_crypto"
        Get-Item .\dist\fiat_crypto.exe | Format-List
        dumpbin.exe /headers .\dist\fiat_crypto.exe
        Write-Host "::endgroup::"

        Write-Host "::group::DLL Dependencies - fiat_crypto"
        dumpbin.exe /dependents .\dist\fiat_crypto.exe
        Write-Host "::endgroup::"

  publish-standalone:
    runs-on: ubuntu-latest
    needs: build
    permissions:
      contents: write  # IMPORTANT: mandatory for making GitHub Releases
    steps:
    - uses: actions/checkout@v4
      with:
        fetch-depth: 0 # Fetch all history for all tags and branches
        tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
    - name: Download standalone Windows
      uses: actions/download-artifact@v4
      with:
        name: standalone-windows
        path: dist/
    - name: List files
      run: find dist
    - name: Rename files
      run: |
        arch="$(etc/ci/find-arch.sh dist/fiat_crypto.exe "x86_64")"
        tag="$(git describe --tags HEAD)"
        fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe"
        echo "$fname"
        mv dist/fiat_crypto.exe "dist/$fname"
        find dist
    - name: Upload artifacts to GitHub Release
      env:
        GITHUB_TOKEN: ${{ github.token }}
      # Upload to GitHub Release using the `gh` CLI.
      # `dist/` contains the built packages
      run: >-
        gh release upload
        '${{ github.ref_name }}' dist/**
        --repo '${{ github.repository }}'
      if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}

  windows-check-all:
    runs-on: ubuntu-latest
    needs: [build, test-standalone, publish-standalone]
    if: always()
    steps:
    - run: echo 'build passed'
      if: ${{ needs.build.result == 'success' }}
    - run: echo 'test-standalone passed'
      if: ${{ needs.test-standalone.result == 'success' }}
    - run: echo 'publish-standalone passed'
      if: ${{ needs.publish-standalone.result == 'success' }}
    - run: echo 'build failed' && false
      if: ${{ needs.build.result != 'success' }}
    - run: echo 'test-standalone failed' && false
      if: ${{ needs.test-standalone.result != 'success' }}
    - run: echo 'publish-standalone failed' && false
      if: ${{ needs.publish-standalone.result != 'success' }}