Merge pull request #375 from toku-sa-n/support-extraction #386
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 | |
| - 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 | |
| - main | |
| # Allows you to run this workflow manually from the Actions tab | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| ocaml-compiler: [4.09.x, 4.10.x, 4.11.x, 4.12.x, 4.13.x, 4.14.x] | |
| test-target: [test] | |
| extra-opam: [coq.dev coq-mathcomp-ssreflect.1.dev] | |
| include: | |
| - ocaml-compiler: 4.13.1 | |
| 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@v3 | |
| - 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 | |
| - name: Basic OPAM setup for SerAPI | |
| run: | | |
| eval $(opam env) | |
| opam repos add coq-released http://coq.inria.fr/opam/released | |
| opam repos add coq-core-dev http://coq.inria.fr/opam/core-dev | |
| # Only for mathcomp.dev which is needed for 8.16, remove when math-comp is fixed | |
| opam repos add coq-extra-dev http://coq.inria.fr/opam/extra-dev | |
| # coq-serapi already pinned by the setup-ocaml@v2 action | |
| opam install --deps-only coq-serapi | |
| - name: Display OPAM Setup | |
| run: | | |
| eval $(opam env) | |
| opam list | |
| - name: Install Coq via git | |
| if: ${{ matrix.coq-from-git }} | |
| run: | | |
| eval $(opam env) | |
| # 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 | |
| # Update to coq-core some day | |
| # opam install --deps-only coq-core | |
| opam install --deps-only coq-core | |
| git clone --depth=3 -b "$COQ_BRANCH" "$COQ_REPOS" "$HOME/coq-$COQ_BRANCH" | |
| # Upstream 'make -C "$HOME/coq-$COQ_BRANCH" world' target now builds coqide | |
| cd "$HOME/coq-$COQ_BRANCH" | |
| ./configure -prefix "$HOME/coq-$COQ_BRANCH/_build/install/default/" | |
| make dunestrap | |
| dune build -p coq-core,coq-stdlib,coq | |
| cd "$HOME" | |
| # Install math-comp using Coq from git | |
| PATH="$HOME/coq-$COQ_BRANCH/_build/install/default/bin:$PATH" | |
| git clone --depth=3 -b mathcomp-1 https://github.com/math-comp/math-comp.git | |
| make -C math-comp/mathcomp/ssreflect | |
| make -C math-comp/mathcomp/ssreflect install | |
| - name: Extra OPAM Setup (Coq.dev, misc extra tools) | |
| if: ${{ matrix.extra-opam != '' }} | |
| run: | | |
| eval $(opam env) | |
| opam install ${{ matrix.extra-opam }} | |
| - name: Build and Test SerAPI | |
| run: | | |
| eval $(opam env) | |
| make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME" "${{ matrix.test-target }}" | |
| ls -lR _build/install/default/ || true |