<div dir="ltr">we can work those problems. We've worked lots harder ones. . Heck, we build, what, 5 different cross compilers now, including the riscv one <div>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</div><div>something that ugly in the tree, I think we have room for SPARK :-)</div><div><br></div><div>I think this could prove to be a very important new direction for coreboot, and I still think it belongs in the tree.</div><div><br></div><div>ron</div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Aug 28, 2015 at 2:07 PM Carl-Daniel Hailfinger <<a href="mailto:c-d.hailfinger.devel.2006@gmx.net">c-d.hailfinger.devel.2006@gmx.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 28.08.2015 18:29, ron minnich wrote:<br>
> I would really like this to be in the tree. It gives us a chance to do<br>
> things in coreboot that go beyond C and assembly. So that's my $.02.<br>
<br>
Same here.<br>
Besides that, SPARK gives us easier provability of code. That is<br>
something governments and safety engineers care about, and it makes for<br>
great marketing.<br>
<br>
> What harm would it do?<br>
<br>
Having it in the tree would be beneficial because it will be easier to<br>
bisect than two separate trees.<br>
The only thing I'm worried about is whether we can guarantee the<br>
complete tree can be built on all of the platforms where it can be built<br>
now, but that worry applies in the git submodule case as well.<br>
<br>
Regards,<br>
Carl-Daniel<br>
</blockquote></div>