-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #4 from coq-io/add-travis
Add Travis and opam file
- Loading branch information
Showing
2 changed files
with
77 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
dist: trusty | ||
sudo: required | ||
language: generic | ||
|
||
services: | ||
- docker | ||
|
||
env: | ||
global: | ||
- PACKAGE_NAME="coq-io-hello-world" | ||
matrix: | ||
- COQ_IMAGE="coqorg/coq:8.4" | ||
- COQ_IMAGE="coqorg/coq:8.5" SHOULD_SUPPORT="true" | ||
- COQ_IMAGE="coqorg/coq:8.6" SHOULD_SUPPORT="true" | ||
- COQ_IMAGE="coqorg/coq:8.7" SHOULD_SUPPORT="true" | ||
- COQ_IMAGE="coqorg/coq:8.8" SHOULD_SUPPORT="true" | ||
- COQ_IMAGE="coqorg/coq:8.9" SHOULD_SUPPORT="true" | ||
|
||
install: | | ||
# Prepare the COQ container | ||
docker pull ${COQ_IMAGE} | ||
docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/project -w /home/project ${COQ_IMAGE} | ||
docker exec COQ /bin/bash --login -c " | ||
# This bash script is double-quoted to interpolate Travis CI env vars: | ||
echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" | ||
export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' | ||
set -ex # -e = exit on failure; -x = trace for debug | ||
opam update | ||
opam pin add ${PACKAGE_NAME}.opam . --kind=path --no-action | ||
opam config list | ||
opam repo list | ||
opam pin list | ||
opam list | ||
" install | ||
script: | ||
- echo -e "${ANSI_YELLOW}Building...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r' | ||
- | | ||
docker exec COQ /bin/bash --login -c " | ||
export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' | ||
set -ex | ||
sudo chown -R coq:coq /home/project | ||
# Check if the package is compatible with the current environment | ||
if [ ${SHOULD_SUPPORT} ] || opam install ${PACKAGE_NAME} --show-action; then | ||
# First install the dependencies | ||
opam install ${PACKAGE_NAME} --deps-only -y | ||
opam list | ||
# Then install the package itself in verbose mode | ||
opam install ${PACKAGE_NAME} -v | ||
fi; | ||
" script | ||
- docker stop COQ # optional | ||
- echo -en 'travis_fold:end:script\\r' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
opam-version: "2.0" | ||
maintainer: "[email protected]" | ||
homepage: "https://github.com/clarus/coq-hello-world" | ||
dev-repo: "git+https://github.com/clarus/coq-hello-world.git" | ||
bug-reports: "https://github.com/clarus/coq-hello-world/issues" | ||
authors: ["Guillaume Claret"] | ||
license: "MIT" | ||
build: [ | ||
["./configure.sh"] | ||
[make "-j%{jobs}%"] | ||
[make "-C" "extraction"] | ||
] | ||
install: [ | ||
["install" "-T" "extraction/main.native" "%{bin}%/helloWorld"] | ||
] | ||
depends: [ | ||
"coq-io" {>= "4.0.0" build} | ||
"coq-io-system" {build} | ||
"coq-io-system-ocaml" {>= "2.3.0"} | ||
] | ||
tags: [ | ||
"keyword:effects" | ||
"keyword:extraction" | ||
] | ||
synopsis: "A Hello World program in Coq" |