# EDIT THE FOLLOWING by replacing the directory with your ACL2 distributed
# books directory.  You are welcome to omit this line, or not as you prefer, in
# your contribution.

include /Users/freekver/Library/acl2/v3-6/acl2-sources/books/Makefile-generic

GeNoC-misc.cert: GeNoC-misc.lisp
GeNoC-misc.cert: GeNoC-types.cert
# GeNoC-misc.cert: $(ACL2_SYSTEM_BOOKS)/make-event/defspec.cert

GeNoC-types.cert: GeNoC-types.lisp
# GeNoC-types.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defuns.cert
# GeNoC-types.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defthms.cert

algorithm.cert: algorithm.lisp
algorithm.cert: definitions.cert

correctness.cert: correctness.lisp
correctness.cert: invariants3.cert

definitions.cert: definitions.lisp
definitions.cert: GeNoC-misc.cert
# definitions.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/lexicographic-ordering.cert
# definitions.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defuns.cert
# definitions.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defthms.cert

invariants.cert: invariants.lisp
invariants.cert: algorithm.cert
invariants.cert: GeNoC-misc.cert

invariants2.cert: invariants2.lisp
invariants2.cert: invariants.cert
invariants2.cert: perm.cert

invariants3.cert: invariants3.lisp
invariants3.cert: invariants2.cert

perm.cert: perm.lisp
# perm.cert: $(ACL2_SYSTEM_BOOKS)/meta/term-defuns.cert
