Static-makefiles
How to use cert.pl within a larger Makefile that needs to know
how to build non-ACL2 files (e.g., C libraries) or dynamically generated ACL2
books.
For many ACL2 projects, cert.pl may allow you to entirely
avoid needing to write any Makefiles. But sometimes it's not enough. For
instance:
- If your project involves dynamically generating new ACL2 books,
cert.pl has no way to see their dependencies.
- If your project has a non-ACL2 component that needs to be built in some
special way, e.g., say you're linking ACL2 with a C library and you need to
recompile the library when you change its code, cert.pl has no support for
building the C library.
In these cases, the general approach is to write an ordinary Makefile,
but use cert.pl to automate the dependency scanning for all of the static
ACL2 books.
Basic Makefile Generation
Ordinarily, when you run a command like cert.pl foo, what happens
is:
- cert.pl scans foo for include-book commands, etc., to
figure out the dependencies of foo.
- It writes these dependencies into a temporary Makefile named
Makefile-tmp.
- It invokes make on Makefile-tmp to do the actual build.
When you use cert.pl as part of your own Makefile, you don't want it to
run make for you. Instead, you just want it to do the dependency analysis
and write out a Makefile that your Makefile can include.
This is done using the -s switch. For instance, here's how we could
create a Makefile for the arithmetic-5 library:
$ cd acl2/books/arithmetic-5
$ cert.pl top.cert -s Makefile-arith5
The resulting Makefile has all the dependencies for Arithmetic-5:
# This makefile was generated by running:
# cert.pl top.cert -s Makefile-arith5
...
ACL2_SYSTEM_BOOKS ?= .. # Boilerplate stuff
export ACL2_BIN_DIR := ../../cn/e/bin
include $(ACL2_SYSTEM_BOOKS)/build/make_cert
.PHONY: all-cert-pl-certs
# Depends on all certificate files.
all-cert-pl-certs:
CERT_PL_CERTS :=
lib/basic-ops/arithmetic-theory.cert
...
top.cert
all-cert-pl-certs: $(CERT_PL_CERTS)
...
lib/basic-ops/integerp-helper.cert : # Dependency info
support/top.cert
lib/basic-ops/building-blocks.cert
lib/basic-ops/default-hint.cert
lib/basic-ops/integerp-helper.lisp
...
The general idea is then to include the generated Makefile into your
own Makefile. For real examples of how to do this, see
- The books/Makefile; just search for cert.pl to see how it is used
to build Makefile-books.
- The similar use of cert.pl in books/projects/milawa/ACL2/Makefile,
which may in some ways be simpler to understand.
There are various options to control whether to emit the boilerplate
section, to rename variables like CERT_PL_CERTS, etc. See cert.pl
--help for a summary.
