Re: [isabelle-dev] CakeML compiler in the AFP

[Gerwin.Klein]

> 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, 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] CakeML compiler in the AFP

[Makarius]

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 https://isabelle.sketis.net/cygwin_2018 -- only the latter causes
>> some odd problems in the first attempt ("./cake.exe: cannot execute
>> binary file: Exec format error"); it might disappear after some more
>> tinkering. In the worst case, such an optional tool is not available for
>> Windows users.
> 
> Ramana has informed me that the .S file makes some assumptions about
> Unix-y behaviour. So it's not surprising to at least one person. Michael
> Norrish reported that it works on WSL.

WSL still does not quite work with Isabelle2017, Isabelle2018: oddly it
is the Z3 component that causes problems. It will hopefully work at some
point in the near future.

For now it merely means that this component is really optional, and does
not work with Windows.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

> 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 https://isabelle.sketis.net/cygwin_2018 -- only the latter causes
> some odd problems in the first attempt ("./cake.exe: cannot execute
> binary file: Exec format error"); it might disappear after some more
> tinkering. In the worst case, such an optional tool is not available for
> Windows users.

Ramana has informed me that the .S file makes some assumptions about
Unix-y behaviour. So it's not surprising to at least one person. Michael
Norrish reported that it works on WSL.

> Providing the already compiled binaries via some component also avoids
> the still open problem of Isabelle sessions that write to the
> file-system as a side-effect: recall that we are in the process to
> eliminate that an turn it into managed "exports" instead, but that does
> not quite fit with executables.

Combined with the other arguments, there seems to be no good reason to
not have it as a component. I'll try to get this done.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] CakeML compiler in the AFP

[Makarius]

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 code [0]. Hence, it
> requires a C compilation toolchain including "make" [1].
> 
> I see two ways forward:
> 
> 1) It becomes a component.
>a) ... in Isabelle (optional)
>b) ... in the AFP (optional?)
> 
> 2) The compressed artifact (~ 2 MB with xz) is committed to the AFP and
> compiled on-the-fly.

What is the meaning for "optional?" for AFP?

It should be clear that committing big blobs to a Source Code Management
system is conceptually wrong. It was common practice for SVN, but that
is long past. For Isabelle we have an established concept of
"components" for artifacts that are somehow non-source (e.g.
hol-light-bundle-0.5-126) and often platform-specific.

So if something needs to be compiled for a particular platform, the
component provides the result for all possible platforms for our
high-end users (see also Isabelle/Admin/PLATFORMS), which are not
expected to have low-level development tools around (make, cc, ...).

I've briefly tried cake-x64-64 on Linux, Mac OS X 10.10, and Cygwin 64
from https://isabelle.sketis.net/cygwin_2018 -- only the latter causes
some odd problems in the first attempt ("./cake.exe: cannot execute
binary file: Exec format error"); it might disappear after some more
tinkering. In the worst case, such an optional tool is not available for
Windows users.

Providing the already compiled binaries via some component also avoids
the still open problem of Isabelle sessions that write to the
file-system as a side-effect: recall that we are in the process to
eliminate that an turn it into managed "exports" instead, but that does
not quite fit with executables.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

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 that this is not yet the full compilation toolchain from
Isabelle/HOL to CakeML! It's just the tiny backend part where a CakeML
AST can be compiled by the official CakeML compiler.

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 code [0]. Hence, it
requires a C compilation toolchain including "make" [1].

I see two ways forward:

1) It becomes a component.
   a) ... in Isabelle (optional)
   b) ... in the AFP (optional?)

2) The compressed artifact (~ 2 MB with xz) is committed to the AFP and
compiled on-the-fly.

I don't have a strong opinion either way. Thoughts?

Cheers
Lars


[0] The original download can be found here:


[1] Luckily the "Makefile" is so simple that I am attaching it below in
full:

cake: cake.o basis_ffi.o

clean:
rm -f cake.o basis_ffi.o cake

.PHONY: clean

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev