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