> Just a side-remark: Fabian Immler has started with some experiments to
> use HOL4 with CakeML inside Isabelle. You should keep in contact with
> him about progress and possibilities.
Of course. I'm aware and we're emailing back and forth.
But this is to some extent orthogonal to Fabian's
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.
Just a side-remark: Fabian Immler has started with some experiments to
use HOL4 with CakeML inside Isabelle. You should keep in contact with
him about
> On 20.09.2018, at 22:19, Lars Hupel 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,
On 20/09/18 14:19, Lars Hupel wrote:
>
> 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've briefly tried cake-x64-64 on Linux, Mac OS X 10.10, and Cygwin 64
>> from
> 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've briefly tried cake-x64-64 on Linux, Mac OS X 10.10, and Cygwin 64
> from
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
On 20/09/18 11:02, Lars Hupel wrote:
>
> I would do so without writing this to the list, but there are some
> obstacles. The major obstacle being that the CakeML compiler is not in
> fact a piece of ML code, but a large assembly artifact (65 MB
> uncompressed) that needs to be linked to some FFI
Dear list,
I'm considering putting the entire CakeML compiler somewhere so that it
is accessible in the AFP. This includes a pretty-printer of (a small
subset of) the abstract syntax; together with some ML code that allows
one to invoke the compiler, not unlike "export_code ... checking".
Note
