News for hackers. Stuff that matters.

A comment on CompCert – Formally-verified C compiler. Parent comment

Re:CompCert – Formally-verified C compiler by andi999 on Sunday June 27, 2021 @05:53AM (#27650115)
It is not a question if some files constitute a majority, since this is not majority vote based.

As far as I read your evaluation, probably it is gpl. But without the gpl linker exception you cannot create non gpl binaries.

[ Parent | on HN ]
Re:CompCert – Formally-verified C compiler by tyingq on Sunday June 27, 2021 @07:41AM (#27650749)
That is confusing. GCC specifically includes the "GCC runtime library exception" so that you can produce non-GPL binaries.
[ Parent | on HN ]
Re:CompCert – Formally-verified C compiler by andi999 on Sunday June 27, 2021 @08:55AM (#27651199)
Yes. Gcc does that and there is no problem, but the post is not about gcc (as far as I can tell from my tiny mobile screen)
[ Parent | on HN ]
Re:CompCert – Formally-verified C compiler by tyingq on Sunday June 27, 2021 @09:13AM (#27651313)
>but the post is not about gcc

Right. It's about a compiler with a GPL license but without a similar exception. I was making a comparison.

[ Parent | on HN ]
Re:CompCert – Formally-verified C compiler by dwheeler on Sunday June 27, 2021 @10:58AM (#27652082)
The CompCert compiler is not under the GPL or LGPL, it is under a proprietary license. Some parts may be released with other licenses, but that is different.
[ Parent | on HN ]
Re:CompCert – Formally-verified C compiler by tyingq on Sunday June 27, 2021 @11:29AM (#27652329)
That's not the point going down this thread. If part of it is GPL (and not LGPL), it makes it impossible to release compiled binaries made with it that are not GPL. It appears they attempted to switch to LGPL to fix that two months ago[1], but perhaps missed some parts.

[1] https://github.com/AbsInt/CompCert/commit/04f499c632a76e4605...

[ Parent | on HN ]