Karl Palmskog (Jan 20 2022 at 10:15): Karl Palmskog (Jan 20 2022 at 10:15):@Michael Soegtrop consider this issue: https://github.com/AbsInt/CompCert/issues/424
Doesn't this mean that CompCert packages should include the conf-gcc dependency? Obtaining and using ccomp is considered part of the coq-compcert package, right?
Michael Soegtrop (Jan 20 2022 at 10:45):Indeed, a good point. One should probably follow what @Xavier Leroy tests and request clang on macOS and gcc on the others.
@Xavier Leroy : what is your opinion on this?
Michael Soegtrop (Jan 20 2022 at 10:48):Btw.: I think it implicitly already requires gcc because it requires Flocq and flocq has ("conf-g++" {build} | "conf-clang" {build}) - afaik because it uses remake and compiles it from sources.
Karl Palmskog (Jan 20 2022 at 10:48):one could argue that you already have conf-g++ via Flocq, so it may be mostly for documentation purposes...
Karl Palmskog (Jan 20 2022 at 10:49):but somehow nice to have the following if both Clang and gcc are supported:
("conf-gcc" | "conf-clang")
Virtually touching your finger tip and making a wish for having the same thought at the same time ;-)
Michael Soegtrop (Jan 20 2022 at 10:50):Actually it is not only cosmetic, because for flocq it is a build dependency.
Last updated: Apr 19 2024 at 17:02 UTC