#!/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