search

mit-plv / fiat

Mostly Automated Synthesis of Correct-by-Construction Programs
http://plv.csail.mit.edu/fiat/
Other
146 stars 31 forks source link

Fail to make querystructures on Coq > 8.9 #36

Open sqrta opened 4 years ago

sqrta commented 4 years ago

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
JasonGross commented 4 years ago

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?

cpitclaudel commented 4 years ago

I think we only support up to 8.9.