[Agda] Releasing app with bundled Agda

[Marko Koležnik]

Thanks for noticing this. 

I’m kind of lost here. I should include other parts of Agda licence as well, right? How about compiled Agda? If I understand correctly from your response… Agda source code is licenced as stated in LICENCE (https://github.com/agda/agda/blob/master/LICENSE <https://github.com/agda/agda/blob/master/LICENSE>), but compiled file includes lots of other libraries? 

In conclusion: Is there reasonable way for me to include executable Agda at all?

Also, I’ve removed unnecessary files from source. Basically I only included Agda executable and Primitive.agda/Primitive.agdai. 

Can you please help me sort this thing out?

Thanks, Marko

> On 7. nov. 2015, at 12:39, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 
> On 2015-10-22 13:16, Nils Anders Danielsson wrote:
>> [...] perhaps all you need to do is to include a copy of each one in
>> the program.
> 
> I looked at your Licence.md. The statement "The file
> agda-writer/blob/master/Agda%20Writer/agda/agda is licenced as follows:
> [...]" is not correct. The Agda license only applies to parts of the
> Agda source code. A couple of Agda source files use different licenses.
> Furthermore, when you compile the program you include code from lots of
> other libraries.
> 
> -- 
> /NAD

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151107/de50d914/attachment.html