we can work those problems. We've worked lots harder ones. . Heck, we build, what, 5 different cross compilers now, including the riscv one

that's not even official? And our *own* C compiler? I think we're OK. Oh, wait, I forgot: we have the ACPI language too. If we can put

something that ugly in the tree, I think we have room for SPARK :-)

I think this could prove to be a very important new direction for coreboot, and I still think it belongs in the tree.

ron

On Fri, Aug 28, 2015 at 2:07 PM Carl-Daniel Hailfinger <c-d.hailfinger.devel.2006@gmx.net> wrote:

On 28.08.2015 18:29, ron minnich wrote:
> I would really like this to be in the tree. It gives us a chance to do
> things in coreboot that go beyond C and assembly. So that's my $.02.

Same here.
Besides that, SPARK gives us easier provability of code. That is
something governments and safety engineers care about, and it makes for
great marketing.

> What harm would it do?

Having it in the tree would be beneficial because it will be easier to
bisect than two separate trees.
The only thing I'm worried about is whether we can guarantee the
complete tree can be built on all of the platforms where it can be built
now, but that worry applies in the git submodule case as well.

Regards,
Carl-Daniel