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 < [email protected]> 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 >
-- coreboot mailing list: [email protected] http://www.coreboot.org/mailman/listinfo/coreboot
