On 20/09/18 11:02, Lars Hupel wrote: > > I'm considering putting the entire CakeML compiler somewhere so that it > is accessible in the AFP. > > 1) It becomes a component. > a) ... in Isabelle (optional) > b) ... in the AFP (optional?)
BTW, anything that becomes part of the Isabelle repository is subject to its existing license in the "COPYRIGHT" file. CakeML also uses such a BSD-style license, but it names the authors explicitly. In Isabelle we only have "and contributors", and this is not subject to changes nor negotiations. All Isabelle contributors need to join the existing license. Of course, there might be more technical reasons to put the component either here or there. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev