Link elm and rust extraction documentation (#244) #647
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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" | |
| git config --global url.https://github.com/.insteadOf [email protected]: | |
| 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: [email protected] | |
| 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 |