#; Support for ACL2 Community Books
#; Copyright (C) 2020, Regents of the University of Texas
#; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.

#; Written by:  Matt Kaufmann               and J Strother Moore
#; email:       Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu
#; Department of Computer Sciences
#; University of Texas at Austin
#; Austin, TX 78712-1188 U.S.A.

#; Adapted from makefiles for IHS and data-structures library, which were
#; created by Bishop Brock.

#; NOTE:  Target "all" causes a recursive invocation of make with ACL2 set to
#; its current value.  These recursive invocations of make thus have ACL2 set
#; on the command line, which overrides any values of ACL2 set in those files.
#; This should not cause any problems unless you try to do something fancy; see
#; the comment for example just above target .exercises.cert in
#; books/case-studies/ivy/ivy-v2/ivy-sources/Makefile from the ACL2
#; distribution.

# Success can be determined by checking for the absence of the following string
# in the log;  "**CERTIFICATION FAILED**".

# We could probably arrange for the make process to stop as soon as
# certification fails, if there is a need.  If we do that, we should also
# arrange that the -k (or --keep_going) flag, as specified by the GNU make
# manual, avoids such stopping.

#################### Editable variables ####################

# The default command below prints runtime statistics for the certification.
# We normally inhibit most output during certification to speed up the proofs.
# Edit as necessary.

# Check that this version of MAKE defines MAKEFILE_LIST
ifdef MAKEFILE_LIST

# Determine the location of this Makefile-generic.  NOTE: We have
# tried $(realpath $(dir ...)) and similarly for abspath, but they
# have returned the empty string, presumably an error.  Also determine
# a default for ACL2, which can be overridden by setting a variable on
# the command line or in the environment.  Note that for cygwin, we
# need to do something special to get a Unix-like pathname.
ifneq (,$(findstring CYGWIN, $(shell uname)))
BOOKS_DIR := $(shell cd $(dir $(word $(words $(MAKEFILE_LIST)),$(MAKEFILE_LIST))) ; cygpath -m `pwd`)
ACL2 ?= $(shell cd $(BOOKS_DIR)/.. ; cygpath -m `pwd`)/saved_acl2
else
BOOKS_DIR := $(shell cd $(dir $(word $(words $(MAKEFILE_LIST)),$(MAKEFILE_LIST))) ; pwd)
ACL2 ?= $(shell cd $(BOOKS_DIR)/.. ; pwd)/saved_acl2
endif

# Unless otherwise specified, use the books under this directory as
# the system books.  We set the flag ACL2_SYSTEM_BOOKS_DYNAMIC if any
# Makefile-generic sets ACL2_SYSTEM_BOOKS, so that recursive calls of
# make using Makefile-generic will re-set ACL2_SYSTEM_BOOKS.
# (With the more naive approach through Version_3.6.1, we had a
# failure with arithmetic-3 and top-level target
# chk-include-book-worlds (for "make" invoked in the directory above
# books/), apparently because Makefile-generic is invoked recursively
# on the subdirectories and we were using :dir ;system in our
# testing.)
ifndef ACL2_SYSTEM_BOOKS
	export ACL2_SYSTEM_BOOKS_DYNAMIC := true
endif
ifdef ACL2_SYSTEM_BOOKS_DYNAMIC
	export ACL2_SYSTEM_BOOKS := $(BOOKS_DIR)
endif
# Otherwise, specify ACL2= and ACL2_SYSTEM_BOOKS= oneself.

# End the ifdef of MAKEFILE_LIST.
endif

ACL2_BOOKS_MAKEFILE ?= Makefile

# Set the following variable to a non-empty string if you want debug information.
ACL2_BOOKS_DEBUG ?=

# Avoid loading customization file unless environment variable is already set.
export ACL2_CUSTOMIZATION ?= NONE

# Fix problem with sh on some Linux systems:
ifeq ($(OSTYPE),linux)
	SHELL = bash
endif
ifeq ($(OSTYPE),linux-gnu)
	SHELL = bash
endif

# Inhibit all output except the summary (which can be useful for tracking down problems).
# Set this to "" if you do want the output.

INHIBIT ?= (set-inhibit-output-lst (list (quote prove) (quote proof-tree) (quote warning) (quote observation) (quote event) (quote history))) (set-debugger-enable :bt)

# Support for make dependencies:  should be a list of book names without
# the .lisp suffix.  Can be overridden on the command line or in a file
# that includes this file.

BOOKS ?= $(patsubst %.lisp, %, $(wildcard *.lisp))

ACL2_COMPILE_FLG ?= :default

# Set the following variable to T in order to use provisional
# certification towards the certification of books.
# export ACL2_PCERT

export ACL2_PCERT_ARG ?=
export ACL2_OUTFILE_SUFFIX  ?=

# Define the following variable as shown in the following example, in
# order to arrange that books be provisionally certified using
# certify-book with :pcert keyword argument of t, to build .pcert1
# file when .pcert0 file is built:
export ACL2_BOOKS_PCERT_ARG_T ?=
# ACL2_BOOKS_PCERT_ARG_T = book1 book2

#################### END of editable variables ####################

# We should really check that following is not empty.  It is the same as
# books, but with .cert suffixes.  This variable should not be overridden;
# it is computed as needed from BOOKS.  Note the use of '=' rather than ':=',
# so that BOOKS can be redefined after including this file in another makefile
# and the variables below will automatically be updated accordingly.

BOOKS_CERT    = $(patsubst %, %.cert,    $(BOOKS))

# As above with BOOKS_CERT, we use '=' for all of the following so
# that BOOKS_COMP can be redefined locally in the local Makefile, by
# setting BOOKS_SKIP_COMP in that local Makefile.  For example, by placing
# BOOKS_SKIP_COMP := foo bar
# after the include of Makefile-generic, one arranges that books foo
# and bar will NOT be compiled in other Lisps.

# Keep the following compiled file extensions in sync with those
# mentioned in the 'clean' target in ../GNUmakefile.
BOOKS_SKIP_COMP :=
BOOKS_COMP    = $(filter-out $(BOOKS_SKIP_COMP),$(BOOKS))
BOOKS_FASL    = $(patsubst %, %.fasl,    $(BOOKS_COMP))
BOOKS_FAS     = $(patsubst %, %.fas,     $(BOOKS_COMP))
BOOKS_SPARCF  = $(patsubst %, %.sparcf,  $(BOOKS_COMP))
BOOKS_UFSL    = $(patsubst %, %.ufsl,    $(BOOKS_COMP))
BOOKS_64UFASL = $(patsubst %, %.64ufasl, $(BOOKS_COMP))
BOOKS_UFASL   = $(patsubst %, %.ufasl,   $(BOOKS_COMP))
BOOKS_DFSL    = $(patsubst %, %.dfsl,    $(BOOKS_COMP))
BOOKS_D64FSL  = $(patsubst %, %.d64fsl,  $(BOOKS_COMP))
BOOKS_DX64FSL = $(patsubst %, %.dx64fsl, $(BOOKS_COMP))
BOOKS_LX64FSL = $(patsubst %, %.lx64fsl, $(BOOKS_COMP))
BOOKS_LX32FSL = $(patsubst %, %.lx32fsl, $(BOOKS_COMP))
BOOKS_SSE2F   = $(patsubst %, %.sse2f,   $(BOOKS_COMP))
BOOKS_X86F    = $(patsubst %, %.x86f,    $(BOOKS_COMP))
BOOKS_O       = $(patsubst %, %.o,       $(BOOKS_COMP))

BOOKS_LISP    = $(patsubst %, %.lisp,    $(BOOKS))
BOOKS_BKCHK_OUT = $(patsubst %, %.bkchk.out, $(BOOKS))

#  This rule certifies every book in BOOKS.  If the dependencies are set up
#  correctly then the order of the books in BOOKS won't matter.

.PHONY: all all_pcert

all:
	@if [ -n "$(ACL2_BOOKS_DEBUG)" ] ;\
	then \
		echo "[Makefile-generic]: Preparing to make 'all'" ;\
		if [ "$$ACL2_PCERT" != "" ] ;\
		then \
			echo "[Makefile-generic]: NOTE: Using provisional certification." ;\
		fi \
	fi
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) \
	  $(BOOKS_CERT) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

all_pcert: ACL2_PCERT = t

all_pcert:
	$(MAKE) all -f $(ACL2_BOOKS_MAKEFILE)

#  This rule tells how to get <book>.cert from <book>.lisp, either by running
#  ACL2 on the <book>.acl2 file (if it exists) or using the default command
#  to certify at ground zero.  Note that some Lisps execute (LP) upon startup
#  and some do not, and some (e.g., OpenMCL) might not even start in the ACL2
#  package, which can cause a problem if .acl2 files in our regressions suite
#  execute (LP) instead of (ACL2::LP).  We deal with these issues below.

%.cert:   WORKXXX = workxxx
%.pcert0: WORKXXX = workxxx_pcert0
%.pcert1: WORKXXX = workxxx_pcert1
%.acl2x:  WORKXXX = workxxx_acl2x

%.cert:   ACL2_OUTFILE_SUFFIX =
%.pcert0: ACL2_OUTFILE_SUFFIX = .pcert0
%.pcert1: ACL2_OUTFILE_SUFFIX = .pcert1
%.acl2x:  ACL2_OUTFILE_SUFFIX = .acl2x

%.pcert0: ACL2_PCERT_ARG = CREATE
# Override:
$(patsubst %, %.pcert0, $(ACL2_BOOKS_PCERT_ARG_T)): ACL2_PCERT_ARG = T
%.pcert1: ACL2_PCERT_ARG = CONVERT
ifneq ($(ACL2_PCERT),)
%.cert:   ACL2_PCERT_ARG = COMPLETE
else
%.cert:   ACL2_PCERT_ARG =
endif
%.acl2x:  ACL2_PCERT_ARG =

define cert_cmd
	echo "Making `pwd`/$@ on `date`"
	rm -f $@
	echo '(acl2::value :q)' > $(WORKXXX).$(*F)
	echo '(in-package "ACL2")' >> $(WORKXXX).$(*F)
	echo '(lp)' >> $(WORKXXX).$(*F)
	if [ "$$ACL2_OUTFILE_SUFFIX" = ".acl2x" ] ; \
	then \
	  echo "(set-write-acl2x t state)" >> workxxx_acl2x.$(*F) ; \
	fi
	echo '$(INHIBIT)' >> $(WORKXXX).$(*F)
	if [ -f $*.acl2 ] ; \
	then \
	  cat $*.acl2 >> $(WORKXXX).$(*F) ; \
	elif [ -f cert.acl2 ] ; \
	then \
	  cat cert.acl2 >> $(WORKXXX).$(*F) ; \
	  echo "" >> $(WORKXXX).$(*F) ; \
	  echo '(certify-book "$*" ? $(ACL2_COMPILE_FLG))' >> $(WORKXXX).$(*F) ; \
	else \
	  echo "" >> $(WORKXXX).$(*F) ; \
	  echo '(certify-book! "$*" 0 $(ACL2_COMPILE_FLG))' >> $(WORKXXX).$(*F) ; \
	fi
	echo "" >> $(WORKXXX).$(*F)
	echo '(acl2::value :q)' >> $(WORKXXX).$(*F)
	echo '(acl2::exit-lisp)' >> $(WORKXXX).$(*F)
	if [ -n "$(ACL2_BOOKS_DEBUG)" ] ;\
	then \
	  echo "[Makefile-generic]: certify book commands (from $(WORKXXX).$(*F)):" ;\
	  echo "" ;\
	  cat $(WORKXXX).$(*F) ;\
	  echo "" ;\
	fi
	($(ACL2) < $(WORKXXX).$(*F) 2>&1) > $*$(ACL2_OUTFILE_SUFFIX).out
	((test -f $<) && (ls -al $@)) || \
	     (echo "" ;\
		   tail -300 $*$(ACL2_OUTFILE_SUFFIX).out | sed 's/^/   | /' ;\
		   echo "" ;\
		   echo "" ;\
		   echo "**CERTIFICATION FAILED** for" `pwd`/$@ "(see $*$(ACL2_OUTFILE_SUFFIX).out)" ;\
		   exit 1)
	rm -f $(WORKXXX).$(*F)
endef

# It is important for the .cert targets to depend on the .pcert1
# targets, so that the .pcert1 targets are triggered as soon as
# possible.  We considered instead making .pcert1 files early in the
# commands for the .cert targets, but then the .pcert1 file cannot be
# made until all subsidiary .cert targets are complete, which defeats
# the point of parallel making of .pcert1 files supported by
# provisional certification.  On the other hand, since the Complete
# procedure of provisional certification moves a .pcert1 file to the
# corresponding .cert file, the .cert target could be considered out
# of date on any subsequent make!  So we declare all .pcert1 files to
# be INTERMEDIATE, so that their absence does not trigger remaking of
# .cert files.
PCERT1 = $(patsubst %.lisp, %.pcert1, $(wildcard *.lisp))
.INTERMEDIATE: $(PCERT1)

# We also make the .pcert0 files INTERMEDIATE, to handle the following
# circumstance.  Suppose we certify a set of books using ordinary
# certification, and then we remake using provisional certification.
# Then we would like to avoid recertifying books with valid .cert
# files such that all their sub-books also have valid .cert files.
# However, unlike the .pcert1 files (which are moved to .cert files,
# and hence are eliminated by ACL2), we make the .pcert0 files
# PRECIOUS; this way, they are still around if we subsequently need to
# recertify only some of the books, still using provisional
# certification.
PCERT0 = $(patsubst %.lisp, %.pcert0, $(wildcard *.lisp))
.INTERMEDIATE: $(PCERT0)
.PRECIOUS: $(PCERT0)

ifneq ($(ACL2_PCERT),)
# Warning: Before thinking about removing dependency below on
# %.pcert1, see the comment above where the .pcert1 files are declared
# to be INTERMEDIATE.
%.cert: %.lisp %.pcert1
	@echo "Making (by moving .pcert1 file) `pwd`/$@ on `date`"
	@echo '(certify-book "$*" ?)' > $(WORKXXX).$(*F)
	@($(ACL2) < $(WORKXXX).$(*F) 2>&1) > $*$(ACL2_OUTFILE_SUFFIX).out
	@(ls -al $@) || \
	     (echo "" ;\
		   tail -300 $*$(ACL2_OUTFILE_SUFFIX).out | sed 's/^/   | /' ;\
		   echo "" ;\
		   echo "" ;\
		   echo "CERTIFICATION FAILED for `pwd`/$@ (see $*$(ACL2_OUTFILE_SUFFIX).out)" ;\
		   exit 1)
else
%.cert: %.lisp
	@$(cert_cmd)
endif

%.pcert0: %.lisp
	@$(cert_cmd)

# See override just below.
%.pcert1: %.pcert0
	@$(cert_cmd)

# Override for %.pcert1 when using :pcert t to build .pcert0 and
# .pcert1 files together (handy use of a static pattern rule):
$(patsubst %, %.pcert1, $(ACL2_BOOKS_PCERT_ARG_T)): %.pcert1: %.pcert0
	@echo "Note: Skipping build of $@ (normally built with $*.pcert0)."

%.acl2x: %.lisp
	@$(cert_cmd)

# The following rules are useful when books have been certified in one lisp,
# but we would also like their compiled files to exist in the other lisp.

.PHONY: fasl
fasl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_FASL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.fasl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.fasl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: fas
fas:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_FAS) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

# For CLISP, apparently only the first echoed form is evaluated.  So do not give multiple forms.
%.fas: %.cert
	@echo "Making $$PWD/$@"
	echo '(ld `((include-book "$(patsubst %.fas,%,$(@))" :load-compiled-file :comp :ttags :all)))' | $(ACL2)

.PHONY: sparcf
sparcf:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_SPARCF) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.sparcf: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.sparcf,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: ufsl
ufsl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_UFSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.ufsl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.ufsl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: 64ufasl
64ufasl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_64UFASL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.64ufasl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.64ufasl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: ufasl
ufasl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_UFASL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.ufasl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.ufasl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: x86f
x86f:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_X86F) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.x86f: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.x86f,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: dfsl
dfsl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_DFSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.dfsl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.dfsl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: d64fsl
d64fsl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_D64FSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.d64fsl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.d64fsl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: dx64fsl
dx64fsl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_DX64FSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.dx64fsl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.dx64fsl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: o
o:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_O) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.o: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.o,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: lx64fsl
lx64fsl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_LX64FSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.lx64fsl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.lx64fsl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: lx32fsl
lx32fsl:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_LX32FSL) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.lx32fsl: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.lx32fsl,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: sse2f
sse2f:
	@echo 'Using ACL2=$(ACL2)'
	$(MAKE) -s -f $(ACL2_BOOKS_MAKEFILE) $(BOOKS_SSE2F) INHIBIT='$(INHIBIT)' ACL2='$(ACL2)'

%.sse2f: %.cert
	@echo "Making $$PWD/$@"
	echo '(acl2::value :q) (acl2::lp) (ld `((include-book "$(patsubst %.sse2f,%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2)

.PHONY: nothing
nothing:
	@echo "There\'s a good reason to do this here."

# The dependencies rule prints make dependency commands to the screen.  The basic
# strategy is to look for include-book commands, and to prefix appropriately
# "$(ACL2_SYSTEM_BOOKS)" when :dir :system is specified.  Thus, if :dir :system is
# specified then a common Makefile header in a books directory could be as
# follows (just strip off the leading "# " on each line).

# ----------------------------------------------------------------------
# # The following variable should represent the ACL2 source directory.
# # It is the only variable in this Makefile that may need to be edited.
# ACL2_SRC = ../../../../../..

# ACL2_SYSTEM_BOOKS = $(ACL2_SRC)/books
# include $(ACL2_SYSTEM_BOOKS)/Makefile-generic
# ACL2 = $(ACL2_SRC)/saved_acl2
# ----------------------------------------------------------------------

# Here are variables that represent egrep commands for finding include-book
# forms, as well as sed commands for modifying those include-book forms to
# generate dependency lines.

# Grep commands to rule out :dir :system:
ACL2_NON_DIR            = egrep -i -v ':dir'

# Grep commands for include-book and ld forms withOUT :dir
# (keep in sync with next set of grep commands):
ACL2_EGREP_CMD          = egrep -i '^[^;]*include-book[ 	]*\".*\"' $$book.lisp | $(ACL2_NON_DIR)
ACL2_EGREP_CMD_ACL2     = $(subst $$book.lisp,$$book.acl2,$(ACL2_EGREP_CMD))
ACL2_EGREP_CMD_CERT     = $(subst $$book.lisp,cert.acl2,$(ACL2_EGREP_CMD))
ACL2_EGREP_CMD_ACL2_LD  = egrep -i '^[^;]*\(ld[ 	]*\".*\"' $$book.acl2 | $(ACL2_NON_DIR)
ACL2_EGREP_CMD_CERT_LD  = egrep -i '^[^;]*\(ld[ 	]*\".*\"' cert.acl2 | $(ACL2_NON_DIR)

# Grep commands for include-book and ld forms withOUT :dir and withOUT
# "/" (since "/" suggests another directory)
# (keep in sync with preceding set of grep commands):
ACL2_NON_SLASH           = egrep -i -v '/'
ACL2X_EGREP_CMD          = egrep -i '^[^;]*include-book[ 	]*\".*\"' $$book.lisp | $(ACL2_NON_DIR) | $(ACL2_NON_SLASH)
ACL2X_EGREP_CMD_ACL2     = $(subst $$book.lisp,$$book.acl2,$(ACL2X_EGREP_CMD))
ACL2X_EGREP_CMD_CERT     = $(subst $$book.lisp,cert.acl2,$(ACL2X_EGREP_CMD))
ACL2X_EGREP_CMD_ACL2_LD  = egrep -i '^[^;]*\(ld[ 	]*\".*\"' $$book.acl2 | $(ACL2_NON_DIR) | $(ACL2_NON_SLASH)
ACL2X_EGREP_CMD_CERT_LD  = egrep -i '^[^;]*\(ld[ 	]*\".*\"' cert.acl2 | $(ACL2_NON_DIR) | $(ACL2_NON_SLASH)

# Grep commands for include-book and ld forms WITH :dir :system (need a file argument):
ACL2_EGREP_CMD_DIR      = egrep -i '^[^;]*include-book[ 	]*\".*\"[ 	]*:dir[ 	]*:system'
ACL2_EGREP_CMD_DIR_LD   = egrep -i '^[^;]*\(ld[ 	]*\".*\"[ 	]*:dir[ 	]*:system'

# Sed commands for transforming above egrep results into a dependency line:
ACL2_SED_CMD            = sed "s/[^\"]*\"/$$book.$$cert_or_acl2x: /" | sed 's/".*/.cert/'
ACL2_SED_CMD_PCERT0     = sed "s/[^\"]*\"/$$book.pcert0: /" | sed 's/".*/.pcert0/'
ACL2_SED_CMD_LD         = sed "s/[^\"]*\"/$$book.$$cert_or_acl2x: /" | sed 's/".*//'
ACL2_SED_CMD_DIR        = $(subst book.$$cert_or_acl2x: ,book.$$cert_or_acl2x: $$\(ACL2_SYSTEM_BOOKS)\/,$(ACL2_SED_CMD))
ACL2_SED_CMD_DIR_LD     = $(subst book.$$cert_or_acl2x: ,book.$$cert_or_acl2x: $$\(ACL2_SYSTEM_BOOKS)\/,$(ACL2_SED_CMD_LD))

# To comment out a line:
ACL2_SED_CMD_COMMENT    = sed "s/^/\# /"

# See comments above.
.PHONY: dependencies
dependencies:
	@for book in $(BOOKS) ; \
	do \
	echo "" ; \
	if [ -f $$book.acl2 ] && [ -n "`egrep -i '^[^;]*\(certify-book[^;]*:acl2x t' $$book.acl2`" ]; then \
	  echo $$book.cert: $$book.acl2x ; \
	  cert_or_acl2x=acl2x ; \
	else \
	  cert_or_acl2x=cert ; \
	fi ; \
	$(ACL2_EGREP_CMD) | $(ACL2_SED_CMD) ;\
	$(ACL2_EGREP_CMD_DIR) $$book.lisp | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	if [ -f $$book.acl2 ]; then \
	echo "$$book.$$cert_or_acl2x: $$book.acl2" ; \
	$(ACL2_EGREP_CMD_ACL2) | $(ACL2_SED_CMD) ;\
	$(ACL2_EGREP_CMD_ACL2_LD) | $(ACL2_SED_CMD_LD) ;\
	$(ACL2_EGREP_CMD_DIR) $$book.acl2 | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	$(ACL2_EGREP_CMD_DIR_LD) $$book.acl2 | $(ACL2_SED_CMD_DIR_LD) | $(ACL2_SED_CMD_COMMENT) ;\
	elif [ -f cert.acl2 ]; then \
	echo "$$book.$$cert_or_acl2x: cert.acl2" ; \
	$(ACL2_EGREP_CMD_CERT) | $(ACL2_SED_CMD) ;\
	$(ACL2_EGREP_CMD_CERT_LD) | $(ACL2_SED_CMD_LD) ;\
	$(ACL2_EGREP_CMD_DIR) cert.acl2 | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	$(ACL2_EGREP_CMD_DIR_LD) cert.acl2 | $(ACL2_SED_CMD_DIR_LD) | $(ACL2_SED_CMD_COMMENT) ;\
	fi ; \
	done
	@echo ''
	@echo '# DEPENDENCIES SUPPORTING PROVISIONAL CERTIFICATION:'
	@for book in $(BOOKS) ; \
	do \
	echo "" ;\
	if [ -f $$book.acl2 ] && [ -n "`egrep -i '^[^;]*\(certify-book[^;]*:acl2x t' $$book.acl2`" ]; then \
	  echo $$book.pcert0: $$book.acl2x ; \
	else \
	  cert_or_acl2x=pcert0 ; \
	  $(ACL2_EGREP_CMD) | $(ACL2_SED_CMD_PCERT0) ;\
	  $(ACL2_EGREP_CMD_DIR) $$book.lisp | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	  if [ -f $$book.acl2 ]; then \
	  echo "$$book.$$cert_or_acl2x: $$book.acl2" ; \
	  $(ACL2_EGREP_CMD_ACL2) | $(ACL2_SED_CMD_PCERT0) ;\
	  $(ACL2_EGREP_CMD_ACL2_LD) | $(ACL2_SED_CMD_LD) ;\
	  $(ACL2_EGREP_CMD_DIR) $$book.acl2 | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	  $(ACL2_EGREP_CMD_DIR_LD) $$book.acl2 | $(ACL2_SED_CMD_DIR_LD) | $(ACL2_SED_CMD_COMMENT) ;\
	  elif [ -f cert.acl2 ]; then \
	  echo "$$book.$$cert_or_acl2x: cert.acl2" ; \
	  $(ACL2_EGREP_CMD_CERT) | $(ACL2_SED_CMD_PCERT0) ;\
	  $(ACL2_EGREP_CMD_CERT_LD) | $(ACL2_SED_CMD_LD) ;\
	  $(ACL2_EGREP_CMD_DIR) cert.acl2 | $(ACL2_SED_CMD_DIR) | $(ACL2_SED_CMD_COMMENT) ;\
	  $(ACL2_EGREP_CMD_DIR_LD) cert.acl2 | $(ACL2_SED_CMD_DIR_LD) | $(ACL2_SED_CMD_COMMENT) ;\
	  fi ; \
	fi ;\
	done

.PHONY: clean
clean:
	rm -f workxxx* *@expansion.lsp *.out *.date *.*cert *.*cert.time *.pcert0 *.pcert1 *cert*.temp \
	*.acl2x *.port Makefile-deps *.h *.c *.o *.sbin *.lbin *.fasl *.ufsl \
	*.64ufasl *.ufasl *.pfsl *.dfsl *.dx32fsl *.lx32fsl *.d64fsl \
	*.dx64fsl *.lx64fsl *.bin *.sparcf *.axpf *.x86f *.ppcf *.fas \
	*.lib *.sse2f *.log TMP*.* temp-emacs-file.lsp

ifdef FAST_DEPS_FOR_CLEAN
# Note that Makefile-deps will be deleted by the clean target
# immediately after the following code creates it.
Makefile-deps:
	@echo "# Skipping deps" > Makefile-deps
else
# The argument --no-print-directory below avoids lines like:
# make[3]: Leaving directory `/v/filer4b/v11q001/acl2/devel/v3-5-alpha-aug31/books/bdd'
Makefile-deps: $(BOOKS_LISP) $(wildcard *.acl2)
	@echo "Updating dependencies in `pwd`"
	@rm -f Makefile-deps
	@echo "# This file is automatically generated; do not hand edit." > Makefile-deps
	+@make --no-print-directory -s dependencies >> Makefile-deps
endif

# The following targets are primarily for developers to be able to
# check well-formedness of the ACL2 world after including each book.
# Note that the two problematic directories for world-checking,
# hacking/ and workshops/2007/dillinger-et-al/code/ override the
# chk-include-book-worlds target by setting environment variable
# ACL2_SKIP_CHK_INCLUDE_BOOK_WORLDS in order to skip this check.  The
# problem seems likely to be that in many of the books in these two
# directories, the first bad triple is a GLOBAL-VALUE for either the
# unknown property EXTEND-PROGN! or RETRACT-PROGN!, or else is an
# unbinding of the PREDEFINED property for PROGN! (indicating a use of
# :REDEF); presumably these books mess with raw mode.

.PHONY: chk-include-book-worlds
chk-include-book-worlds:
	if [ -z "$(ACL2_SKIP_CHK_INCLUDE_BOOK_WORLDS)" ]; then \
	echo "Using ACL2=$(ACL2)" ; \
	(rm -f *.bkchk.out > /dev/null) ; \
	$(MAKE) -s $(BOOKS_BKCHK_OUT) ACL2='$(ACL2)' ; \
	fi

%.bkchk.out: %.cert
	@echo "Including `pwd`/$* on `date`"
	@echo '(acl2::value :q)' > workxxx.bkchk.$(*F)
	@echo '(in-package "ACL2")' >> workxxx.bkchk.$(*F)
	@echo '(acl2::lp)' >> workxxx.bkchk.$(*F)
	@echo '(acl2::in-package "ACL2")' >> workxxx.bkchk.$(*F)
	@echo '(include-book "$*")' >> workxxx.bkchk.$(*F)
	@echo '(include-book "system/pseudo-good-worldp" :dir :system)' >> workxxx.bkchk.$(*F)
	@echo "Checking world created by including `pwd`/$* on `date`"
	@echo '(chk-pseudo-good-worldp "$*")' >> workxxx.bkchk.$(*F)
	@($(ACL2) < workxxx.bkchk.$(*F) 2>&1) > $*.bkchk.out
	@(fgrep 'Pseudo-good-worldp check for including "$*" passed.' $@) || \
            (echo '** Pseudo-good-worldp check FAILED for including $*;' "see `pwd`/$@" '**' ;\
             exit 1)
	@rm -f workxxx.bkchk.$(*F)