Skip to content

Commit

Permalink
[ci] Remove SerAPI from CI.
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed Nov 12, 2024
1 parent 06d8fe7 commit e11de61
Show file tree
Hide file tree
Showing 5 changed files with 1 addition and 36 deletions.
7 changes: 0 additions & 7 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -1026,13 +1026,6 @@ library:ci-rupicola:
plugin:ci-coq_lsp:
extends: .ci-template-flambda

plugin:ci-serapi:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-coq_lsp
stage: build-2

plugin:ci-vscoq:
extends: .ci-template-flambda

Expand Down
4 changes: 0 additions & 4 deletions Makefile.ci
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,6 @@ CI_TARGETS= \
ci-rewriter \
ci-riscv_coq \
ci-rupicola \
ci-serapi \
ci-serapi_test \
ci-sf \
ci-simple_io \
ci-smtcoq \
Expand Down Expand Up @@ -179,8 +177,6 @@ ci-compcert: ci-menhir ci-flocq

ci-relation_algebra: ci-aac_tactics ci-mathcomp

ci-serapi: ci-coq_lsp

ci-smtcoq_trakt: ci-trakt

# Virtual targets used by the CI to group compilation of rules in a single job
Expand Down
6 changes: 0 additions & 6 deletions dev/ci/ci-basic-overlay.sh
Original file line number Diff line number Diff line change
Expand Up @@ -504,12 +504,6 @@ project jasmin "https://github.com/jasmin-lang/jasmin" "main"
project lean_importer "https://github.com/SkySkimmer/coq-lean-import" "master"
# Contact @SkySkimmer on github

########################################################################
# SerAPI
########################################################################
project serapi "https://github.com/ejgallego/coq-serapi" "main"
# Contact @ejgallego on github

########################################################################
# SMTCoq
########################################################################
Expand Down
2 changes: 1 addition & 1 deletion dev/ci/ci-coq_lsp.sh
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,6 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
_build/install/default/bin/coq-lsp --version
dune runtest --root . test/serlib
dune runtest --root . test/compiler
# Needed by coq-serapi in CI
# It was needed by coq-serapi in CI, we keep it for now
dune install -p coq-lsp --prefix="$CI_INSTALL_DIR"
)
18 changes: 0 additions & 18 deletions dev/ci/ci-serapi.sh

This file was deleted.

0 comments on commit e11de61

Please sign in to comment.