[Agda] Example Runnable Agda Programs

Philipp Hausmann p.hausmann at students.uu.nl
Tue Dec 16 10:50:57 CET 2014


Thanks everybody for the examples, this helps us a lot. When we have
some interesting results, I will let you know.

Philipp

On 12.12.2014 15:47, Philipp Hausmann wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda




More information about the Agda mailing list