[Agda] Bundlling Agda with agda-writer

[Nils Anders Danielsson]

On 2015-09-08 10:50, Andrej Bauer wrote:
> As far as I can tell the license allows us to do that (I see Marko has
> not put a license on agda-writer, but I imagine it's going to be an
> open-source one).

Note that Agda's license only covers the Agda source code, not the
libraries that Agda depend on (transitively). If you distribute a
binary, then you should presumably respect the license of every
component. I haven't checked every individual license, but I think most
or all of them put mild requirements on you. Examples from the Agda
license (MIT + BSD3):

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

   "Redistributions in binary form must reproduce the above copyright
   notice, this list of conditions and the following disclaimer in the
   documentation and/or other materials provided with the distribution."

> My question is technical: what needs to be bundled, and will there be
> problems with Agda assuming that it can find things in certain
> folders?

I don't know how agda-writer communicates with Agda. If it uses
agda --interaction, then it needs to find the agda binary. The binary,
in turn, looks for files (lib/prim/Agda/Primitive.agda, Agda.css, etc.)
in a certain directory that can be configured by setting the
Agda_datadir environment variable.

-- 
/NAD