Stream: Coq Platform devs & users

Topic: CompCert and gcc


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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")

view this post on Zulip Michael Soegtrop (Jan 20 2022 at 10:49):

Virtually touching your finger tip and making a wish for having the same thought at the same time ;-)

view this post on Zulip Michael Soegtrop (Jan 20 2022 at 10:50):

Actually it is not only cosmetic, because for flocq it is a build dependency.


Last updated: Jan 30 2023 at 11:03 UTC