@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?
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?
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.
one could argue that you already have conf-g++
via Flocq, so it may be mostly for documentation purposes...
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 ;-)
Actually it is not only cosmetic, because for flocq it is a build dependency.
Last updated: Jun 03 2023 at 04:30 UTC