Merge pull request #5 from coq-io/add-travis

Add travis

.gitignore

@@ -1,4 +1,3 @@
-opam*
 .coqdeps.d
 Makefile
 Makefile.bak

.travis.yml

@@ -0,0 +1,48 @@
+dist: trusty
+sudo: required
+language: generic
+
+services:
+  - docker
+
+env:
+  global:
+  - OPAMJOBS="2"
+  matrix:
+  - COQ_IMAGE="coqorg/coq:8.5"
+  - COQ_IMAGE="coqorg/coq:8.6"
+  - COQ_IMAGE="coqorg/coq:8.7"
+  - COQ_IMAGE="coqorg/coq:8.8"
+  - COQ_IMAGE="coqorg/coq:8.9"
+
+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
+    if [ -n \"\${COMPILER_EDGE}\" ]; then opam switch \${COMPILER_EDGE}; eval \$(opam env); fi
+    opam update -y
+    opam pin add coq-io-system.opam . --kind=path -y --no-action
+    opam pin add coq-io-system-ocaml.opam . --kind=path -y --no-action
+    opam install coq-io-system --deps-only -y --ignore-constraints-on=coq-io-system-ocaml
+    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
+    opam install coq-io-system -v --ignore-constraints-on=coq-io-system-ocaml
+    " script
+- docker stop COQ  # optional
+- echo -en 'travis_fold:end:script\\r'

README.md

@@ -1,6 +1,8 @@
 # ![Logo](https://raw.githubusercontent.com/clarus/icons/master/megaphone-48.png) IO System
 > Library of Unix effects for Coq. See also [Coq.io](http://coq.io/).
 
+[![build status](https://img.shields.io/travis/coq-io/system.svg)](https://travis-ci.org/coq-io/system)
+
     Require Import Io.All.
     Require Import Io.System.All.
     Require Import ListString.All.

coq-io-system-ocaml.opam

@@ -0,0 +1,25 @@
+opam-version: "2.0"
+maintainer: "dev@clarus.me"
+homepage: "https://github.com/clarus/io-system"
+dev-repo: "git+https://github.com/clarus/io-system.git"
+bug-reports: "https://github.com/clarus/io-system/issues"
+authors: ["Guillaume Claret"]
+license: "MIT"
+build: [
+  [make "-C" "ocaml" "-j%{jobs}%"]
+]
+install: [
+  [make "-C" "ocaml" "install"]
+]
+depends: [
+  "lwt" {>= "2.4.7"}
+  "ocaml" {>= "4.00.0"}
+  "ocamlbuild"
+  "ocamlfind"
+  "num"
+]
+tags: [
+  "keyword:effects"
+  "keyword:extraction"
+]
+synopsis: "Extraction to OCaml of system effects"

coq-io-system.opam

@@ -0,0 +1,28 @@
+opam-version: "2.0"
+maintainer: "dev@clarus.me"
+homepage: "https://github.com/clarus/io-system"
+dev-repo: "git+https://github.com/clarus/io-system.git"
+bug-reports: "https://github.com/clarus/io-system/issues"
+authors: ["Guillaume Claret"]
+license: "MIT"
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "ocaml"
+  "coq" {>= "8.5"}
+  "coq-function-ninjas"
+  "coq-list-string" {>= "2.0.0"}
+  "coq-io" {>= "4.0.0"}
+  "coq-io-system-ocaml" {= "2.5.0"}
+]
+tags: [
+  "keyword:effects"
+  "keyword:extraction"
+  "logpath:Io/System"
+]
+synopsis: "System effects for Coq"

ocaml/Makefile

@@ -0,0 +1,11 @@
+default:
+	ocamlbuild ioSystem.cma ioSystem.cmxa -use-ocamlfind -package lwt,lwt.unix,num
+
+install: default
+	ocamlfind install io-system META _build/ioSystem.cmi _build/ioSystem.cmx _build/ioSystem.a _build/ioSystem.cma _build/ioSystem.cmxa _build/ioSystem.mllib
+
+uninstall:
+	ocamlfind remove io-system
+
+clean:
+	ocamlbuild -clean