search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
442 stars 93 forks source link

Running `coqc sublist.v` yields the error message `Error: export attribute not supported here` #618

Closed eleehiga closed 2 years ago

eleehiga commented 2 years ago

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?

eleehiga commented 2 years ago

Actually turns out I had to comment out the #[export] from lines

QinshiWang commented 2 years ago

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.

eleehiga commented 2 years ago

@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].

QinshiWang commented 2 years ago

Yes. As you may have found, VST has dropped support for Coq 8.13.2 https://github.com/PrincetonUniversity/VST/blob/master/Makefile#L24

eleehiga commented 2 years ago

@QinshiWang Ah ok I understand thank you and you guys should update that Verifiable C pdf accordingly

eleehiga commented 2 years ago

@QinshiWang I was wondering on the Verifiable C pdf what does it mean by the Hint database?

mansky1 commented 2 years ago

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

mansky1 commented 2 years ago

@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).

eleehiga commented 2 years ago

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

eleehiga commented 2 years ago

@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