[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Proving Axiom Correct
From: |
daly |
Subject: |
[Axiom-developer] Proving Axiom Correct |
Date: |
Wed, 15 Jul 2015 21:47:37 -0500 |
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