build.yml

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 https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y
          opam pin add js_of_ocaml https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -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,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