search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Document how to set up autocorres #367

Open jyizheng opened 4 years ago

jyizheng commented 4 years ago

I am trying to code ext2 code under cogent/impl/fs/ext2/cogent by following the README. I got the error at the bottom. BTW, I have gone through the Adder example code. For it, I can generate the final executable successfully.

Is there any fix for this?

Cannot find $AC_DIR (/home/andy/cogent/autocorres) Cannot find $AC_DIR (/home/andy/cogent/autocorres) Cannot find $AC_DIR (/home/andy/cogent/autocorres) Cannot find $AC_DIR (/home/andy/cogent/autocorres) Cannot find $AC_DIR (/home/andy/cogent/autocorres) Cannot find $AC_DIR (/home/andy/cogent/autocorres) make: bash: Command not found Makefile:165: recipe for target '.c-gen' failed make: *** [.c-gen] Error 127

zilinc commented 4 years ago

You need to download autocorres from http://ts.data61.csiro.au/projects/TS/autocorres/ and set $AC_DIR to it. The README files (https://github.com/NICTA/cogent#proofs) and the documentation (https://cogent.readthedocs.io/en/latest/verification.html?highlight=AC_DIR#building-running-the-generated-files) are not super clear about it; I'll fix it. Thanks for the report. If you are only interested in building the kernel image, I don't think autocorres is needed. I'll test it---maybe the Makefile is unnecessarily requiring it. But you'll certainly need it for any C refinement proofs.

jyizheng commented 4 years ago

Thanks, I am able to compile ext2 now after I downloaded autocorres.