include ../Makefile-generic

# Dependencies:

bash.cert: bash.lisp

beta-reduce.cert: beta-reduce.lisp

book-thms.cert: book-thms.lisp

computed-hint-rewrite.cert: computed-hint-rewrite.lisp

computed-hint.cert: computed-hint.lisp

csort.cert: csort.lisp

definline.cert: definline.lisp
definline.cert: definline.acl2

defmac.cert: defmac.lisp

defopener.cert: defopener.lisp
defopener.cert: bash.cert

defp.cert: defp.lisp
defp.cert: defpun.cert

defpun.cert: defpun.lisp

dft-ex.cert: dft-ex.lisp
dft-ex.cert: dft.cert
# dft-ex.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/top-with-meta.cert
# dft-ex.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/top-with-meta.cert
dft-ex.cert: dft-ex.acl2

dft.cert: dft.lisp

dump-events.cert: dump-events.lisp

expander.cert: expander.lisp

fibonacci.cert: fibonacci.lisp
fibonacci.cert: int-division.cert
fibonacci.cert: grcd.cert

file-io.cert: file-io.lisp

find-lemmas.cert: find-lemmas.lisp

getprop.cert: getprop.lisp

goodstein.cert: goodstein.lisp
# goodstein.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/e0-ordinal.cert

grcd.cert: grcd.lisp
grcd.cert: int-division.cert
# grcd.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/e0-ordinal.cert

hanoi.cert: hanoi.lisp
hanoi.cert: hanoi.acl2

hons-help.cert: hons-help.lisp

hons-help2.cert: hons-help2.lisp
hons-help2.cert: hons-help.cert

hons-tests.cert: hons-tests.lisp
hons-tests.cert: qi.cert

how-to-prove-thms.cert: how-to-prove-thms.lisp

int-division.cert: int-division.lisp
# int-division.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/equalities.cert
# int-division.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/inequalities.cert

integer-type-set-test.cert: integer-type-set-test.lisp

meta-lemmas.cert: meta-lemmas.lisp

mult.cert: mult.lisp
# mult.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/top-with-meta.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/ihs/ihs-definitions.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/ihs/ihs-lemmas.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/structures.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/array1.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/ihs/@logops.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defuns.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defthms.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/deflist.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/defalist.cert
# mult.cert: $(ACL2_SYSTEM_BOOKS)/misc/meta-lemmas.cert

oprof.cert: oprof.lisp
oprof.cert: oprof.acl2

priorities.cert: priorities.lisp

problem13.cert: problem13.lisp
# problem13.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/equalities.cert
# problem13.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/inequalities.cert
# problem13.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/e0-ordinal.cert

process-book-readme.cert: process-book-readme.lisp

qi-correct.cert: qi-correct.lisp
qi-correct.cert: qi.cert

qi.cert: qi.lisp
qi.cert: hons-help2.cert

radix.cert: radix.lisp
# radix.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-2/meta/top.cert
# radix.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-2/floor-mod/floor-mod.cert
radix.cert: radix.acl2

random.cert: random.lisp
# random.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-2/floor-mod/floor-mod.cert

records.cert: records.lisp
records.cert: total-order.cert

records0.cert: records0.lisp
records0.cert: total-order.cert

rtl-untranslate.cert: rtl-untranslate.lisp
rtl-untranslate.cert: symbol-btree.cert

simplify-defuns.cert: simplify-defuns.lisp
simplify-defuns.cert: file-io.cert

sin-cos.cert: sin-cos.lisp

sort-symbols.cert: sort-symbols.lisp

sticky-disable.cert: sticky-disable.lisp

symbol-btree.cert: symbol-btree.lisp
# symbol-btree.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/floor-mod/floor-mod.cert

total-order.cert: total-order.lisp

transfinite.cert: transfinite.lisp

untranslate-patterns.cert: untranslate-patterns.lisp
untranslate-patterns.cert: symbol-btree.cert
# untranslate-patterns.cert: $(ACL2_SYSTEM_BOOKS)/misc/untranslate-patterns.cert

wet.cert: wet.lisp