-
Notifications
You must be signed in to change notification settings - Fork 23
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 #1 from coq-community/add-ci-metadata
Add metadata and CI
- Loading branch information
Showing
14 changed files
with
309 additions
and
932 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 |
---|---|---|
@@ -1,4 +1,5 @@ | ||
Makefile.conf | ||
Makefile.coq | ||
Makefile.coq.conf | ||
execute_loops.ml | ||
execute_loops.mli | ||
insert-sort.ml | ||
|
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 @@ | ||
opam: &OPAM | ||
language: minimal | ||
sudo: required | ||
services: docker | ||
install: | | ||
# Prepare the COQ container | ||
docker pull ${COQ_IMAGE} | ||
docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} ${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 -y | ||
opam pin add ${CONTRIB_NAME} . -y -n -k path | ||
opam install ${CONTRIB_NAME} -y -j ${NJOBS} --deps-only | ||
opam config list | ||
opam repo list | ||
opam list | ||
" | ||
script: | ||
- echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${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/coq/${CONTRIB_NAME} | ||
opam install ${CONTRIB_NAME} -v -y -j ${NJOBS} | ||
" | ||
- docker stop COQ # optional | ||
- echo -en 'travis_fold:end:script\\r' | ||
|
||
nix: &NIX | ||
language: nix | ||
script: | ||
- nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI=" | ||
|
||
matrix: | ||
include: | ||
|
||
# Test supported versions of Coq via Nix | ||
- env: | ||
- COQ=8.9 | ||
<<: *NIX | ||
|
||
# Test supported versions of Coq via OPAM | ||
- env: | ||
- COQ_IMAGE=coqorg/coq:8.9 | ||
- CONTRIB_NAME=coq-coq-art | ||
- NJOBS=2 | ||
<<: *OPAM | ||
|
This file was deleted.
Oops, something went wrong.
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 @@ | ||
All of the Coq'Art examples and solutions of the exercises are available under the CeCILL-B license. |
Oops, something went wrong.