Makefile

.PHONY: all install plugin check checker clean development-without-install revert-development-without-install

-include Makefile.rocq.conf

all : Makefile.rocq
	$(MAKE) -f Makefile.rocq $@

install : Makefile.rocq
	test ! theories -ef $(COQMF_COQLIB)/user-contrib/codegen || ( echo "$(COQMF_COQLIB)/user-contrib/codegen is linked to theories.  No need to install."; false )
	$(MAKE) -f Makefile.rocq $@

uninstall : Makefile.rocq
	test ! theories -ef $(COQMF_COQLIB)/user-contrib/codegen || ( echo "$(COQMF_COQLIB)/user-contrib/codegen is linked to theories.  Use revert-development-without-install."; false )
	$(MAKE) -f Makefile.rocq $@

ifdef COQMF_COQLIB
development-without-install : revert-development-without-install
	ln -s META.rocq-codegen src/META
	ln -s `pwd`/theories "$(COQMF_COQLIB)/user-contrib/codegen"
	ln -s `pwd`/src "$(COQMF_COQLIB)/../rocq-codegen"

revert-development-without-install :
	rm -f "$(COQMF_COQLIB)/user-contrib/codegen" "$(COQMF_COQLIB)/../rocq-codegen" || ( echo "Do 'make uninstall' first"; false )
	rm -f src/META
else
development-without-install :
	@echo 'COQMF_COQLIB not defined.  run "make" first.'
revert-development-without-install :
	@echo 'COQMF_COQLIB not defined.  run "make" first.'
endif

plugin : Makefile.rocq
	$(MAKE) -f Makefile.rocq src/codegen_plugin.cmxs

.merlin : Makefile.rocq
	$(MAKE) -f Makefile.rocq .merlin

# Makefile.rocq.conf is also generated by "rocq makefile".
Makefile.rocq : _CoqProject
	rocq makefile -f _CoqProject -o Makefile.rocq

check checker:
	cd test; $(MAKE) $@
	rocq c -Q theories codegen -I src test/test_verify.v

run-sample:
	rocq top -Q theories codegen -I src -batch -l sample/ind.v
	rocq top -Q theories codegen -I src -batch -l sample/genc.v
	rocq c -Q theories codegen -I src sample/pow.v
	gcc -g -Wall sample/pow.c -o sample/pow
	sample/pow
	rocq c -Q theories codegen -I src sample/rank.v
	gcc -g -Wall sample/rank.c -o sample/rank
	sample/rank 11011110001010101111
	rocq c -Q theories codegen -I src sample/sprintf.v
	gcc -g -Wall sample/sprintf.c -o sample/sprintf
	sample/sprintf
	(cd sample/lseq; make clean all; ./test_lseq)
	(cd sample/str; make clean all)
	(cd sample/str2; make clean all)

clean :
	rm -f \
	  .Makefile.rocq.d \
	  src/g_codegen.ml \
	  src/*.o \ \
	  src/*.cmi \
	  src/*.cmo \
	  src/*.cmx \
	  src/*.cma \
	  src/*.cmt \
	  src/*.cmti \
	  src/*.cmxa \
	  src/*.cmxs \
	  src/*.a \
	  src/*.d \
	  src/*.annot \
	  theories/*.glob \
	  theories/*.vo \
	  theories/*.vok \
	  theories/*.vos \
	  theories/*.d \
	  theories/.*.aux \
	  test/*.cache \
	  test/test_codegen \
	  test/*.cmi \
	  test/*.cmx \
	  test/*.o \
	  test/oUnit-* \
	  sample/pow \
	  sample/rank \
	  sample/*.vo \
	  sample/*.vok \
	  sample/*.vos \
	  sample/*.glob \
	  sample/.*.aux \
	  oUnit-*

distclean : clean
	rm -f \
	  Makefile.rocq \
	  Makefile.rocq.conf \
	  theories/codegen_plugin.cmi \
	  theories/codegen_plugin.cmx \
	  theories/codegen_plugin.cmxa \
	  theories/codegen_plugin.cmxs