diff --git a/.github/Dockerfile b/.github/Dockerfile index eefec40f..0256694c 100644 --- a/.github/Dockerfile +++ b/.github/Dockerfile @@ -1,4 +1,4 @@ -FROM coqorg/coq:8.17.1 +FROM coqorg/coq:8.17.1-ocaml-4.14.1-flambda ENV NCPUS=4 ENV OPAMYES="true" diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml new file mode 100644 index 00000000..98d730b0 --- /dev/null +++ b/.github/workflows/ci_build.yaml @@ -0,0 +1,75 @@ +name: CI build +on: + push: + branches: + - main + pull_request: + branches: + - main + +env: + REGISTRY: "ghcr.io" + IMAGE_TAG: "beluga-lang/mcltt:main" + +jobs: + wf: + name: Completeness of _CoqProject + runs-on: ubuntu-latest + steps: + - name: repo checkout + uses: actions/checkout@v3 + - name: check + run: | + .github/scripts/check_projects.sh theories + + build: + name: Continuous Intergration + runs-on: ubuntu-latest + permissions: + packages: read + steps: + - name: get number of CPU cores + uses: SimenB/github-actions-cpu-cores@v2 + id: cpu-cores + + - name: repo checkout + uses: actions/checkout@v3 + + - name: container registry log in + uses: docker/login-action@v3 + with: + registry: ${{ env.REGISTRY }} + username: ${{ github.actor }} + password: ${{ secrets.GITHUB_TOKEN }} + + - name: image pre-pulling + run: docker pull ${{ env.REGISTRY }}/${{ env.IMAGE_TAG }} + + - name: coq processing + uses: coq-community/docker-coq-action@v1 + with: + custom_image: ${{ env.REGISTRY }}/${{ env.IMAGE_TAG }} + install: | + before_script: | + startGroup "Fix the permission issue" + sudo chown -R coq:coq . + endGroup + script: | + startGroup "Build Coq lib" + cd theories/ + make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed + endGroup + after_script: | + startGroup "Test parser" + dune build + dune runtest + endGroup + export: "OPAMJOBS OPAMYES" + env: + OPAMJOBS: ${{ steps.cpu-cores.outputs.count }} + OPAMYES: "true" + + - name: permissions revert + # to avoid a warning at cleanup time + if: ${{ always() }} + run: sudo chown -R 1001:116 . diff --git a/.github/workflows/ci_build.yml b/.github/workflows/ci_build.yml deleted file mode 100644 index 9e2762a9..00000000 --- a/.github/workflows/ci_build.yml +++ /dev/null @@ -1,63 +0,0 @@ -name: CI build -on: - push: - branches: - - main - pull_request: - branches: - - main - -env: - OCAML_VER: "4.14.0" - COQ_VER: "8.17.1" - -jobs: - wf: - name: Completeness of _CoqProject - runs-on: ubuntu-latest - steps: - - name: repo checkout - uses: actions/checkout@v3 - - name: check - run: | - .github/scripts/check_projects.sh theories - - build: - name: Continuous Intergration - runs-on: ubuntu-latest - steps: - - name: Get number of CPU cores - uses: SimenB/github-actions-cpu-cores@v2 - id: cpu-cores - - name: repo checkout - uses: actions/checkout@v3 - - name: setup OCaml - uses: ocaml/setup-ocaml@v2 - with: - ocaml-compiler: ${{ env.OCAML_VER }} - dune-cache: true - cache-prefix: "v2.2" - - name: install Menhir and Coq - run: | - opam update - opam install menhir - opam pin add coq "${{ env.COQ_VER }}" - - name: install Coq dependencies - run: | - opam repo add coq-released https://coq.inria.fr/opam/released - opam update - opam install coq-equations - opam install coq-menhirlib - opam install ppx_inline_test - env: - OPAMYES: "true" - - name: build lib - run: | - eval $(opam env) - cd theories/ - make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed - - name: test parser - run: | - eval $(opam env) - dune build - dune runtest diff --git a/README.md b/README.md index 0cd82b18..ba2f4792 100644 --- a/README.md +++ b/README.md @@ -47,7 +47,7 @@ implementation. ## Dependencies -* OCaml 4.14.0 +* OCaml 4.14.1 * Menhir * coq-menhirlib * Coq 8.17.1 @@ -56,7 +56,7 @@ implementation. We recommend to install dependencies in the following way: ```bash -opam switch create coq-8.17.1 4.14.0 +opam switch create coq-8.17.1 4.14.1 opam install menhir opam pin add coq 8.17.1 opam repo add coq-released https://coq.inria.fr/opam/released