[Agda] Example Runnable Agda Programs

Philipp Hausmann p.hausmann at students.uu.nl
Fri Dec 12 15:47:59 CET 2014


Hi,

I am looking for example programs to test the Agda compilers. Just by
searching github, google & co I couldn't find many Agda programs which
can actually be run and do something interesting.

To give a bit of context, we are working on a new backend for Agda and
would like to have some regression tests. We have some simple
HelloWorld-style programs. but we are missing some more complicated
examples. Currently we are porting the Eliza [1] example from GHC's
nofib testsuite, but adding already existing Agda programs would be much
less work....  Especially interesting would also be examples where the
current MAlonzo backend fails or produces bad code. I remember seeing
some emails about them on the mailing list [2, 3, 4], but I don't
remember seeing any actual code example for reproducing these errors.

As the behaviour of Agda programs should not really depend on the
backend, I think the test programs would be useful for the MAlonzo
backend as well.

Long story short, does anyone have actual runnable Agda programs we
could use for testing?

Cheers,
Philipp

[1]
https://github.com/phile314/agda/blob/compiler-tests/test/exec/with-stdlib/Eliza.agda
[2] https://lists.chalmers.se/pipermail/agda/2012/004423.html
[3] https://lists.chalmers.se/pipermail/agda/2013/005229.html
[4] https://lists.chalmers.se/pipermail/agda/2014/006990.html


More information about the Agda mailing list