[Agda] Releasing app with bundled Agda

[Nils Anders Danielsson]

On 2015-10-21 09:56, Marko Koležnik wrote:
> Anyway, since we bundled the Agda, we need to respect Licence Agda is
> using. So my questions are:
> 1.) Am I allowed to bundle Agda into Agda Writer?
> 2.) Am I allowed to have compiled agda in repository and/or in program
>     Resources when program is compiled?
> 3.) Is attribution in About enough? What should I put there?

If you check the main Agda license, it states that you can do lots of
things ("use, copy, modify, merge, publish, distribute", etc.), "subject
to the following conditions":

* "The above copyright notice and this permission notice shall be
   included in all copies or substantial portions of the Software."

* Some text in all caps.

The Agda source code also uses more licences (see the LICENSE file), and
Agda depends on other libraries, which come with their own licenses. I
suspect that all of these licenses are quite similar, so perhaps all you
need to do is to include a copy of each one in the program. However, I
haven't read all of the other licenses. If one or more dependencies is,
say, GPL'ed, then the situation is different.

-- 
/NAD