Skip to content

[vendor] Bump Coq #3049

[vendor] Bump Coq

[vendor] Bump Coq #3049

Workflow file for this run

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 exec -- make opam-deps
opam pin add js_of_ocaml-compiler --dev -y
opam pin add js_of_ocaml --dev -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,rocq-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