Makefile.coq.local

include Makefile.ml-files

script/assumptions.vo script/assumptions.glob script/assumptions.v.d: script/assumptions.v theories/RaftProofs/EndToEndLinearizability.vo
	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) script/assumptions.v

$(VARDML): extraction/vard/coq/ExtractVarDRaft.v theories/Systems/VarDRaft.vo
	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard/coq/ExtractVarDRaft.v

$(VARDSERML): extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v theories/Systems/VarDRaftSerialized.vo
	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v

$(VARDLOGML): extraction/vard-log/coq/ExtractVarDRaftLog.v theories/Systems/VarDRaftLog.vo
	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-log/coq/ExtractVarDRaftLog.v

$(VARDSERLOGML): extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v theories/Systems/VarDRaftSerializedLog.vo
	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v

$(VARDDEBUGML): extraction/vard-debug/coq/ExtractVarDRaftDebug.v theories/Systems/VarDRaft.vo
	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-debug/coq/ExtractVarDRaftDebug.v

clean::
	rm -f script/assumptions.vo script/assumptions.glob script/assumptions.v.d \
	  script/.assumptions.vo.aux script/.assumptions.aux \
	  $(VARDML) \
	  $(VARDSERML) \
	  $(VARDLOGML) \
	  $(VARDSERLOGML) \
	  $(VARDDEBUGML)