License status of file x86/Builtins1.v

[MSoegtropIMC]

I am currently testing a makefile PR to build only the open source/dual license part of CompCert, mostly for speed up of the VST CI (it runs into hard time restrictions with a full CompCert build), but also to avoid silently depending the open source package VST on the non open source package "full compcert". VST will work with both opam packages, but the idea is that the user has to install the non free part explicitly.

Doing so I came across the file x86/Builtins1.v which is required by the dual license file common/Builtins.v and recursively by quite a few more of the dual license files. As far as I can tell VST would not compile without this file.

Would you please revise the license status of x86/Builtins1.v or give advice what to do about this issue on the VST side?

[xavierleroy]

Thanks for the notice, we'll re-check the licensing of the various files in the coming days.

One word of caution, though: an "open source CompCert" package should be enough to build VST but may not be enough to use VST, because the clightgen tool is not open source.

[MSoegtropIMC]

we'll re-check the licensing of the various files in the coming days.

Perfect, thanks!

One word of caution, though: an "open source CompCert" package should be enough to build VST but may not be enough to use VST, because the clightgen tool is not open source.

My thought behind that is that the open source part is sufficient for teaching VST because then one uses clightgen generated files provided in the course. Since cligthgen is not e.g. AGPL my understanding is that the files clightgen produces share the copyright of the corresponding C-source and not of clightgen. VST includes quite a few such files which should be sufficient for a fairly deep exploration of VST. This makes it also easier to explore VST in industrial environments. I know that the license rules of clightgen allow commercial evaluation usage, but in an industrial environment usually either the license is trivially compliant to corporate open source usage rules or one has to consult the legal department - not that hard either but it might anyway keep a good fraction of potential users away from trying it, e.g. usually such a consultation takes some time. A fully open source installation which keeps interested users busy for a month should mostly solve this issue.

Also this separation makes it clear that clightgen is not part of the open source package. I think about also providing a clightgen only opam package to make this even more clear. It might also make sense to discuss with the opam maintainers to request explicit confirmation when non open source packages are installed (opam knows what the licenses are).

One more note: it would make sense to make it clear in the license that clightgen is not dual licensed. The selection of files is such that even experts might assume that it is exactly the set of files used by clightgen - especially because the set was increased a while back - see e.g. (PrincetonUniversity/VST#406 (comment))

[xavierleroy]

The issue with Builtins1.v should be fixed by commit b46c0c0 .

[MSoegtropIMC]

Perfect thanks! As you might have seen I added an open source build to my compcert opam PR (coq/opam#1246), mostly for the benefit of VST CI. May I ask which option you would prefer for handling this in the 3.7 "almost open source" package:

• include this commit as patch in the 3.7 compcert open source opam package - usually I wouldn't even think of patching a license file, but if you agree to it, it would make things quite bit easier and per your commit the file is dual licensed from today on (unless it changed since the 3.7 tag).

• rename the opam package from "open-source" to "reduced-build"

• use this commit as source for the open source build rather than the 3.7 tag

of cause any other option is also fine with me. Right now it is documented in the description of the package that one file is not open source, but the package variant name is "open-source".

[xavierleroy]

To me, the Builtins1.v files have always been dual-licensed, because their headers say so. It's just the top-level LICENSE file that was not up to date. So, commit b46c0c0 is not really a change of license, more like a clarification.

Among your three choices I would go with the simplest: "include this commit as patch in the 3.7 compcert open source opam package".

[MSoegtropIMC]

Thanks for the clarification! I will then provide this commit as patch to 3.7 in opam.