[isabelle-dev] CakeML compiler in the AFP

Makarius makarius at sketis.net
Thu Sep 20 13:11:29 CEST 2018


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



More information about the isabelle-dev mailing list