Document how to set up autocorres

[jyizheng]

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]

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]

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