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
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
-
Carl-Daniel Hailfinger -
ron minnich