CompCert icon indicating copy to clipboard operation
CompCert copied to clipboard

Some dual-licensed code, such as PrintCsyntax, depends on NCL-only sources

Open shym opened this issue 5 years ago • 0 comments

Since PrintCsyntax is dual-licensed, I expected it could be used in a GPL project. But according to tools/modorder .depend.extr cfrontend/PrintCsyntax.cmx (using opam coq-compcert v3.8 package, in case it matters), it indirectly depends on some NCL-only source files. The problem comes (at least in part) from its dependency on cfrontend/C2C.ml which is dual-licensed but directly depends on NCL-only sources such as cfrontend/Initializers.v, driver/Configuration.ml, etc.

shym avatar Dec 17 '20 18:12 shym