The system build has now been updated to automatically extract and prove any acl2 stanzas. This behavior is activated by including ACL2=acl2 on the make command line. This will, of course, only work if you have acl2 installed.
This automation will make sure the proofs occur at build time in order to catch failures. Currently, failing tests will not stop the build. The plan is to report failures after the build just as we do with the regression test suite. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
