~ubuntu-branches/ubuntu/wily/acl2/wily

(echo '(ld `((include-book "$(patsubst %.$(ACL2_COMP_EXT),%,$(@))" :load-compiled-file :comp :ttags :all))) (acl2::value :q) (acl2::exit-lisp)' | $(ACL2) >& $@.out) ; (ls -al $@ || (echo "**COMPILATION FAILED** for `pwd`/$@" ; exit 1)) ; fi

865

931

866

# Finally, we handle system/pcert/, which is a special case and thus

867

# would otherwise be ignored because of its cert_pl_exclude file. We

868

# use -j 1 because the old Makefile-generic, included by the

869

# directory's Makefile, doesn't establish dependencies between the

870

# compiled files, and this can cause an error when attempting to load

871

# another book's partially-built compiled file. Note that this rule

872

# overrides the pattern rule just above (a feature of GNU make).

873

system/pcert/sub.$(ACL2_COMP_EXT): \

874

system/deps-pcert.$(ACL2_COMP_EXT)

875

@echo "Making $@"

876

@cd system/pcert/ ; \

877

$(MAKE) -j 1 $(ACL2_COMP_EXT) ACL2_PCERT= >& make-$(ACL2_COMP_EXT).out ; \

878

(cd ../.. ; ls -al $(@D)/*.$(ACL2_COMP_EXT)) ; \

879

if [ `ls -1 *.$(ACL2_COMP_EXT) | wc -l` != `ls -1 *.cert | wc -l` ] ; then \

880

echo "**COMPILATION FAILED** for $(@D);" ; \

881

echo " search for '**' in `pwd`/make-$(ACL2_COMP_EXT).out to see failures." ; \

882

exit 1 ; \

883

884

885

932

OK_CERTS += system/pcert/sub.$(ACL2_COMP_EXT)

886

933

887

934

endif # ifdef ACL2_COMP

947

994

948

995

all: $(OK_CERTS)

949

996

950

# It was tempting to handle the `everything' target as follows:

951

# everything: USE_QUICKLISP = 1

952

# everything: all $(ADDED_BOOKS)

953

# But that didn't work, presumably because the value of OK_CERTS was

954

# on a first pass through the Makefile without USE_QUICKLISP being

955

# set.

997

# Starting 8/15/2014, everything does not automatically set USE_QUICKLISP=1,

998

# even in the HONS case. In particular, "make everything" no longer makes

999

# doc/manual/; for that, specify USE_QUICKLISP=1.

956

1000

.PHONY: everything

957

# Note: We add doc/top.cert explicitly, even though that might not

958

# be necessary, because at one point doc/top.cert was not

959

# otherwise made (something related to glucose).

960

1001

everything:

961

ifeq ($(ACL2_HAS_HONS), )

962

$(MAKE) all $(ADDED_BOOKS)

963

else

964

$(MAKE) all USE_QUICKLISP=1 $(ADDED_BOOKS) doc/top.cert

965

endif # ifeq ($(ACL2_HAS_HONS), )

1002

$(MAKE) all $(ADDED_BOOKS) $(ADDED_BOOK_TARGETS)

966

1003

967

1004

# The critical path report will work only if you have set up certificate timing

968

1005

# BEFORE you build the books. See ./critpath.pl --help for details.

977

1014

978

1015

# basic is the default set of books to build:

979

1016

.PHONY: basic

980

basic: arithmetic arithmetic-2 arithmetic-3 arithmetic-5 ihs std str xdoc tools misc data-structures

1017

basic: arithmetic arithmetic-3 arithmetic-5 ihs std xdoc tools misc data-structures

981

1018

1019

.PHONY: acl2s

1020

acl2s: $(filter acl2s/%, $(OK_CERTS))

982

1021

983

1022

.PHONY: add-ons

984

1023

add-ons: $(filter add-ons/%, $(OK_CERTS))

998

1037

.PHONY: bdd

999

1038

bdd: $(filter bdd/%, $(OK_CERTS))

1000

1039

1001

.PHONY: ccg

1002

ccg: $(filter ccg/%, $(OK_CERTS))

1003

1004

1040

.PHONY: centaur

1005

1041

centaur: $(filter centaur/%, $(OK_CERTS))

1006

1042

1007

.PHONY: cgen

1008

cgen: $(filter cgen/%, $(OK_CERTS))

1009

1010

1043

.PHONY: clause-processors

1011

1044

clause-processors: $(filter clause-processors/%, $(OK_CERTS))

1012

1045

1162

1195

MILAWA_DEPS := misc/untranslate-patterns.cert \

1163

1196

misc/hons-help2.cert \

1164

1197

misc/definline.cert \

1165

str/top.cert \

1198

std/strings/top.cert \

1166

1199

arithmetic-3/floor-mod/floor-mod.cert \

1167

1200

tools/include-raw.cert \

1168

1201

centaur/misc/seed-random.cert \

1213

1246

# unknown property EXTEND-PROGN! or RETRACT-PROGN!, or else is an

1214

1247

# unbinding of the PREDEFINED property for PROGN! (indicating a use of

1215

1248

# :REDEF); presumably these books mess with raw mode. Since we have

1216

# had such problems with ccg/ccg.lisp (presumably because it includes

1249

# had such problems with acl2s/ccg/ccg.lisp (presumably because it includes

1217

1250

# hacking/hacker), we exclude that book too.

1218

1251

1219

1252

BOOKS_BKCHK_OUT := $(patsubst %.cert,%.bkchk.out,$(OK_CERTS))

1220

1253

BOOKS_BKCHK_OUT := $(filter-out hacking/%, $(BOOKS_BKCHK_OUT))

1221

1254

BOOKS_BKCHK_OUT := $(filter-out workshops/2007/dillinger-et-al/code/%, $(BOOKS_BKCHK_OUT))

1222

BOOKS_BKCHK_OUT := $(filter-out ccg/ccg.bkchk.out, $(BOOKS_BKCHK_OUT))

1255

BOOKS_BKCHK_OUT := $(filter-out acl2s/ccg/ccg.bkchk.out, $(BOOKS_BKCHK_OUT))

1223

1256

1224

1257

.PHONY: chk-include-book-worlds

1225

1258

chk-include-book-worlds: $(BOOKS_BKCHK_OUT)

1371

1404

1372

1405

clean: clean_vl

1373

1406

1407

1408

1409

# Getopt Demo

1410

1411

centaur/getopt/demo2: centaur/getopt/demo2.cert

1412

@echo "Making getopt demo executable"

1413

@cd centaur/getopt; \

1414

ACL2_CUSTOMIZATION=NONE $(STARTJOB) -c "$(ACL2) < demo2-save.lsp &> demo2-save.out"

1415

@ls -l centaur/getopt/demo2

1416

1417

centaur/getopt/demo2-test.ok: centaur/getopt/demo2 \

1418

centaur/getopt/demo2-test.pl

1419

@echo "Testing getopt demo executable"

1420

@cd centaur/getopt; \

1421

$(STARTJOB) -c "./demo2-test.pl &> demo2-test.out"

1422

@cd centaur/getopt; cp demo2-test.out demo2-test.ok

1423

@ls -l centaur/getopt/demo2-test.ok

1424

1425

all: centaur/getopt/demo2-test.ok

1426

1427

1428

1374

1429

##############################

1375

1430

### Section: Tags

1376

1431

##############################

1493

1548

# default to simply (certify-book "foo" ? t)

1494

1549

# These instructions specify arguments to certify-book, for example:

1495

1550

# ; cert-flags: ? t :ttags :all

1496

# - In the following cases, books may be skipped in which case,

1497

# recursively, so are books that include such books, books that

1498

# include those parent books, and so on. In each case, the

1499

# indicated line may be placed either in the .lisp file or in the

1500

# .acl2 file that is consulted, as discussed above.

1501

# - Books that depend on ACL2(h), such as

1502

# centaur/tutorial/alu16-book.lisp, contain this line:

1503

# ; cert_param: (hons-only)

1504

# - Books that depend on ANSI Common Lisp, such as

1505

# oslib/*.lisp, contain this line (or in this case,

1506

# file cert.acl2 contains this line):

1507

# ; cert_param: (ansi-only)

1508

# - Books that require glucose (a SAT solver) contain this line:

1509

# ; cert_param: (uses-glucose)

1510

# - Books that require quicklisp contain this line:

1511

# ; cert_param: (uses-quicklisp)

1512

# - Two-pass certification is handled as follows, for example in

1513

# books/make-event/stobj-test.acl2 (as indicated above, this can

1514

# also go into the book instead of the relevant .acl2 file):

1515

# ; cert_param: (acl2x)

1551

# - See :DOC books-certification for documentation of the cert_param

1552

# comment, which can be used to restrict which books are to be

1553

# certified.

1516

1554

# - It's not clear that provisional certification is fully

1517

1555

# supported. For now, we implement it for two specific

1518

1556

# directories; search below for "provisional certification" to see

1539

1577

# cert-flags instead of certify-book commands. Alternately, maybe the scheme

1540

1578

# should be something like: if you give a certify-book command, we use it;

1541

1579

# otherwise we generate one using the cert-flags.

1580

Older »