1TMPFILE = /tmp/workxxx 2 3top: pkg-check.txt 4 5include ${ACL2_SYSTEM_BOOKS}/Makefile-generic 6# The following line shouldn't be necessary. 7ACL2 ?= acl2 8 9-include Makefile-deps 10 11pkg-check.txt: PKGS.lsp PKGS.sml 12 @echo '(include-book "../../lisp/pkg-alist-to-alist")' > $(TMPFILE) 13 @echo "(ld (quote (" >> $(TMPFILE) 14 @for book in $(BOOKS) ; \ 15 do \ 16 echo "(include-book \"$$book\")" >> $(TMPFILE) ; \ 17 echo '(chk-known-package-alist "PKGS.lsp" state)' >> $(TMPFILE) ; \ 18 echo '(u)' >> $(TMPFILE) ; \ 19 done 20 @echo "(note-chk-known-package-alist-success \"pkg-check.txt\" state)" >> $(TMPFILE) 21 @echo ")))" >> $(TMPFILE) 22 @$(ACL2) < $(TMPFILE) > pkg-check.out 2> pkg-check.err 23 @if [ ! -e pkg-check.txt ]; then \ 24 echo "FAILURE for pkg-check.txt" ; \ 25 exit 1 ; \ 26 fi 27 28PKGS.lsp PKGS.sml: all 29 echo '(include-book "../../lisp/pkg-alist-to-alist")' > $(TMPFILE) 30 echo '(include-book "pkg-test")' >> $(TMPFILE) 31 echo '(include-book "m1-story")' >> $(TMPFILE) 32 echo '(print-kpa "PKGS.lsp" "PKGS.sml")' >> $(TMPFILE) 33 $(ACL2) < $(TMPFILE) > PKGS.out 2> PKGS.err 34 35clean: clean-pkgs 36 37clean-pkgs: 38 rm -f pkg-check.* 39