Set up Travis to automatically check pull requests for us about unimath HOT 9 CLOSED

Sounds like a good idea to me.

On Sun Nov 23 2014 at 1:10:51 AM Benedikt Ahrens [email protected]
wrote:

If set up correctly, Travis checks that pull requests do indeed compile,
so that reviewing can focus on other aspects.

Some setup information is here:
http://docs.travis-ci.com/user/getting-started/
and looking at how it is done in HoTT
https://github.com/HoTT/HoTT
might also be useful.

—
Reply to this email directly or view it on GitHub
#52.

from unimath.

To me too.

On Nov 23, 2014, at 3:07 PM, Daniel R. Grayson [email protected] wrote:

Sounds like a good idea to me.

On Sun Nov 23 2014 at 1:10:51 AM Benedikt Ahrens [email protected]
wrote:

If set up correctly, Travis checks that pull requests do indeed compile,
so that reviewing can focus on other aspects.

Some setup information is here:
http://docs.travis-ci.com/user/getting-started/
and looking at how it is done in HoTT
https://github.com/HoTT/HoTT
might also be useful.

—
Reply to this email directly or view it on GitHub
#52.

—
Reply to this email directly or view it on GitHub #52 (comment).

from unimath.

One needs to have admin status for the repository in question in order to set Travis up for it, which I do not have.
Dan, could you please do the setup, or give me superpowers?

from unimath.

@DanGrayson : I have just tried it on my fork of UniMath, and it is dead simple: one just needs to follow the first three steps of
http://docs.travis-ci.com/user/getting-started/
where the first two only involve clicking buttons in the browser.
The third step is committing a file ".travis.yml" to the root of the repository, for which a suitable content is

language: ocaml

before_install:
  - sudo apt-get update -qq
  - sudo apt-get install -y ocaml ocaml-nox ocaml-native-compilers camlp4-extra 

script: make && make

The double "make" is to work around that bug mentioned in the README.
We can see later if we want fancy functionality like the HoTT crowd.
A Travis run on my fork took a little less than half an hour.

from unimath.

I have made you and Vladimir into members of the "Owners Team", which
means you can do everything I can do.

On Sun Nov 23 2014 at 12:48:35 PM Benedikt Ahrens [email protected]
wrote:

One needs to have admin status for the repository in question in order to
set Travis up for it, which I do not have.
Dan, could you please do the setup, or give me superpowers?

—
Reply to this email directly or view it on GitHub
#52 (comment).

from unimath.

Ok, I have sent a pull request with a basic travis file.
One can do a lot of customisation for notifications about success and failure of the build test, for one's own PRs and for others', and so on. Details are given here:
http://docs.travis-ci.com/user/notifications/
The default is described by there as follows: "By default, a build email is sent to the committer and the author, but only if they have access to the repository the commit was pushed to."
Let me know what messages you would like to receive by email, or modify the file .travis.yml accordingly.
Of course, on the Github site, there is always an indicator showing the build status.

from unimath.

I guess the way travis works is by giving us free rein of a pristine virtual debian server.

from unimath.

On 11/24/2014 02:38 PM, Daniel R. Grayson wrote:

I guess the way travis works is by giving us free rein of a pristine virtual debian server.

The machines are running Ubuntu 12.04, I read somewhere.

from unimath.

We could find out what they're running by adding
cat /etc/issue
to the script. That might be interesting.

from unimath.