Build failure under Ubuntu 18.04 with coqc 8.6

[practicalswift]

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

[rigille]

I'm also very interested! But I had trouble building under Ubuntu 19.04 and coqc 8.10.2

$ 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 8, characters 0-38:
Warning: There is no option Automatic Coercions Import.
[unknown-option,option]
File "./prelude/base.v", line 43, characters 0-29:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope C_scope.". [undeclared-scope,deprecated]
File "./prelude/base.v", line 54, characters 0-39:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./prelude/base.v", line 55, characters 0-42:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./prelude/base.v", line 83, characters 0-39:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./prelude/base.v", line 84, characters 0-48:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./prelude/base.v", line 199, characters 0-28:
Error:
Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on.

scons: *** [prelude/base.vo] Error 1
scons: building terminated because of errors.
$ coqc -v
The Coq Proof Assistant, version 8.10.2 (December 2019)
compiled on Dec 24 2019 16:31:24 with OCaml 4.06.1