acl2
Factor out tests from library build targets
From [email protected] on September 01, 2014 12:17:34
Some of the tests that people have written are fantastic. However, the "std" build target probably shouldn't include the tests for std.
Maybe this is just me being detail-oriented, and it wouldn't have enough value to us to actually do it, but, at least in terms of good software engineering, it would be good to tease out the various tests in our libraries and have separate "doc" and "doc-with-tests" targets.
I can imagine that in a world where I knew there was a build server making sure that the build was stable, that I wouldn't want to bother building doc-with-tests after updating my copy of ACL2.
Original issue: http://code.google.com/p/acl2-books/issues/detail?id=223
From [email protected] on September 01, 2014 10:17:49
Summary: Factor out tests from library build targets (was: Tease out tests from library build targets)
Status: New
From [email protected] on September 01, 2014 11:26:23
Do the tests take more than a trivial amount of time to run? If not, then it might be good not to exclude them, just to get an additional way to discover problems early.
From [email protected] on September 01, 2014 11:33:59
The thing that triggered this is that the new pretty-printing tests take a good amount of RAM (I think 3+ GB), and I'm back to running on smaller VMs.
It's really great that we have tests! But it occurred to me that some of the users (here I could name users for which we created the "basic" target) might not need to run them. I suspect this is only really the problem of UT/Oracle/Centaur if, as Matt points out, these tests end up on the critical path. And I don't think any test book is on the critical path, because nothing should include a testing book.
So, doing this refactoring ends up becoming charity work :/.
From [email protected] on September 02, 2014 06:55:17
Good point about memory (which I should have thought of when I mentioned "time").
I think it would probably be reasonable to change the "std" build target to depend on std/top.lisp instead of all of the books within std. Besides the string tests, this would exclude a few books such as std/strings/base64.lisp, which are unlikely to be widely useful.
On the other hand, it might be worth discussing what we regard as the minimum expected memory to be available for certifying normal books.
I think I generally regard as normal any book that uses less than 4 GB of memory. This is encoded into make_cert_help.pl, after a fashion: if the book doesn't include a set-max-mem line, we tell our cluster to reserve 4 GB for it. (Otherwise we reserve max-mem + 3GB for stacks and other padding.) I think we've successfully used this heuristic for a long time, and added set-max-mem commands to books that have run afoul of it.
Of course, in the brave new era of VMs and clouds, memory may not be as cheap and abundant as it has previously been, so maybe 4 GB is excessive.
It looks like the GNUMakefile contains many targets of the form
.PHONY: <something>
<something>: $(filter <something>/%, $(OK_CERTS))
besides std. So maybe this issue is broader than just Std.
Given that one can already do cert.pl [books]/std/top.lisp to certify the Std library without the tests, perhaps it's not such a bad thing for the std target to include also the tests. That is, we can regard the std target as certifying and testing Std. And the same for other targets.
As another direction, we could have separate targets std and std-with-tests, something like that.
