diff options
Diffstat (limited to 'make_makefile')
| -rwxr-xr-x | make_makefile | 62 |
1 files changed, 0 insertions, 62 deletions
diff --git a/make_makefile b/make_makefile deleted file mode 100755 index 1cef3d3..0000000 --- a/make_makefile +++ /dev/null @@ -1,62 +0,0 @@ -#!/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 -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 - - -# override inadequate coq_makefile auto-regeneration -Makefile: make_makefile magic.txt files.txt - ./make_makefile - -# 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: $CMXA $CMXS aac_tactics.cma - -# .depend contains dependencies for .mli files --include .depend -.SECONDARY: .depend - -EOF -) > Makefile - - - -# TOTHINK: coq_makefile est bête, [make all] compile systématiquement -# les .cmxs associés à chaque module, alors que ça ne sert à rien, -# seul aac_rewrite.cmxs compte - -# problemes lorsqu'un module porte un meme nom qu'un module predefini -# (matching par exemple), prendre garde si ce probleme s'etend a la -# confusion module/nom de librairie |