Skip to content

Fix-ups for "significant proof checking refactoring" #58

Fix-ups for "significant proof checking refactoring"

Fix-ups for "significant proof checking refactoring" #58

Workflow file for this run

name: Build and test
on:
push:
branches:
- main
pull_request:
branches:
- main
- 'v[0-9]+.[0-9]+.[0-9]+-dev'
workflow_dispatch:
workflow_call:
outputs:
artifactName:
description: "The name of the build artifact (packaged extension)."
value: ${{ jobs.build-and-test.outputs.artifactName }}
vsixPath:
description: "The path to the packaged and published VSIX file."
value: ${{ jobs.build-and-test.outputs.vsixPath }}
env:
coqlsp-path: "coq-lsp"
coqlsp-version: "0.2.2+8.19"
artifact-name: ubuntu-latest-build
jobs:
build-and-test:
strategy:
matrix:
os: [ubuntu-latest, macos-latest]
ocaml-compiler: [4.14]
runs-on: ${{ matrix.os }}
outputs:
artifactName: ${{ env.artifact-name }}
vsixPath: ${{ steps.package-extension.outputs.vsixPath }}
steps:
- name: Checkout tree
uses: actions/checkout@v4
# For some reason, the most significant thing for caching opam dependencies properly
# is `dune-cache: true` instead of this caching action.
- name: Restore cached opam dependencies
id: cache-opam
uses: actions/cache@v4
with:
path: ~/.opam/
key: opam-${{ matrix.os }}-${{ matrix.ocaml-compiler }}-${{ env.coqlsp-version }}
restore-keys: opam-${{ matrix.os }}-${{ matrix.ocaml-compiler }}-
- name: Set-up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/[email protected]
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}
dune-cache: true
- name: Install opam dependencies
env:
OPAMYES: true
run: |
opam install coq-lsp.0.2.2+8.19
eval $(opam env)
- name: Install Node.js
uses: actions/setup-node@v4
with:
node-version-file: ".nvmrc"
- run: npm ci
- name: Check coq-lsp version
env:
OPAMYES: true
run: |
opam list coq-lsp
eval $(opam env)
which coq-lsp
- name: Check if coq-lsp is in PATH
run: |
eval $(opam env)
if ! command -v coq-lsp &> /dev/null
then
echo "coq-lsp could not be found"
fi
echo "coqlsppath=`which coq-lsp`" >> $GITHUB_ENV
shell: bash
- name: Test on Linux
if: runner.os == 'Linux'
env:
COQ_LSP_PATH: ${{ env.coqlsp-path }}
run: |
eval $(opam env)
xvfb-run -a npm run clean-test
- name: Test not on Linux
if: runner.os != 'Linux'
env:
COQ_LSP_PATH: ${{ env.coqlsp-path }}
run: |
eval $(opam env)
npm run clean-test
- name: Package Extension
id: package-extension
uses: HaaLeo/publish-vscode-extension@v1
with:
pat: stub
dryRun: true
- name: Upload Extension Package as Artifact
if: matrix.os == 'ubuntu-latest'
id: upload-artifact
uses: actions/upload-artifact@v4
with:
name: ${{ env.artifact-name }}
path: ${{ steps.package-extension.outputs.vsixPath }}
setup-ci-debug-session:
name: Start a CI debug session if build or test fail
needs: [build-and-test]
if: always()
strategy:
matrix:
os: [ubuntu-latest]
ocaml-compiler: [4.14]
runs-on: ${{ matrix.os }}
steps:
- name: Setup tmate session
if: ${{ failure() }}
uses: mxschmitt/action-tmate@v3