[Agda] Makefile

[Samuel Gélineau]

On 2010-09-24 at 14:19, David Leduc wrote
> [...] coq_makefile is a shell command that takes as input names of Coq
> files and output a makefile that will take care of everything
> including their dependencies, their compilation and their
> documentation.
>
> Anything like that with Agda?

I wrote a simple ruby script which parses Agda import directives and
generates parts of a Makefile based on them. I didn't include it in
the public release of my library because I didn't want to have ruby as
a dependency, but the code is still there, in the online git archive.

http://github.com/agda/agda-finite-prover/tree/f73ad34119967c183f35e27f1bd4786775015e41


To use it, simply add some Agda files to the src folder and import
some of them from "src/Main.agda". Type "make", and the ruby script
will gather all of the dependencies, copy the relevant files to a
folder called "crumbs" (to separate the generated .agdai files from
source .agda files) and type-check them. The makefile assumes you have
installed the standard library at ~/lib/agda, but it should be easy to
change this folder for something else.

hope this helps,
– Samuel