Running `coqc sublist.v` yields the error message `Error: export attribute not supported here`
Closed this issue · 10 comments
I ran coqc sublist.v (from here https://github.com/PrincetonUniversity/VST/blob/master/zlist/sublist.v) and that yielded the error message Error: export attribute not supported here. Was wondering if you guys could please help me solve this issue?
Actually turns out I had to comment out the #[export] from lines
Are you compiling with an old Coq version? I remember there were related issues. Old Coq versions don't support #[export] attribute for Hint Rewrite.
@QinshiWang I am running coq 8.13.2 like the Verifiable C pdf recommended. And ah ok I understand that I should update Coq probably in order to run #[export].
Yes. As you may have found, VST has dropped support for Coq 8.13.2
https://github.com/PrincetonUniversity/VST/blob/master/Makefile#L24
@QinshiWang Ah ok I understand thank you and you guys should update that Verifiable C pdf accordingly
@QinshiWang I was wondering on the Verifiable C pdf what does it mean by the Hint database?
Yes. As you may have found, VST has dropped support for Coq 8.13.2 https://github.com/PrincetonUniversity/VST/blob/master/Makefile#L24
More specifically, the issue here is that the repo version of VST is a bit ahead of the OPAM version of VST, and so the examples you've checked out are designed for VST 2.11 (which hasn't been released yet). You should expect small compatibility errors in this situation. As it happens, in this case Coq 8.15 will work for both VST 2.10 and VST 2.11, but it's always possible for a new version to include breaking changes. For 100% compatibility, you could check out the repo at the time of the 2.10 release instead: https://github.com/PrincetonUniversity/VST/tree/afb02be3fde53d23d9963ca6f1908b1b913b9a39
@QinshiWang I was wondering on the Verifiable C pdf what does it mean by the
Hint database?
https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#hint-databases
By the way, you may find that the VST-user mailing list (https://lists.cs.princeton.edu/mailman/listinfo/vst-user) is a better place to ask background and troubleshooting questions than the Issues page of the repo (which is for bugs in VST itself).
Yes. As you may have found, VST has dropped support for Coq 8.13.2 https://github.com/PrincetonUniversity/VST/blob/master/Makefile#L24
More specifically, the issue here is that the repo version of VST is a bit ahead of the OPAM version of VST, and so the examples you've checked out are designed for VST 2.11 (which hasn't been released yet). You should expect small compatibility errors in this situation. As it happens, in this case Coq 8.15 will work for both VST 2.10 and VST 2.11, but it's always possible for a new version to include breaking changes. For 100% compatibility, you could check out the repo at the time of the 2.10 release instead: https://github.com/PrincetonUniversity/VST/tree/afb02be3fde53d23d9963ca6f1908b1b913b9a39
Ah ok I understand and may check that out thank you
@QinshiWang I was wondering on the Verifiable C pdf what does it mean by the
Hint database?https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#hint-databases
By the way, you may find that the VST-user mailing list (https://lists.cs.princeton.edu/mailman/listinfo/vst-user) is a better place to ask background and troubleshooting questions than the Issues page of the repo (which is for bugs in VST itself).
Ah ok thank you I will definitely join that