definitions:
	Holmake lts_memory_modelTheory.uo axiomatic_memory_modelTheory.uo typesettingTheory.uo moretypesettingTheory.uo

checker:
	cd proofs && Holmake executable_checkerTheory.uo
	cd proofs/ocaml; ocamlbuild -I Caml executable_checkerML.o

proof:
	cd proofs && Holmake lts_axiomatic_equivTheory.uo correct_typesettingTheory.uo lts_erasureTheory.uo linear_valid_executionTheory.uo  

clean:
	Holmake cleanAll
	cd proofs && Holmake cleanAll

# clean removes the Holmake-generated files only.  make realclean is
# defined below; it removes also all the document-related files

all:
	make definitions
	##make checker
	make proof
	make holdoc-tools
	make install-alldoc-tso
	#cd ../doc; make x86tso-paper.pdf



################################################################
#                                                              #
#  HolDoc typesetting generation and spec tarball construction #
#                                                              #
################################################################

HOLDOCDIR=../HOLDoc
LTSHOLDOCDIR=../HOLDoc_Net

holdoc-tools:
	cd ${HOLDOCDIR}; make 
	cd ${LTSHOLDOCDIR}; make 

# to make the documents with "make alldoc-tso", one has to "make definitions" first, to run HOL on the definition files in order to generate the imn files

alldoc-tso: alldoc-tso.ps alldoc-tso.pdf

install-alldoc-tso: alldoc-tso-inc.tex alldoc-tso.ps glommed-imn-tso.imn
	cp -f alldoc-tso-inc.tex ../doc/generated_alldoc
	cp -f alldoc-tso.ps ../doc/generated_alldoc
	cp -f glommed-imn-tso.imn ../doc/generated_alldoc

tarball: tarball-tso-spec-public.tar.gz

install-tarball: tarball-tso-spec-public.tar.gz
	rm -rf ~pes20/public_html/weakmemory/tarball-tso-spec-public*
	cp -f tarball-tso-spec-public.tar.gz ~pes20/public_html/weakmemory
	cd ~pes20/public_html/weakmemory ; tar -zxvf tarball-tso-spec-public.tar.gz

LATEX=latex
PDFLATEX=extra_mem_top=1000000 pdflatex
DVIPS=dvips
PSTOPDF=ps2pdf

LTS_TO_LATEX=$(LTSHOLDOCDIR)/lts_to_latex
MNG_TO_LATEX=${HOLDOCDIR}/mng_to_latex

DVIPSFLAGS=-t a4 -Ppdf -j1 -G0

# IMNFILES order may be significant.
IMNFILESTSO=x86_auto_tso.imn  x86_extraimn.imn x86_typeabbrev_tso.imn #util.imn
#x86_.imn
EXTRATEXINPUTS=${HOLDOCDIR}:$(LTSHOLDOCDIR)
OTHERTEXFILES=

# lists of files:


# TSOSPECTHEORYFILES are the for-public-consumption files to be typeset
#  (listed here in a sensible order)

TSOSPECTHEORYFILES=\
axiomatic_memory_modelScript.sml \
typesettingScript.sml \
moretypesettingScript.sml\
lts_memory_modelScript.sml\
proofs/lts_erasureScript.sml\
proofs/linear_valid_executionScript.sml\
proofs/lts_traceScript.sml\
proofs/lts_axiomatic_equivScript.sml\
proofs/executable_checkerScript.sml\
proofs/correct_typesettingScript.sml


#TSOSPECDEFNPUBLICFILES are the toplevel defn files, to be included in the tarball
TSOSPECDEFNPUBLICFILES=\
axiomatic_memory_modelScript.sml \
typesettingScript.sml \
moretypesettingScript.sml\
lts_memory_modelScript.sml\

# TSOSPECPROOFPUBLICFILES are the proof/ public files, to be included in the tarball
TSOSPECPROOFPUBLICFILES= \
basic_lemmasScript.sml         linear_valid_executionScript.sml  lts_traceScript.sml  utilScript.sml correct_typesettingScript.sml lts_axiomatic_equivHand executable_checkerScript.sml   lts_axiomatic_equivScript.sml     utilLib.sig Holmakefile                    lts_erasureScript.sml             utilLib.sml 

# TSOSPECOTHERPUBLICFILES are the other toplevel public files, to be included in the tarball
TSOSPECOTHERPUBLICFILES=    \
HolDoc.sig                  \
HolDoc.sml		    \
Holmakefile		    \
Makefile		    \
Net_Hol_reln.sig	    \
Net_Hol_reln.sml	    \
README			    \
set_relationScript.sml      


TSOSPECTHEORIES=$(patsubst %Script.sml,%,$(TSOSPECTHEORYFILES))
TSOSPECTHEORYIMNS=$(addsuffix .imn, $(TSOSPECTHEORIES))
TSOSPECTHEORYPSFILES=$(addsuffix -doc.ps, $(TSOSPECTHEORIES))
TSOSPECTHEORYPDFFILES=$(addsuffix -doc.pdf, $(TSOSPECTHEORIES))


TSOSPECPUBLICFILES=$(TSOSPECDEFNPUBLICFILES) $(TSOSPECOTHERPUBLICFILES)


reheader: LICENSE
	headache -h LICENCE $(TSOSPECDEFNPUBLICFILES) Holmakefile set_relationScript.sml
	cd proofs; headache -h LICENCE $(TSOSPECPROOFPUBLICFILES)

tarball-tso-spec-public.tar.gz: alldoc-tso.ps alldoc-tso.pdf
	rm -rf tarball-tso-spec-public*
	mkdir tarball-tso-spec-public
	mkdir tarball-tso-spec-public/proofs
	cp $(TSOSPECPUBLICFILES) tarball-tso-spec-public
	cd proofs; cp $(TSOSPECPROOFPUBLICFILES) ../tarball-tso-spec-public/proofs
	svn status -v $(TSOSPECPUBLICFILES) > tarball-tso-spec-public/VERSIONS-spec-public
	cp Makefile  tarball-tso-spec-public/Makefile
	cp alldoc-tso.ps alldoc-tso.pdf tarball-tso-spec-public/
	tar -cvf tarball-tso-spec-public.tar tarball-tso-spec-public
	gzip tarball-tso-spec-public.tar



HOLTHEORIES=$(patsubst %Script.sml,%,$(wildcard *Script.sml))

# Theories that don't generate .imn files:
NONIMNTHEORIES=integer_word32 LetCompute

HOLTHEORYIMNS=$(addsuffix .imn, $(filter-out $(NONIMNTHEORIES), $(HOLTHEORIES)))

## hack to generate brief table of contents
BRIEFTOC='Contents|Index|{part}'   # {chapter}|{section}|{bchy}'


#
# hack from GNU Make manual, to set $(space) to a single space:
#
nullstring :=
space := $(nullstring) # end of the line




# .imn files contain identifier information for use by lts_to_latex
# They are produced as follows.
#
# .imn files from the HOL theories, the $(TSOSPECTHEORYIMNS), e.g. 
# axiomatic_memory_model.imn, are made when HOL builds the theories 
# (by the HolDoc package)
# 
# x86_auto_tso.imn is made by a target below that concatenates 
# the $(TSOSPECTHEORYIMNS)
# 
# x86_typeabbrev_tso.imn is made by a target below that pulls out 
# HOL type abbreviations from $(TSOSPECTHEORYFILES) (using sed)
# 
# x86_extraimn.imn is some hand-written extra imn configuration, e.g. for
# HOL library identifiers

glommed-imn-tso.imn: $(EXTRAIMNFILES) $(IMNFILESTSO)
	cat $(EXTRAIMNFILES) $(IMNFILESTSO) > glommed-imn-tso.imn


# Intermediate tex files - lts_to_latex is used to build:
#
# %.tmp2-tex  for standalone alldoc-tso.pdf
# %.tmp3-tex  for includable alldoc-tso-inc.tex



%.tmp-tex : %Script.sml $(if ${FAST},,${IMNFILES}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX) $(EXTRAIMNFILES) $(IMNFILES) $< > $@



# special-case the tex generation for some of the tso files 

typesetting.tmp2-tex : typesettingScript.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX)  -nocmds -texprefix  -nomerge $(EXTRAIMNFILES) $(IMNFILESTSO) typesettingScript.sml > $@

typesetting.tmp3-tex : typesettingScript.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX)  -bodies -texprefix "Typesetting" -cmds -nomerge $(EXTRAIMNFILES) $(IMNFILESTSO) typesettingScript.sml > $@
#-bodies

moretypesetting.tmp2-tex : moretypesettingScript.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX)  -nocmds -texprefix  -nomerge $(EXTRAIMNFILES) $(IMNFILESTSO) moretypesettingScript.sml > $@

moretypesetting.tmp3-tex : moretypesettingScript.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX)  -bodies  -texprefix "Typesetting" -cmds -nomerge $(EXTRAIMNFILES) $(IMNFILESTSO) moretypesettingScript.sml > $@
#-bodies

typesetting_proofs.tmp2-tex : typesetting_proofsScript.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX)  -nocmds -nomerge $(EXTRAIMNFILES) $(IMNFILESTSO) typesetting_proofsScript.sml > $@

typesetting_proofs.tmp3-tex : typesetting_proofsScript.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX)  -bodies -texprefix "" -cmds -nomerge $(EXTRAIMNFILES) $(IMNFILESTSO) typesetting_proofsScript.sml > $@
#-bodies





# non-special cases

%.tmp2-tex : %Script.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX) -nocmds $(EXTRAIMNFILES) $(IMNFILESTSO) $< > $@

%.tmp3-tex : %Script.sml $(if ${FAST},,${IMNFILESTSO}) ${LTS_TO_LATEX}
	$(LTS_TO_LATEX) -bodies -texprefix "" -cmds -nomerge $(EXTRAIMNFILES) $(IMNFILESTSO) $< > $@


alldoc-tso.tex : alldoc-tso-pre.template alldoc-between.template alldoc-post.template $(addsuffix .tmp2-tex, $(TSOSPECTHEORIES))
	(echo "% auto-generated file; do not edit"; \
	cat alldoc-tso-pre.template; \
	for f in $(TSOSPECTHEORIES); do \
		h=`basename $$f`;\
		g=`echo $$h | sed -e 's/_/\\\\\\\\protect\\\\\\\\textunderscore /g'`; \
		cat alldoc-between.template | sed -e "s/THEORYNAME/$$g/g"; \
		cat $$f.tmp2-tex; \
	done; \
	cat alldoc-post.template \
	) > $@


junk-all.tex : alldoc-tso-pre.template alldoc-between.template alldoc-post.template junk.tex
	cat alldoc-tso-pre.template junk.tex  alldoc-post.template  > junk-all.tex 


alldoc-tso-inc.tex  : alldoc-inc-pre.template alldoc-inc-between.template alldoc-inc-post.template $(addsuffix .tmp3-tex, $(TSOSPECTHEORIES))
	(echo "% auto-generated file; do not edit"; \
	cat alldoc-inc-pre.template; \
	for f in $(TSOSPECTHEORIES); do \
		h=`basename $$f`;\
		g=`echo $$h | sed -e 's/_/\\\\\\\\protect\\\\\\\\textunderscore /g'`; \
		cat alldoc-inc-between.template  | sed -e "s/THEORYNAME/$$g/g"; \
		cat $$f.tmp3-tex; \
	done; \
	cat alldoc-inc-post.template \
	) > $@



alldoc-tso-inc.dvi : alldoc-tso-inc.tex
	@echo
	@echo "Sorry, you can't build alldoc-tso-inc directly; you must include it in another document"
	@exit 1


x86_typeabbrev_tso.imn: $(TSOSPECTHEORYFILES)
	echo '(*[ NOECHO ]*)' > $@
	echo '(*[ C  AUTOGENERATED -- DO NOT EDIT ]*)' >> $@
	echo '(*[ TYPE_LIST' >> $@
	grep "type_abbrev" $(TSOSPECTHEORYFILES) | cut -f2 -d\" >> $@
	echo ']*)' >> $@
	echo '(*[ ECHO ]*)' >> $@

x86_auto_tso.imn: $(TSOSPECTHEORYIMNS)
	echo '(*[ NOECHO ]*)' > $@
	cat $(TSOSPECTHEORYIMNS) >> $@
#	cat $(filter-out %LIBinterface.imn %ruleids.imn, $(TSOSPECTHEORYIMNS)) >> $@
#	cat $(filter     %LIBinterface.imn, $(TSOSPECTHEORYIMNS)) | \
#		sed -e 's/CON_LIST/LIB_LIST/' - >> $@
#	echo '(*[ CLASS RULE "\tsrule" ]*)' >> $@
#	cat $(filter     %ruleids.imn, $(TSOSPECTHEORYIMNS)) | \
#		sed -e 's/CON_LIST/CLASS_LIST RULE/' - >> $@
	echo '(*[ ECHO ]*)' >> $@



# implicit rules:

.PRECIOUS: %.tmp-tex %-doc.tex %.dvi %.tob



%.dvi %.pdf : %.tex $(LTSHOLDOCDIR)/ltsmunge.sty $(OTHERTEXFILES)
	TEXINPUTS=$(subst $(space),:,$(strip $(EXTRATEXINPUTS))):$(TEXINPUTS) $(LATEX) $<
	-makeindex $*
	TEXINPUTS=$(subst $(space),:,$(strip $(EXTRATEXINPUTS))):$(TEXINPUTS) $(LATEX) $<
	TEXINPUTS=$(subst $(space),:,$(strip $(EXTRATEXINPUTS))):$(TEXINPUTS) $(PDFLATEX) $<

%.tex : %.mng $(if ${FAST},,${IMNFILES}) ${MNG_TO_LATEX}
	  $(MNG_TO_LATEX) $(IMNFILES) $*.mng > $*.tex

%.ps : %.dvi
	$(DVIPS) $(DVIPSFLAGS) $< -o $@.tmp
	mv $@.tmp $@

%.pdf : %.ps
	$(PSTOPDF) $< $@.tmp
	mv $@.tmp $@

wc:
	wc -l -c   $(SPECTHEORYFILES)
#	wc -l -c   $(CHECKERSOURCEFILES)

realclean: clean
	rm -f $(HOLTHEORYIMNS) x86_auto_tso.imn x86_typeabbrev_tso.imn
	rm -f .HOLMK  alldoc-tso.idx alldoc-tso.ilg alldoc-tso-inc.idx alldoc-tso-inc.log alldoc-tso-inc.tex alldoc-tso.ind alldoc-tso.log alldoc-tso.out alldoc-tso.pdf alldoc-tso.ps alldoc-tso.tex alldoc-tso.tob alldoc-tso.toc alldoc-tso.aux alldoc-tso.dvi *.tmp2-tex *.tmp3-tex

# extra dependencies:

%-doc.dvi : $(LTSHOLDOCDIR)/ltsmunge.sty tcp.sty

# end