Adapt to coq/coq#19927 (coq-core renamed to rocq-runtime) #3056
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@v4 | |
| 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-js: | |
| name: Web Worker Build | |
| strategy: | |
| fail-fast: false | |
| runs-on: ubuntu-latest | |
| steps: | |
| # OPAM figures out everything but the libgmp-dev:i386 | |
| # dependency, maybe worth fixing this upstream in the opam | |
| # repository | |
| - 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 -o Acquire::Retries=30 install gcc-multilib g++-multilib pkg-config libgmp-dev libgmp-dev:i386 -y | |
| - name: 🔭 Checkout code | |
| uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: 🐫 Setup OCaml | |
| uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: "ocaml-variants.4.14.2+options,ocaml-option-32bit" | |
| dune-cache: true | |
| - name: 🐫🐪🐫 Get dependencies | |
| run: | | |
| opam update | |
| opam exec -- make opam-deps | |
| opam pin add js_of_ocaml-compiler -k version 5.9.1 -y | |
| opam pin add js_of_ocaml -k version 5.9.1 -y | |
| opam install zarith_stubs_js js_of_ocaml-ppx -y | |
| - name: 💉💉💉 Patch Coq | |
| run: make patch-for-js | |
| - name: 🦏🧱🦏 Build coq-lsp JS version 🦏🦏🦏 | |
| run: | | |
| opam exec -- make controller-js/coq-fs-core.js | |
| opam exec -- make js | |
| - name: 🚀 Setup node | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: 22 | |
| - name: 🦏🧱🦏 Build coq-lsp VSCode extension 🦏🦏🦏 | |
| run: opam exec -- make extension | |
| - name: Upload artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: coq-lsp_worker and front-end | |
| path: | | |
| editor/code/package.json | |
| editor/code/README.md | |
| editor/code/CHANGELOG.md | |
| editor/code/syntaxes | |
| editor/code/out/ | |
| editor/code/coq.configuration.json | |
| compression-level: 9 | |
| build-opam: | |
| name: Opam dev install | |
| strategy: | |
| fail-fast: false | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 🔭 Checkout code | |
| uses: actions/checkout@v4 | |
| 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,rocq-core,stdlib/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@v4 | |
| with: | |
| submodules: recursive | |
| - name: ❄️ Setup Nix | |
| uses: cachix/install-nix-action@v27 | |
| - 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@v4 | |
| - name: 🚀 Setup node | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: 22 | |
| - 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@v4 | |
| with: | |
| submodules: recursive | |
| - name: ❄️ Setup Nix | |
| uses: cachix/install-nix-action@v18 | |
| - name: 📐 Run flake check | |
| run: nix flake check |