Merge pull request #426 from proux01/coq_19370 #508
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: | |
| - v8.8 | |
| - v8.9 | |
| - v8.10 | |
| - v8.11 | |
| - v8.12 | |
| - v8.13 | |
| - v8.14 | |
| - v8.15 | |
| - v8.16 | |
| - v8.17 | |
| - v8.18 | |
| - v8.19 | |
| - v8.20 | |
| - main | |
| pull_request: | |
| branches: | |
| - v8.8 | |
| - v8.9 | |
| - v8.10 | |
| - v8.11 | |
| - v8.12 | |
| - v8.13 | |
| - v8.14 | |
| - v8.15 | |
| - v8.16 | |
| - v8.17 | |
| - v8.18 | |
| - v8.19 | |
| - v8.20 | |
| - main | |
| # Allows you to run this workflow manually from the Actions tab | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| ocaml-compiler: [4.12.x, 4.13.x, 4.14.x] | |
| test-target: [test] | |
| extra-opam: [coq.dev] | |
| include: | |
| - ocaml-compiler: 4.14.x | |
| test-target: test | |
| extra-opam: | |
| coq-from-git: true | |
| env: | |
| OPAMJOBS: "2" | |
| OPAMROOTISOK: "true" | |
| OPAMYES: "true" | |
| NJOBS: "2" | |
| COQ_REPOS: "https://github.com/coq/coq.git" | |
| COQ_BRANCH: "master" | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - name: Install apt dependencies | |
| run: | | |
| sudo apt-get install aptitude | |
| sudo dpkg --add-architecture i386 | |
| sudo aptitude -o Acquire::Retries=30 update -q | |
| sudo aptitude --log-resolver -o Acquire::Retries=30 install gcc-multilib libgmp-dev:i386 -y | |
| - name: Set up OCaml ${{ matrix.ocaml-compiler }} | |
| uses: avsm/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | |
| dune-cache: true | |
| opam-pin: false | |
| opam-repositories: | | |
| default: https://opam.ocaml.org | |
| coq-core-dev: http://coq.inria.fr/opam/core-dev | |
| - name: Display OPAM Setup | |
| run: opam list | |
| - name: Install SerAPI deps | |
| run: | | |
| opam install --ignore-constraints-on=coq --deps-only vendor/coq-lsp/coq-lsp.opam | |
| opam install --ignore-constraints-on=coq,coq-lsp --deps-only . | |
| - name: Install Coq via git | |
| if: ${{ matrix.coq-from-git }} | |
| run: | | |
| # We are going to install Coq in a root dir as to keep our | |
| # main working dir clean, however we need to spec the OPAM root | |
| export OPAMSWITCH="$PWD" | |
| # First we update SERAPI_COQ_HOME for future steps as per | |
| # https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable | |
| echo "SERAPI_COQ_HOME=$HOME/coq-$COQ_BRANCH/_build/install/default/lib/" >> $GITHUB_ENV | |
| # Clone Coq's repos | |
| git clone --depth=3 -b "$COQ_BRANCH" "$COQ_REPOS" "$HOME/coq-$COQ_BRANCH" | |
| # Note that Coq's 'make -C "$HOME/coq-$COQ_BRANCH" world' | |
| # target now builds coqide too | |
| cd "$HOME/coq-$COQ_BRANCH" | |
| # Install deps for Coq, and build Coq | |
| opam install --deps-only ./coq-core.opam | |
| opam exec -- ./configure -prefix "$HOME/coq-$COQ_BRANCH/_build/install/default/" | |
| opam exec -- make dunestrap | |
| opam exec -- dune build -p coq-core,coq-stdlib,coq | |
| - name: Extra OPAM Setup (Coq.dev, misc extra tools) | |
| if: ${{ matrix.extra-opam != '' }} | |
| run: opam install ${{ matrix.extra-opam }} | |
| - name: Build SerAPI | |
| run: | | |
| opam exec -- make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME" | |
| ls -lR _build/install/default/bin || true | |
| ls -l _build/install/default/lib/coq-serapi || true | |
| - name: Test SerAPI | |
| run: opam exec -- make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME" "${{ matrix.test-target }}" |