Adapt to Coq PR #19301: unify the syntax of definition and theorem #3027
Workflow file for this run
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: Github CI | |
| on: | |
| push: | |
| branches: | |
| - main | |
| - v8.20 | |
| - v8.19 | |
| - v8.18 | |
| - v8.17 | |
| - v8.16 | |
| - v8.15 | |
| pull_request: | |
| branches: | |
| - main | |
| - v8.20 | |
| - v8.19 | |
| - v8.18 | |
| - v8.17 | |
| - v8.16 | |
| - v8.15 | |
| # Cancels previous runs of the same workflow | |
| concurrency: | |
| group: "${{ github.workflow }} @ ${{ github.event.pull_request.head.label || github.head_ref || github.ref }}" | |
| cancel-in-progress: true | |
| jobs: | |
| build: | |
| strategy: | |
| matrix: | |
| include: | |
| - os: ubuntu-latest | |
| ocaml: 4.14.x | |
| - os: ubuntu-latest | |
| ocaml: 4.13.x | |
| - os: ubuntu-latest | |
| ocaml: 4.12.x | |
| - os: ubuntu-latest | |
| ocaml: 5.0.x | |
| - os: ubuntu-latest | |
| ocaml: 5.1.x | |
| - os: ubuntu-latest | |
| ocaml: 5.2.x | |
| - os: macos-latest | |
| ocaml: 4.14.x | |
| - name: Windows Latest | |
| ocaml: 4.14 | |
| os: windows-latest | |
| opam-repositories: | | |
| windows-5.0: https://github.com/dra27/opam-repository.git#windows-5.0 | |
| opam-repository-mingw: https://github.com/ocaml-opam/opam-repository-mingw.git#sunset | |
| default: https://github.com/ocaml/opam-repository.git | |
| fail-fast: false | |
| runs-on: ${{ matrix.os }} | |
| timeout-minutes: 45 | |
| steps: | |
| - name: 🔭 Checkout code | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: 🐫 Setup OCaml | |
| uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml }} | |
| dune-cache: true | |
| opam-repositories: ${{ matrix.opam-repositories }} | |
| - name: 🐫🐪🐫 Get dependencies | |
| run: opam exec -- make opam-deps | |
| - name: 🐛 Special Windows Config [only on Win CI] | |
| if: matrix.os == 'windows-latest' | |
| run: opam exec -- make winconfig | |
| - name: 🧱 Build coq-lsp | |
| run: opam exec -- make build | |
| - name: 🐛 Test coq-lsp | |
| run: opam exec -- make test | |
| - name: 🐛 Test fcc | |
| run: opam exec -- make test-compiler | |
| build-opam: | |
| name: Opam dev install | |
| strategy: | |
| fail-fast: false | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 🔭 Checkout code | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: 🐫 Setup OCaml | |
| uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: 4.14.x | |
| dune-cache: true | |
| - name: Install Coq and SerAPI into OPAM switch | |
| run: | | |
| opam install lwt logs # Also build pet-server | |
| opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops | |
| opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam | |
| - name: Install `coq-lsp` into OPAM switch | |
| run: opam install . | |
| - name: Test `coq-lsp` in installed switch | |
| run: opam exec -- fcc examples/Demo.v | |
| - name: Test `pet-server` is built | |
| run: opam exec -- which pet-server | |
| build-nix: | |
| name: Nix | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macOS-latest] | |
| fail-fast: false | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: 🔭 Checkout code | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: ❄️ Setup Nix | |
| uses: cachix/install-nix-action@v22 | |
| - name: 🧱 Build coq-lsp | |
| run: nix build .?submodules=1 | |
| client-compile: | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: ./editor/code | |
| steps: | |
| - name: 🔭 Checkout code | |
| uses: actions/checkout@v3 | |
| - name: 🚀 Setup node | |
| uses: actions/setup-node@v3 | |
| with: | |
| node-version: 18 | |
| - run: npm ci | |
| - run: npx --yes @vscode/vsce ls | |
| nix-flake-check: | |
| name: Nix Flake Check | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 🔭 Checkout code | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: ❄️ Setup Nix | |
| uses: cachix/install-nix-action@v18 | |
| - name: 📐 Run flake check | |
| run: nix flake check |