Unit tests with Specdris and Travis CI Improvement.

[pheymann]

I applied Specdris to rewrite your unit tests:

Advantages

• nice dsl to create the tests and get formatted output
• exit code depends on test result; if some test case fails it is 1. So you don't need to analyse the text output anymore
• reduces code you had to write and maintain to build your tests
• you don't need the additional runtests.sh script anymore

Disadvantages

• you need Specdris as package (but I added a new make task dependencies which installs Specdris)

What do I mean with I improving the travis ci builds? The current YML uses os: mac which takes hours for vm provisioning. By using docker the whole build process is reduced to a minute or so.

Note: I didn't touch Testing.idr as it is part of the package and I wasn't sure if it used by lib users.

Disclaimer: I am the author of Specdris ;)

What do you think of these changes?

[pheymann]

Ha, failed my own PR test. Need to add Specdris to Travis :).

[jfdm]

Of interest, if you are concerned with the speed of a travis build, then there are alternate ways to test idris. For example, I use a nix based configuration.

[pheymann]

@jfdm but you also have to add a nix script to get it running which isn't necessary for a Docker build.

And the speed wasn't my main concern, but with os: mac you don't get a build (as far as my experience goes) at all, because it takes forever :).

[ziman]

Thank you for all this work!

I would prefer to have everything related to testing contained in this repository so that we don't have to depend on external things (such as a Docker container). Perhaps you could add a Dockerfile + a build script — or switch to the Nix way.

I like that the Docker container is not needed for non-Travis testing and I also like that you don't need Specdris for the ordinary build, you need it only for testing.

Alternatively, you could add commented-out code that shows how to run tests if the Docker container (or Specdris) becomes bitrotten/not available/etc. (Even if the alternative is slower.)

The bottom line is that I would like to reduce the inconvenience and blockage resulting from external resources becoming unavailable in the future, which happens often because people get too busy or for other reasons. (Been there myself on the busy end.)

[pheymann]

I would then switch to nix script and remove the Docker dependency.

[pheymann]

When I find the time to resolve these merge conflicts 😄 . But I think I will get this ready by tomorrow.

[pheymann]

I resolved merge conflicts with master and fixed LazyTest which produces in master:

nb-pheymann:lightyear paul.heymann$ make test
idris --build lightyear.ipkg
(cd tests; bash runtests.sh)
TIMOUTCMD set to gtimeout
compiling lightyear tests...
Type checking ./Json.idr
Type checking ./JsonTest.idr
Type checking ./Test.idr
Type checking ./TestLazy.idr
TestLazy.idr:24:1:(ty1 : Ty **
                   SExpr ty1)  cannot be a parameter of Prelude.Show.Show
(Implementation arguments must be type or data constructors)
* could not compile tests *
make: *** [test] Error 1

[pheymann]

@ziman I added nix-script travis build and removed docker dependency. When you have some time left could you have a look?

[ziman]

Thank you!

Sorry for coming up with this so late but there's one more thing -- LazyTest tests that laziness works. If it does not, the program will either take too long or segfault from stack overflow -- I don't remember which in this case.

That was also the point of the timeout command in the shell script. I understand that if a test segfaults, then the test program will exit with a non-zero exit value, which will be recognised as a test failure. Does Specdris support timeouts, too? Or would we rely on the timeouts in Travis?

[pheymann]

Currently it doesn't support timeouts. I'll add it to specdris but this will take a moment. I let you know when I'm done.