diff options
Diffstat (limited to 'make_makefile')
| -rwxr-xr-x | make_makefile | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/make_makefile b/make_makefile index 3cfc096..1cef3d3 100755 --- a/make_makefile +++ b/make_makefile @@ -1,35 +1,48 @@ +#!/bin/sh # - set variable MLIFILES so that it can be used in custom targets to # build documentation and dependencies for .mli files # - remove useless ' -I . .../plugins/ ' lines so that we can read something in the compilation log # - rename the rule for Makefile auto-regeneration, and replace it with an appropriate command # - patch the rule for cleaning doc # - include the .depend custom target, to take .mli dependencies into account +# - added some hackish settings of Variables, in order to be able to install the plugin in user-contrib (coq_makefile should define a "INSTALL" variables that we can modify, instead of copying 4 times the same code in install !) + +set -e + +if [ -f `ocamlc -where`/dynlink.cmxa ]; then + BEST=opt + CMXA=aac_tactics.cmxa + CMXS=aac_tactics.cmxs +else + BEST=byte + if which ocamlopt >/dev/null; then + CMXA=aac_tactics.cmxa + fi +fi ( -coq_makefile -no-install -opt MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \ - | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g' +coq_makefile -R . AAC_tactics -$BEST MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \ + | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g;s|\.opt||g' cat <<EOF -# sanity checks -tests: Tests.vo # override inadequate coq_makefile auto-regeneration Makefile: make_makefile magic.txt files.txt - . make_makefile + ./make_makefile -# We want to keep the proofs only in the Tutorial -tutorial: Tutorial.vo Tutorial.glob - \$(COQDOC) --no-index --no-externals -html \$(COQDOCLIBS) -d html Tutorial.v - -world: \$(VOFILES) doc gallinahtml tutorial +# We want to keep the proofs in Caveats and the Tutorial +world: \$(VOFILES) doc + - mkdir -p html + \$(COQDOC) -toc -utf8 -html -g \$(COQDOCLIBS) -d html \$(VFILES) + \$(COQDOC) --no-index --no-externals -s -utf8 -html \$(COQDOCLIBS) -d html Tutorial.v + \$(COQDOC) --no-index --no-externals -s -utf8 -html \$(COQDOCLIBS) -d html Caveats.v # additional dependencies for AAC (since aac_tactics.cmxs/cma are not # around the first time we run make, coqdep issues a warning and # ignores this dependency) # (one can safely select one of theses dependencies according to # coq' compilation mode--bytecode or native) -AAC.vo: aac_tactics.cmxs aac_tactics.cma - +AAC.vo: $CMXA $CMXS aac_tactics.cma # .depend contains dependencies for .mli files -include .depend |