robbertkrebbers / ch2o Goto Github PK

Thanks for a very interesting project!

I had trouble building ch2o under Ubuntu 18.04 with coqc 8.6.

What am I doing wrong? :-)

$ cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=18.04
DISTRIB_CODENAME=bionic
DISTRIB_DESCRIPTION="Ubuntu 18.04.2 LTS"
$ git clone https://github.com/robbertkrebbers/ch2o
$ cd ch2o
$ scons
scons: Reading SConscript files ...
scons: done reading SConscript files.
scons: Building targets ...
coqc -R . ch2o -q prelude/base.v
File "./prelude/base.v", line 499, characters 0-62:
Error: The "clear implicits" flag is incompatible with implicit annotations
scons: *** [prelude/base.vo] Error 1
scons: building terminated because of errors.
$ coqc --version
The Coq Proof Assistant, version 8.6 (October 2017)
compiled on Oct 28 2017 14:23:55 with OCaml 4.05.0

C18 adds (almost) no features, and consists only of folding in Technical Corrigenda (and otherwise resolving defect reports against C11).

As a result, it should hopefully not be too onerous to support, and may also help further inform some places where judgment was required in interpreting the C11 standard.

The sole change beyond resolving DRs (listed in the summary linked below) is that ATOMIC_VAR_INIT is deprecated and no longer mandatory when initializing atomic variables.

References:

• The last public draft
• The clarification request summary for C11, which lists the ones which made it in (marked "C17")
• A post that states an intent to go into more detail on some of the changes