##############################################################################
# CFML setup.

CFML := ..

include $(CFML)/Makefile.common


##############################################################################
# Compilation.

# The official list of files that should be compiled by [make]
# and included in the archive by [make export].
SRC := $(shell cat FILES)

ifeq ($(ARTHUR),1)
	# Note: double space below is important for export.sh
	SRC  := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic  ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
endif

PWD := $(shell pwd)

V := $(addprefix $(PWD)/,$(SRC:=.v))

COQINCLUDE := \
  -R $(TLC) TLC \
  -R $(PWD) MODEL

include $(TLC)/Makefile.coq

# Exporting the self-contained archive.
.PHONY: export

demo:
	echo ${V}


export:
	./export.sh

export_francois: export
	scp -p -B -C seplogics.tar.gz yquem.inria.fr:public_html/dev/seplogics/