# Milawa OMakeroot # Copyright (C) 2005-2009 by Jared Davis # # This program is free software; you can redistribute it and/or modify it under # the terms of the GNU General Public License as published by the Free Software # Foundation; either version 2 of the License, or (at your option) any later # version. # # This program is distributed in the hope that it will be useful, but WITHOUT # ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS # FOR A PARTICULAR PURPOSE. See the GNU General Public License for more # details. # # You should have received a copy of the GNU General Public License along with # this program (see the file COPYING); if not, write to the Free Software # Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, # USA. open build/C DefineCommandVars() # We instruct omake not to print what it's about to execute, since that gets # pretty verbose and isn't typically relevant. We also tell it to keep going # after errors. OMakeFlags(-s -k) # These are the ANSI color codes for green, blue, black, red, and purple. If # you don't have an ANSI compatible terminal or don't want to see color in your # makefile, you can replace these with $(EMPTY) BLACK = $(shell printf "\033[0m") RED = $(shell printf "\033[31m") GREEN = $(shell printf "\033[32m") BLUE = $(shell printf "\033[34m") PURPLE = $(shell printf "\033[35m") BOLD_BLUE = $(shell printf "\033[34;1m") BOLD_PURPLE = $(shell printf "\033[35;1m") BOLD_RED = $(shell printf "\033[31;5;1m") align(str, len) = # Adds spaces to the end of str until its length is len and returns the # result. str = $(string $(str)) i = $(str.length) while $(lt $i, $(len)): str = $"$(str) " i = $(add $i, 1) return $(str) deps_if(string,deps) = # String should be a string and deps should be an array. We return deps if # string is non-empty, or an empty array otherwise. This is useful for # creating conditional dependency lines, e.g., # target: $(deps_if $(FOO), dep1.cert dep2.cert ...) # will cause the target to depend dep1.cert, ... only if $(FOO) is non-empty. if $(equal $(string), "") return $(array) return $(deps) locate_program(program) = # We try to find executable of the given name in the current $PATH. We # return the full path to the program on success, or the empty string # otherwise. locations = $(where $(program)) if $(equal $(length $(locations)), 0) println($(PURPLE)Note: $(program) not found$(BLACK)) return else ret = $(nth 0, $(locations)) println($(GREEN)Found $(align $(program), 10)$(BLACK) $(ret)) return $(ret) first_nonempty(stringlist) = # We return the first string in the list which is not empty, or the empty # string if all of the strings are empty i = 0 while $(lt $i, $(length $(stringlist))) case $(equal $(nth $i, $(stringlist)), "") i = $(add $i, 1) default return $(nth $i, $(stringlist)) return time(cmd) = # Execute cmd and return the amount of time it takes to complete, in seconds, # as an integer. start = $(gettimeofday) $(cmd) end = $(gettimeofday) return $(int $(sub $(end) $(start))) all_books() = # Returns an array which includes foo.cert for every foo.lisp found in the directory. lispfiles = $(glob *.lisp) if $(equal $(string $(lispfiles)), $"*.lisp") # The glob function bizarrely returns the string *.lisp instead of the empty # array when there are no files named *.lisp. We return the empty array in # this case. return else return $(replacesuffixes .lisp, .cert, $(lispfiles)) all_subdirs() = # Returns an array which includes all of the immediate subdirectories of the current # directory. The OMake subdirs function returns recursive subdirectories, making it # not very useful. The OMake glob function inanely returns * when there are no # subdirectories. dirs = $(glob D, *) if $(equal $(string $(dirs)), $"*") return else return $(set-diff $(dirs), autodoc proofs) all_pcerts() = # Returns an array which includes foo.pcert for every foo.lisp found in the directory. lispfiles = $(glob *.lisp) if $(equal $(string $(lispfiles)), $"*.lisp") # The glob function bizarrely returns the string *.lisp instead of the empty # array when there are no files named *.lisp. We return the empty array in # this case. return else return $(replacesuffixes .lisp, .pcert, $(lispfiles)) # We search for programs of the following names in your $(PATH). ACL2 = $(locate_program acl2) ACL = $(locate_program acl) CCL = $(locate_program ccl) SBCL = $(locate_program sbcl) SCL = $(locate_program scl) CMUCL = $(locate_program lisp) CLISP = $(locate_program clisp) #GCL_CLTL1 = $(locate_program gcl-cltl1) ADDJOB = $(locate_program addjob) # We have some helper scripts in the Build directory, written in Lisp. We'll # use the first one of these lisps to run these scripts. GENERIC_LISP = $(first_nonempty $(CCL) $(SBCL) $(CMUCL) $(CLISP) $(SCL) $(ACL)) # Dependency Scanning for ACL2 Books ------------------------------------------- # We scan for include-books and list all of those as dependencies. We ignore # all "ld" calls and we do not consider "portcullis" dependencies. DIRMAP = $(create-map $"SYSTEM", $"$(HOME)/Milawa/Support/acl2-3.4/books") DirLookup(key) = if $(DIRMAP.mem $"$(key)") return $(DIRMAP.find $"$(key)") else println(*** Fatal error) println(*** No DIRMAP entry for :dir $(key)) println(*** Perhaps you should add it to $(ROOT)/OMakeroot?) exit(1) ParseIncludeBookLine(line, ext) = match $(line) case $'[^;]*[(][Ii][Nn][Cc][Ll][Uu][Dd][Ee]-[Bb][Oo][Oo][Kk][ \t]*["]\([^"]*\)["].*:[Dd][Ii][Rr][ \t]*:\([^ \t)]*\)[ \t)].*' filename = $1 symbolic_dir = $2 resolved_dir = $(DirLookup $(uppercase $(symbolic_dir))) return $"$(resolved_dir)/$(filename).$(ext)" case $'[^;]*[(][Ii][Nn][Cc][Ll][Uu][Dd][Ee]-[Bb][Oo][Oo][Kk][ \t]*["]\([^"]*\)["].*' filename = $1 return $"$(filename).$(ext)" default println(ParseIncludeBookLine called on bad line: $(line)) CollectIncludeBookDeps(file, ext) = scan = '^[^;]*\([ \t]*include-book[ \t]*\".*\"' includes = $(shella egrep -i $(scan) $(file) || echo "") ret[] = foreach(line, $(includes)): ret[] += $(ParseIncludeBookLine $(line), $(ext)) export return $(ret) .SCANNER: %.cert: %.lisp section includes = $(CollectIncludeBookDeps $<, cert) foreach(i, $(includes)): println($"$@: $(i)") .SCANNER: %.mtime: %.lisp section includes = $(CollectIncludeBookDeps $<, mtime) foreach(i, $(includes)): println($@: $(i)) # You can further customize how output lines are displayed by changing these # functions. announce_job(file) = println($(GREEN)\($(file)\)$(BLACK)) rm($(file) -f) actually_check_file_exists(name) = # # This actually checks whether a file exists, and manages to avoid OMake's # caching mechanisms, so it can be used in a loop. # res = $(shell sh -c "test -e $(name) && echo 1 || echo 0") if $(equal $(res), 0) return 0 else return 1 slow_nfs_check_file_exists(name) = # # For slow NFS systems, we may not see that a file exists until some time # after it is written. This puts us into a waiting loop which gives the # file a chance to show up. # max_tries = 20 tries = $(max_tries) arg = $(name) while $(gt $(tries), 0) case $(equal 1, $(actually_check_file_exists $(arg))) if $(equal $(tries), $(max_tries)) return 1 else println(Successful NFS recovery for $(arg)) return 1 default println(Slow NFS? $(tries) tries left for $(arg)) tries = $(sub $(tries), 1) sleep 3 return 0 check_job(target,debug,time) = # check_job checks that the target has been created. If so, it prints out a # banner saying it is complete. Else, it prints the last 200 lines from the # debug file, with surrounding banner failures. if $(equal 1, $(slow_nfs_check_file_exists $(file $(target)))) println($(align $(BLUE)$(target), 60) $(PURPLE)$(time)s$(BLACK)) else println($(BOLD_RED)*** FAILED TO BUILD $(target) ***$(BLACK)$(RED)) tail -200 $(outfile) println($(BOLD_RED)*** FAILED TO BUILD $(target) ***$(BLACK)) write_file(filename,contents) = fd = $(fopen $(filename), w) fprintln($(fd), $(contents)) close($(fd)) shell(sync) shell(sleep 2) basic_job(target,program,instructions) = # We run $(program) < $(target).work > $(target).out # where $(target).work is a new file we create using the $(instructions) # as its contents. # We print out appropriate banners, etc. tempfile = $(addsuffix .work, $(target)) outfile = $(addsuffix .out, $(target)) announce_job($(target)) write_file($(tempfile), $(instructions)) if $(equal $(ADDJOB), $(EMPTY)) time = $(time $(program) < $(tempfile) >& $(outfile)) shell(sync) shell(sleep 2) check_job($(target), $(outfile), $(time)) else time = $(time $(ADDJOB) "$(program) < $(tempfile) >& $(outfile)") shell(sync) shell(sleep 2) check_job($(target), $(outfile), $(time)) #rm($(tempfile)) job_from_file(target,program,infile) = # We run $(program) < $(infile) > $(target).out outfile = $(addsuffix .out, $(target)) announce_job($(target)) if $(equal $(ADDJOB), $(EMPTY)) time = $(time $(program) < $(infile) >& $(outfile)) shell(sync) shell(sleep 2) check_job($(target), $(outfile), $(time)) else time = $(time $(ADDJOB) "$(program) < $(infile) >& $(outfile)") shell(sync) shell(sleep 2) check_job($(target), $(outfile), $(time)) CertifyBook(target,program) = basic_job($(target), $(program), $"" :ubt! 1 (ACL2::set-debugger-enable t) (ACL2::set-inhibit-output-lst '(ACL2::prove ACL2::proof-tree ACL2::warning ACL2::observation ACL2::event ACL2::expansion)) (ACL2::certify-book "$*" ACL2::? t :skip-proofs-okp t :defaxioms-okp t :ttags :all) (ACL2::good-bye) "") PCertifyBook(bookname, program) = basic_job($(bookname).pcert, $(program), $"" :ubt! 1 (ACL2::set-debugger-enable t) (ACL2::include-book "$(ROOT)/ACL2/acl2-hacks/pcert") (ACL2::defttag pcert-ttag) (ACL2::remove-untouchable ACL2::certify-book-info nil) (ACL2::provisionally-certify "$(bookname)") (ACL2::good-bye) "") ExtractBody(lispfile, features) = # We parse the lisp file and create the .body file for it bodyfile = $(addsuffixes .body, $(removesuffix $(lispfile))) rm($(bodyfile) -f) basic_job($(bodyfile), $(GENERIC_LISP), $"" (setf *features* (append $(features) *features*)) (load "$(ROOT)/Build/parse.lisp") (copy-lisp-file "$(lispfile)" "$(bodyfile)") (quit) "") # HELPER ROUTINES ------------------------------------------------------------- standard_cleaning() = # We remove the typical temporary files from a directory section rmfiles = *.cert *.o *.h *.out *.x86f *.date TMP.* TMP1.* *.work *.log *~ \#* *.omc \ autodoc/*.tex proofs/*.proof proofs/*.proofs *.fasl *.boot *.lx86cl64 *.lx64fsl \ *.dfsl *.body *.pcert *.mtime *.ccl *.ajout *.tem proofs/*.tem *.core foreach(r, $(rmfiles)): rm($(glob $(r)) -f) # ACL2 BOOK CERTIFICATION ----------------------------------------------------- %.cert: %.body section CertifyBook($(file $@), $(ACL2)) %.body: %.lisp section ExtractBody($(file $*.lisp), $""'(:acl2)"") %.mtime: %.body section announce_job($(file $@)) time = $(time stat --format="%y\n" $*.body > $*.mtime) check_job($(file $@), $(file $@), $(time)) %.pcert: %.mtime section PCertifyBook($(file $*), $(ACL2)) # Finally, include the top level OMakefile .SUBDIRS: .