fiat
fiat copied to clipboard
mit-plv
Fail to make querystructures on Coq > 8.9
I clone the repo and follow the instruction "make querystructures" to build the SQL-like library, but it fail, the error message is below
COQC src/QueryStructure/Specification/SearchTerms/ListInclusion.v
Warning: The -require option is deprecated, please use -require-import
instead. [deprecated-boot,deprecated]
File "./src/QueryStructure/Specification/SearchTerms/ListInclusion.v", line 49, characters 2-140:
Error: Unsolved obligations remaining.
Makefile.coq:677: recipe for target 'src/QueryStructure/Specification/SearchTerms/ListInclusion.vo' failed
make: *** [src/QueryStructure/Specification/SearchTerms/ListInclusion.vo] Error 1
my system is Ubuntu 16.04, my "coqc -v" output is
The Coq Proof Assistant, version 8.11.0 (March 2020)
compiled on Mar 23 2020 4:55:38 with OCaml 4.07.1
According the the CI, the querystructures target hasn't been supported since Coq 8.5pl3. I'm still maintaining the parsers and fiat-core targets, but I'm not sure if anyone is maintaining the other targets. @cpitclaudel, can you say anything about the state of the rest of the repo?
