[isabelle-dev] CakeML compiler in the AFP

Gerwin.Klein at data61.csiro.au Gerwin.Klein at data61.csiro.au
Fri Sep 21 00:10:30 CEST 2018


> On 20.09.2018, at 22:19, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> What is the meaning for "optional?" for AFP?
> 
> We don't have any established process for additional components in the
> AFP. The question is, should this go into "$AFP_BASE/etc/components" or not?

I don’t think this should go into the AFP, it’s too far away from what the AFP is supposed to achieve.

Distributing it as a component together with Isabelle would work, though, I think. 

Cheers,
Gerwin



More information about the isabelle-dev mailing list