############################################################################### # Makefile for HOL Light # # # # Simple "make" just builds the camlp4 syntax extension "pa_j.cmo", which is # # necessary to load the HOL Light core into the OCaml toplevel. # # # # The later options such as "make hol" create standalone images, but only # # work under Linux when the "ckpt" checkpointing program is installed. # # # # See the README file for more detailed information about the build process. # # # # Thanks to Carl Witty for 3.07 and 3.08 ports of pa_j.ml and this process. # ############################################################################### # Installation directory for standalone binaries. Set here to the user's # binary directory. You may want to change it to something like /usr/local/bin BINDIR=${HOME}/bin # This is the list of source files in the HOL Light core HOLSRC=system.ml lib.ml type.ml term.ml thm.ml basics.ml nets.ml \ preterm.ml parser.ml printer.ml equal.ml bool.ml drule.ml \ tactics.ml itab.ml simp.ml theorems.ml ind_defs.ml class.ml \ trivia.ml canon.ml meson.ml quot.ml recursion.ml pair.ml \ nums.ml arith.ml wf.ml calc_num.ml normalizer.ml grobner.ml \ ind_types.ml lists.ml realax.ml calc_int.ml realarith.ml \ real.ml calc_rat.ml int.ml sets.ml iterate.ml cart.ml define.ml \ help.ml database.ml update_database.ml # Build the camlp4 syntax extension file (camlp5 for OCaml >= 3.10) pa_j.cmo: sources pa_j.ml; if test `ocamlc -version | cut -c1-4` = "3.10" -o `ocamlc -version | cut -c1-4` = "3.11" ; \ then ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml; \ else ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_j.ml; \ fi # Copy over and modify the sources sources:; cp ../../*.ml .; \ cp -f ../diffs/*.ml .; \ java -jar ../tools/nametheorems.jar *.ml; \ rm *.ml.old # Choose an appropriate camlp4 or camlp5 syntax extension. # # For OCaml < 3.10 (OCAML_BINARY_VERSION = "0"), this uses the built-in # camlp4, and in general there are different versions for each OCaml version # # For OCaml >= 3.10 (OCAML_BINARY_VERSION = "1"), this uses the separate # program camlp5. Now the appropriate syntax extensions is determined based # on the camlp5 version, currently just versions < 6.00 and >= 6.00 OCAML_VERSION=`ocamlc -version | cut -c1-4` OCAML_BINARY_VERSION=`ocamlc -version | cut -c3` CAMLP5_BINARY_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1` pa_j.ml: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx.ml; \ if test ${OCAML_BINARY_VERSION} = "0" ; \ then cp pa_j_${OCAML_VERSION}.ml pa_j.ml ; \ else cp pa_j_3.1x_${CAMLP5_BINARY_VERSION}.xx.ml pa_j.ml; \ fi # Compile depgraph depgraph.ml:; cp ../diffs/depgraph.ml . depgraph: depgraph.ml; ocamlc -a -I +ocamlgraph graph.cma -o depgraph.cma depgraph.ml # Create a top-level using str and depgraph top: depgraph; ocamlmktop -o top -I +ocamlgraph graph.cma depgraph.cma str.cma # Build a standalone hol image called "hol" (needs Linux and ckpt program) hol: pa_j.cmo ${HOLSRC} update_database.ml; \ if test `uname` = Linux; then \ echo -e '#use "make.ml";;\nloadt "update_database.ml";;\nself_destruct "";;' | ckpt -a SIGUSR1 -n hol.snapshot ocaml;\ mv hol.snapshot hol; \ else \ echo '******************************************************'; \ echo 'FAILURE: Image build assumes Linux and ckpt program'; \ echo '******************************************************'; \ fi # Build an image with multivariate calculus preloaded. hol.multivariate: ./hol \ Library/card.ml Library/permutations.ml Multivariate/misc.ml \ Library/products.ml Library/floor.ml Multivariate/vectors.ml \ Multivariate/determinants.ml Multivariate/topology.ml \ Multivariate/convex.ml Multivariate/polytope.ml \ Multivariate/dimension.ml Multivariate/derivatives.ml \ Multivariate/clifford.ml Multivariate/integration.ml \ Multivariate/measure.ml \ Multivariate/multivariate_database.ml update_database.ml; \ echo -e 'loadt "Multivariate/make.ml";;\nloadt "update_database.ml";;\nself_destruct "Preloaded with multivariate analysis";;' | ./hol; mv hol.snapshot hol.multivariate; # Build an image with analysis and SOS procedure preloaded hol.sosa: ./hol \ Library/analysis.ml Library/transc.ml \ Examples/sos.ml update_database.ml; \ echo -e 'loadt "Library/analysis.ml";;\nloadt "Library/transc.ml";;\nloadt "Examples/sos.ml";;\nloadt "update_database.ml";;\nself_destruct "Preloaded with analysis and SOS";;' | ./hol; mv hol.snapshot hol.sosa; # Build an image with cardinal arithmetic preloaded hol.card: ./hol Library/card.ml; update_database.ml; \ echo -e 'loadt "Library/card.ml";;\nloadt "update_database.ml";;\nself_destruct "Preloaded with cardinal arithmetic";;' | ./hol; mv hol.snapshot hol.card; # Build an image with multivariate-based complex analysis preloaded hol.complex: ./hol.multivariate \ Library/binomial.ml Library/iter.ml Multivariate/complexes.ml \ Multivariate/canal.ml Multivariate/transcendentals.ml \ Multivariate/realanalysis.ml Multivariate/cauchy.ml \ Multivariate/complex_database.ml update_database.ml; \ echo -e 'loadt "Multivariate/complexes.ml";;\nloadt "Multivariate/canal.ml";;\nloadt "Multivariate/transcendentals.ml";;\nloadt "Multivariate/realanalysis.ml";;\nloadt "Multivariate/cauchy.ml";;\nloadt "Multivariate/complex_database.ml";;\nloadt "update_database.ml";;\nself_destruct "Preloaded with multivariate-based complex analysis";;' | ./hol.multivariate; mv hol.snapshot hol.complex; # Build all those all: hol hol.multivariate hol.sosa hol.card hol.complex; # Build binaries and copy them to binary directory install: hol hol.multivariate hol.sosa hol.card hol.complex; cp hol hol.multivariate hol.sosa hol.card hol.complex ${BINDIR} # Clean up all generated files clean:; rm -f *.ml *.ml.old pa_j.cmi pa_j.cmo hol hol.multivariate hol.sosa hol.card clean_all: clean; rm -f *~ *.cma *.cmi *.cmo top top.exe