Stream: Coq Platform devs & users

Topic: -compcert=o

view this post on Zulip Enrico Tassi (Jan 03 2021 at 17:05):

On branch v8.13 I have:

case "$COQ_PLATFORM_COMPCERT" in
  [fF]) PACKAGES="${PACKAGES} coq-compcert.3.8" ;;
  [oO]) echo "The open source variant of CompCert is notsupp orted in the beta"; exit 1 ;;
  [nN]) true ;;
  *) echo "Illegal value for COQ_PLATFORM_COMPCERT - aborting"; false ;;
esac

Is this easy to fix?

view this post on Zulip Michael Soegtrop (Jan 03 2021 at 18:58):

The makefile of Compcert doesn't support this, so one has to port the patch from 3.7 - not difficult but not zero work either.

Last updated: Jun 03 2023 at 05:01 UTC