
all: slides-pp.pdf poly-pp.pdf
	grep -w frametitle slides.tex | wc -l

%.pdf: %.tex
	rubber -d -s $^

OPTIONS=-e ocaml ocaml-colorbox-tt -m of why

%-pp.tex: %.tex
	latexpp -o $@ -g color yes -e of why -m of why $(OPTIONS) $^

WWW=/users/projets/why3/ssft-16/

export: slides-pp.pdf poly-pp.pdf
	scp slides-pp.pdf filliatr@moloch:$(WWW)/slides-filliatre.pdf
	scp demo_*.mlw demo_logic.why filliatr@moloch:$(WWW)
	scp poly-pp.pdf filliatr@moloch:$(WWW)/notes-why3.pdf

export-www:
	scp index.html filliatr@moloch:$(WWW)
	scp trywhy3_help.html filliatr@moloch:$(WWW)/trywhy3/

export-lab: lab.zip
	scp lab/*.mlw filliatr@moloch:$(WWW)/trywhy3/examples/
	scp lab.zip filliatr@moloch:$(WWW)

lab.zip: lab/*.mlw
	zip $@ $^

OCAMLLIB= why3__BuiltIn__BuiltIn.ml \
 int__Int.ml \
 why3__Prelude__Prelude.ml \
 ref__Ref.ml \
 ref__Refint.ml \
 array__Array.ml

EXTRACT=mjrty__Mjrty.ml

OPAM:=~/.opam/$(shell opam switch show)/lib

test_mjrty: $(EXTRACT) test_mjrty.ml
	ocamlopt -o $@ -annot -I $(OPAM)/zarith -I ~/why3/lib/why3 zarith.cmxa why3extract.cmxa $(OCAMLLIB) $(EXTRACT) test_mjrty.ml

$(EXTRACT):
	~/why3/bin/why3 extract -D ocaml64 -D mjrty.drv -L ~/why3/examples/ -T mjrty.Mjrty -o .

clean:
	rm -f *~ *.cm* *.o *.annot
	rm -f *.bak test_mjrty
	rm -f why3__*.ml
	rm -f array__*.ml int__*.ml map__*.ml ref__*.ml mjrty__Mjrty.ml

