build.yml

name: Build
on:
  push:
    branches:
    - 'master'
    paths-ignore:
    - '**.md'
    - '**.gitignore'
    - '**.opam'
    - '**.editorconfig'
    - 'LICENSE'
    - 'papers/**'
    - 'extra/docker/**'
  pull_request:
    paths-ignore:
    - '**.md'
    - '**.gitignore'
    - '**.opam'
    - '**.editorconfig'
    - 'LICENSE'
    - 'papers/**'
    - 'extra/docker/**'
permissions:
  contents: read
env:
  OCAML_COMILER_VERSION: "4.13.1"
  JOBS: 2
jobs:
  build:
    runs-on: ubuntu-latest
    permissions:
      contents: write
    steps:
      - name: Checkout branch ${{ github.ref_name }}
        uses: actions/checkout@v4

      - run: sudo apt-get update
      - name: Restore opam cache
        id: opam-cache
        uses: actions/cache@v4
        with:
          path: "~/.opam"
          key: opam-${{env.OCAML_COMILER_VERSION}}-${{hashFiles('.github/coq-concert.opam.locked')}}
          restore-keys: |
            opam-${{env.OCAML_COMILER_VERSION}}-

      - name: Set up OCaml
        uses: avsm/setup-ocaml@v1
        with:
          ocaml-version: ${{env.OCAML_COMILER_VERSION}}

      - name: Build dependencies
        #if: ${{ !steps.opam-cache.outputs.cache-hit }}
        run: |
          opam repo add coq-released https://coq.inria.fr/opam/released
          opam install --deps-only -j${{ env.JOBS }} .github/coq-concert.opam.locked
          opam install -y -j${{ env.JOBS }} coq-dpdgraph
          opam clean -a -c -s --logs

      - name: Set up environment
        run: |
          echo "::group::Setting up problem matcher"
          echo "::add-matcher::./.github/coq-errors.json"
          echo "::endgroup::"

      - name: Build core
        run: |
          echo "::group::Build utilities"
          opam exec -- make -j${{ env.JOBS }} utils
          echo "::endgroup::"

          echo "::group::Build execution layer"
          opam exec -- make -j${{ env.JOBS }} execution
          echo "::endgroup::"

          echo "::group::Build embedding layer"
          opam exec -- make -j${{ env.JOBS }} embedding
          echo "::endgroup::"

          echo "::group::Build extraction layer"
          opam exec -- make -j${{ env.JOBS }} extraction
          echo "::endgroup::"

      - name: Build examples
        run: |
          echo "::group::Build examples"
          opam exec -- make -j${{ env.JOBS }} examples
          echo "::endgroup::"

      - name: Set up Rust
        uses: actions-rs/toolchain@v1
        with:
          toolchain: 1.69.0
          target: wasm32-unknown-unknown
      - name: Set up Concordium tools
        run: |
          curl -L -O https://distribution.concordium.software/tools/linux/cargo-concordium_1.0.0
          sudo chmod +x cargo-concordium_1.0.0
          sudo mv cargo-concordium_1.0.0 /usr/local/bin/cargo-concordium

      - name: Set up LIGO v0.59.0
        run: |
          curl -L -O https://gitlab.com/ligolang/ligo/-/jobs/3553205311/artifacts/raw/ligo
          sudo chmod +x ./ligo
          sudo mv ligo /usr/local/bin/

      - name: Set up Liquidity
        run: |
          sudo chmod +x ./extra/docker/liquidity
          sudo mv extra/docker/liquidity /usr/local/bin/

      - name: Test extraction
        run: |
          echo "::group::Running tests"
          make -j${{ env.JOBS }} test-extraction
          echo "::endgroup::"

      - name: Upload Liquidity extraction logs
        if: false # Do we still want these logs?
        uses: actions/upload-artifact@v4
        with:
          name: Liquidity logs
          path: extraction/tests/extracted-code/liquidity-extract/liquidity.log
          retention-days: 14

      - name: Prepare extraction results
        if: github.event_name == 'push' && github.repository == 'AU-COBRA/ConCert' && github.ref == 'refs/heads/master'
        run: |
          echo "::group::Cleaning up extracted code"
          make -j${{ env.JOBS }} clean-extraction-out-files
          make -j${{ env.JOBS }} clean-compiled-extraction
          find extraction/tests/extracted-code -name 'placeholder' -delete
          echo "::endgroup::"

          cp LICENSE extraction/tests/extracted-code/LICENSE
          cp extra/extraction-results.md extraction/tests/extracted-code/README.md
          cp .gitattributes extraction/tests/extracted-code/.gitattributes

      - name: Push to the extraction results repository
        # don't push the extraction results on pull requests and push only from the master branch of the AU-COBRA/ConCert repo.
        if: github.event_name == 'push' && github.repository == 'AU-COBRA/ConCert' && github.ref == 'refs/heads/master'
        uses: cpina/github-action-push-to-another-repository@main
        env:
          SSH_DEPLOY_KEY: ${{ secrets.EXTRACTION_RESULTS_DEPLOY_KEY }}
        with:
          source-directory: 'extraction/tests/extracted-code'
          destination-github-username: 'AU-COBRA'
          destination-repository-name: 'extraction-results'
          user-email: danil.v.annenkov@gmail.com
          commit-message: See ORIGIN_COMMIT from $GITHUB_REF
          target-branch: master

      - name: Build documentation
        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
        run: |
          echo "::group::Running coqdoc"
          opam exec -- make -j${{ env.JOBS }} html
          echo "::endgroup::"

          echo "::group::Install dependencies"
          sudo apt install -y graphviz
          echo "::endgroup::"

          echo "::group::Generate dependency graphs"
          rm -rf docs/graphs
          mkdir -p docs
          mkdir -p docs/graphs

          opam exec -- make dependency-graphs
          mv utils/svg/* docs/graphs/
          mv execution/svg/* docs/graphs/
          mv embedding/svg/* docs/graphs/
          mv extraction/svg/* docs/graphs/
          mv examples/svg/* docs/graphs/
          echo "::endgroup::"

      - name: Prepare documentation for deployment
        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
        uses: actions/upload-pages-artifact@v3
        with:
          path: docs

  deploy-docs:
    if: github.event_name == 'push' && github.ref == 'refs/heads/master'
    needs: build
    runs-on: ubuntu-latest
    permissions:
      pages: write
      id-token: write
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4