Skip to content

Commit

Permalink
Merge PR #17848: Add waterproof to ci
Browse files Browse the repository at this point in the history
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
  • Loading branch information
coqbot-app[bot] and SkySkimmer committed Aug 1, 2023
2 parents 74e210c + aa4e664 commit 677b524
Show file tree
Hide file tree
Showing 4 changed files with 25 additions and 1 deletion.
3 changes: 3 additions & 0 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -959,3 +959,6 @@ plugin:ci-stalmarck:

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

plugin:ci-waterproof:
extends: .ci-template-flambda
3 changes: 2 additions & 1 deletion Makefile.ci
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,8 @@ CI_TARGETS= \
ci-unicoq \
ci-verdi_raft \
ci-vscoq \
ci-vst
ci-vst \
ci-waterproof

.PHONY: ci-all $(CI_TARGETS)

Expand Down
5 changes: 5 additions & 0 deletions dev/ci/ci-basic-overlay.sh
Original file line number Diff line number Diff line change
Expand Up @@ -399,3 +399,8 @@ project tactician "https://github.com/coq-tactician/coq-tactician" "coqdev"
# Ltac2 compiler
########################################################################
project ltac2_compiler "https://github.com/SkySkimmer/coq-ltac2-compiler" "main"

########################################################################
# Waterproof
########################################################################
project waterproof "https://github.com/impermeable/coq-waterproof" "coq-master"
15 changes: 15 additions & 0 deletions dev/ci/ci-waterproof.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#!/usr/bin/env/ bash

set -e

ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"

git_download waterproof

if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi

( cd "${CI_BUILD_DIR}/waterproof"
dune build -p coq-waterproof
dune install -p coq-waterproof --prefix=$CI_INSTALL_DIR
)

0 comments on commit 677b524

Please sign in to comment.