[isabelle-dev] CakeML compiler in the AFP

[Makarius]

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