index and install plus new readme #1115
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: CI | |
| on: | |
| push: | |
| branches: [master] | |
| pull_request: | |
| branches: [master] | |
| merge_group: | |
| workflow_dispatch: | |
| env: | |
| NODE_VERSION: 18 | |
| DOCKER_TEST_TAG: gillian:test | |
| jobs: | |
| build: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| operating-system: [macos-latest, ubuntu-latest] | |
| runs-on: ${{ matrix.operating-system }} | |
| steps: | |
| - name: Setup Z3 | |
| id: z3 | |
| uses: cda-tum/setup-z3@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-python@v4 | |
| with: | |
| python-version: "3.10" | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: "ocaml-variants.5.2.0+options" | |
| - name: Installing Python prerequisites | |
| run: sudo pip install sphinx furo | |
| - name: Restore Cache | |
| id: restore-cache | |
| uses: actions/cache@v3 | |
| env: | |
| cache-name: cache-ocaml | |
| with: | |
| path: _opam | |
| key: ${{ runner.os }}-${{ env.cache-name}}-ocaml-5.2.0-${{ hashFiles('**/*.opam') }} | |
| restore-keys: | | |
| ${{ runner.os }}-${{ env.cache-name}}-ocaml-5.2.0 | |
| - name: Install dependencies | |
| run: make init-ci | |
| - name: Build Gillian | |
| run: opam exec -- dune build @all | |
| - name: Basic tests | |
| run: opam exec -- dune test | |
| - name: Wisl checks | |
| run: "opam exec -- dune exec -- bash ./wisl/scripts/quicktests.sh" | |
| - name: Format checking | |
| run: opam exec -- dune fmt | |
| - name: Installing to opam switch | |
| run: | | |
| opam exec -- dune build @install | |
| opam install . -y | |
| - name: Compressing artifact | |
| run: tar czf opam.tar.gz _opam | |
| - name: Sending artifact for next jobs | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-opam | |
| path: opam.tar.gz | |
| - name: Building docs | |
| run: make docs | |
| if: runner.os == 'Linux' | |
| - name: Sending docs artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-docs | |
| path: _docs | |
| if: runner.os == 'Linux' | |
| - name: Setting dependency cache | |
| run: opam clean | |
| if: steps.restore-cache.outputs.cache-hit != 'true' | |
| gillian_c_tests: | |
| strategy: | |
| matrix: | |
| operating-system: [ubuntu-latest] | |
| runs-on: ${{ matrix.operating-system }} | |
| needs: build | |
| steps: | |
| - name: Setup Z3 | |
| id: z3 | |
| uses: cda-tum/setup-z3@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: "ocaml-variants.5.2.0+options" | |
| - name: Checkout project | |
| uses: actions/checkout@v3 | |
| with: | |
| path: Gillian | |
| - name: Download release | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-opam | |
| path: opam | |
| - name: Extract release | |
| run: | | |
| tar xzf opam/opam.tar.gz | |
| rm -rf opam | |
| - name: init env | |
| run: "Gillian-C/scripts/setup_environment.sh" | |
| working-directory: "Gillian" | |
| - name: Test All | |
| run: "./testAll.sh" | |
| working-directory: "Gillian/Gillian-C/environment/" | |
| - name: Test Amazon | |
| run: "make" | |
| working-directory: "Gillian/Gillian-C/examples/amazon/" | |
| gillian_js_tests: | |
| strategy: | |
| matrix: | |
| operating-system: [ubuntu-latest] | |
| runs-on: ${{ matrix.operating-system }} | |
| needs: build | |
| steps: | |
| - name: Setup Z3 | |
| id: z3 | |
| uses: cda-tum/setup-z3@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: "ocaml-variants.5.2.0+options" | |
| - name: Checkout project | |
| uses: actions/checkout@v3 | |
| with: | |
| path: Gillian | |
| - name: Download release | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-opam | |
| path: opam | |
| - name: Extract release | |
| run: | | |
| tar xzf opam/opam.tar.gz | |
| rm opam -rf | |
| - name: init env | |
| run: "Gillian-JS/scripts/setup_environment.sh" | |
| working-directory: "Gillian" | |
| - name: Test JaVerT | |
| run: "./testJaVerT.sh" | |
| working-directory: "Gillian/Gillian-JS/environment/" | |
| # - name: Test Amazon | |
| # run: "make" | |
| # working-directory: "Gillian/Gillian-JS/Examples/Amazon/" | |
| kanillian_c_tests: | |
| strategy: | |
| matrix: | |
| operating-system: [ubuntu-latest] | |
| runs-on: ${{ matrix.operating-system }} | |
| needs: build | |
| steps: | |
| - name: Setup Z3 | |
| id: z3 | |
| uses: cda-tum/setup-z3@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: "ocaml-variants.5.2.0+options" | |
| - name: install CBMC | |
| run: sudo apt install cbmc -y | |
| - name: Checkout project | |
| uses: actions/checkout@v3 | |
| with: | |
| path: Gillian | |
| - name: Download release | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-opam | |
| path: opam | |
| - name: Extract release | |
| run: | | |
| tar xzf opam/opam.tar.gz | |
| rm -rf opam | |
| - name: init env | |
| run: "kanillian/scripts/setup_environment.sh" | |
| working-directory: "Gillian" | |
| - name: Test All | |
| run: "opam exec -- bash ./testAll.sh" | |
| working-directory: "Gillian/kanillian/environment/" | |
| test262: | |
| if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master') | |
| strategy: | |
| matrix: | |
| operating-system: [ubuntu-latest] | |
| runs-on: ${{ matrix.operating-system }} | |
| needs: build | |
| steps: | |
| - name: Setup Z3 | |
| id: z3 | |
| uses: cda-tum/setup-z3@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: "ocaml-variants.5.2.0+options" | |
| - name: Checkout project | |
| uses: actions/checkout@v3 | |
| with: | |
| repository: GillianPlatform/javert-test262 | |
| path: test262 | |
| ref: 93e0d0b04093cabc3234a776eec5cc3e165f3b1a | |
| - name: Download release | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-opam | |
| path: opam | |
| - name: Extract release | |
| run: | | |
| tar xzf opam/opam.tar.gz | |
| rm -rf opam | |
| - name: Test262 | |
| run: "opam exec -- gillian-js test262 test262/test --ci" | |
| collections-c: | |
| if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master') | |
| strategy: | |
| matrix: | |
| operating-system: [ubuntu-latest] | |
| runs-on: ${{ matrix.operating-system }} | |
| needs: build | |
| steps: | |
| - name: Setup Z3 | |
| id: z3 | |
| uses: cda-tum/setup-z3@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: "ocaml-variants.5.2.0+options" | |
| - name: checkout project | |
| uses: actions/checkout@v3 | |
| with: | |
| repository: GillianPlatform/collections-c-for-gillian | |
| path: collections-c | |
| ref: ffa76e788a1fbdb67910bb7b794214ebc22c1b8c | |
| - name: Download release | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-opam | |
| path: opam | |
| - name: Extract release | |
| run: | | |
| tar xzf opam/opam.tar.gz | |
| rm -rf opam | |
| - name: Symbolic Testing Collections-C | |
| run: "opam exec -- bash ./scripts/gillian-compcert/runTests.sh" | |
| working-directory: collections-c | |
| # test-Buckets: | |
| # if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master') | |
| # strategy: | |
| # matrix: | |
| # operating-system: [macos-latest] | |
| # runs-on: ${{ matrix.operating-system }} | |
| # needs: build | |
| # steps: | |
| # - name: Setup Z3 | |
| # id: z3 | |
| # uses: cda-tum/setup-z3@v1 | |
| # env: | |
| # GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # - uses: ocaml/setup-ocaml@v2 | |
| # with: | |
| # ocaml-compiler: "ocaml-variants.5.2.0+options" | |
| # - name: Checkout project | |
| # uses: actions/checkout@v3 | |
| # with: | |
| # path: Gillian | |
| # - name: Download release | |
| # uses: actions/download-artifact@v4 | |
| # with: | |
| # name: ${{ runner.os }}-opam | |
| # path: opam | |
| # - name: Extract release | |
| # run: | | |
| # tar xzf opam/opam.tar.gz | |
| # rm -rf opam | |
| # - name: Symbolic Testing Buckets.js | |
| # run: "opam exec -- gillian-js cosette-bulk Gillian/Gillian-JS/Examples/Cosette/Buckets --ci" | |
| build-docker: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| - name: Set up docker buildx | |
| uses: docker/setup-buildx-action@v2 | |
| with: | |
| driver: docker | |
| - name: Restore Cache | |
| id: restore-cache | |
| uses: actions/cache@v3 | |
| env: | |
| cache-name: cache-ocaml | |
| with: | |
| path: .docker_opam_cache | |
| key: docker-${{ env.cache-name }}-ocaml-5.2.0-${{ hashFiles('**/*.opam') }} | |
| restore-keys: | | |
| docker-${{ env.cache-name }}-ocaml-5.2.0 | |
| - name: Build and export docker image | |
| uses: docker/build-push-action@v4 | |
| with: | |
| context: . | |
| load: true | |
| tags: ${{ env.DOCKER_TEST_TAG }} | |
| target: test | |
| - name: Dune test | |
| run: docker run --rm ${{ env.DOCKER_TEST_TAG }} opam exec -- dune test | |
| - name: Extract cache | |
| if: steps.restore-cache.outputs.cache-hit != 'true' | |
| run: | | |
| rm -rf .docker_opam_cache | |
| docker run --name deps ${{ env.DOCKER_TEST_TAG }} bash -c "opam clean" | |
| docker cp deps:/home/opam/.opam/5.2 ./.docker_opam_cache | |
| docker rm deps | |
| deploy-docs: | |
| if: github.ref == 'refs/heads/master' | |
| runs-on: ubuntu-latest | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| operating-system: [ubuntu-latest] | |
| steps: | |
| - name: Download built docs | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ runner.os }}-docs | |
| path: docs | |
| - name: Deploy docs | |
| run: | | |
| git config --global user.email "<>" | |
| git config --global user.name "GitHub Actions" | |
| git clone https://${{ secrets.DOCS_USER }}:${{ secrets.DOCS_TOKEN }}@github.com/GillianPlatform/GillianPlatform.github.io.git docs-repo --branch master | |
| cd docs-repo | |
| rm * -rf | |
| cp -r ../docs/* . | |
| git add -A | |
| git commit --allow-empty -m "Deployment from $GITHUB_REPOSITORY@$GITHUB_SHA" | |
| git push --force |