<commit_before>PYTHON=python2.7
COQVERSION := $(shell coqc --version|grep "version 8.5")

ifeq "$(COQVERSION)" ""
$(error "Verdi Raft is only compatible with Coq version 8.5")
endif

COQPROJECT_EXISTS=$(wildcard _CoqProject)
ifeq "$(COQPROJECT_EXISTS)" ""
$(error "Run ./configure before running make")
endif

CHECKPATH := $(shell ./script/checkpaths.sh)

ifneq ("$(CHECKPATH)","")
$(info $(CHECKPATH))
$(warning checkpath reported an error)
endif

default: Makefile.coq
	$(MAKE) -f Makefile.coq
	$(MAKE) -C extraction/vard

quick: Makefile.coq
	$(MAKE) -f Makefile.coq quick

proofalytics:
	$(MAKE) -C proofalytics clean
	$(MAKE) -C proofalytics
	$(MAKE) -C proofalytics publish

STDBUF=$(shell [ -x "$$(which gstdbuf)" ] && echo "gstdbuf" || echo "stdbuf")

proofalytics-aux: Makefile.coq
	sed "s|^TIMECMD=$$|TIMECMD=$(PWD)/proofalytics/build-timer.sh $(STDBUF) -i0 -o0|" \
	  Makefile.coq > Makefile.coq_tmp
	mv Makefile.coq_tmp Makefile.coq
	$(MAKE) -f Makefile.coq

MLFILES = extraction/vard/ml/VarDRaft.ml extraction/vard/ml/VarDRaft.mli

Makefile.coq: raft/RaftState.v _CoqProject
	coq_makefile -f _CoqProject -o Makefile.coq \
	  -extra 'script/assumptions.vo script/assumptions.glob script/assumptions.v.d' \
	    'script/assumptions.v raft-proofs/EndToEndLinearizability.vo' \
	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) script/assumptions.v' \
          -extra '$(MLFILES)' \
	    'extraction/vard/coq/ExtractVarDRaft.v extraction/vard/coq/VarDRaft.vo' \
	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) extraction/vard/coq/ExtractVarDRaft.v'

raft/RaftState.v:
	$(PYTHON) script/extract_record_notation.py raft/RaftState.v.rec raft_data > raft/RaftState.v

clean:
	if [ -f Makefile.coq ]; then \
	  $(MAKE) -f Makefile.coq cleanall; fi
	rm -f Makefile.coq raft/RaftState.v
	find . -name '*.buildtime' -delete
	$(MAKE) -C proofalytics clean
	$(MAKE) -C extraction/vard clean

vard:
	@echo "To build everything (including vard) use the default target."
	@echo "To quickly provision vard use the vard-quick target."

$(MLFILES): Makefile.coq
	$(MAKE) -f Makefile.coq $@

vard-quick:
	+$(MAKE) -C extraction/vard

vard-test:
	+$(MAKE) -C extraction/vard test

lint:
	@echo "Possible use of hypothesis names:"
	find . -name '*.v' -exec grep -Hn 'H[0-9][0-9]*' {} \;

distclean: clean
	rm -f _CoqProject extraction/vard/lib

.PHONY: default quick clean vard vard-quick vard-test lint proofalytics distclean
<commit_msg>ml files PHONY in main Makefile to rebuild when Coq files change<commit_after>PYTHON=python2.7
COQVERSION := $(shell coqc --version|grep "version 8.5")

ifeq "$(COQVERSION)" ""
$(error "Verdi Raft is only compatible with Coq version 8.5")
endif

COQPROJECT_EXISTS=$(wildcard _CoqProject)
ifeq "$(COQPROJECT_EXISTS)" ""
$(error "Run ./configure before running make")
endif

CHECKPATH := $(shell ./script/checkpaths.sh)

ifneq ("$(CHECKPATH)","")
$(info $(CHECKPATH))
$(warning checkpath reported an error)
endif

default: Makefile.coq
	$(MAKE) -f Makefile.coq
	+$(MAKE) -C extraction/vard

quick: Makefile.coq
	$(MAKE) -f Makefile.coq quick

proofalytics:
	$(MAKE) -C proofalytics clean
	$(MAKE) -C proofalytics
	$(MAKE) -C proofalytics publish

STDBUF=$(shell [ -x "$$(which gstdbuf)" ] && echo "gstdbuf" || echo "stdbuf")

proofalytics-aux: Makefile.coq
	sed "s|^TIMECMD=$$|TIMECMD=$(PWD)/proofalytics/build-timer.sh $(STDBUF) -i0 -o0|" \
	  Makefile.coq > Makefile.coq_tmp
	mv Makefile.coq_tmp Makefile.coq
	$(MAKE) -f Makefile.coq

MLFILES = extraction/vard/ml/VarDRaft.ml extraction/vard/ml/VarDRaft.mli

Makefile.coq: raft/RaftState.v _CoqProject
	coq_makefile -f _CoqProject -o Makefile.coq \
	  -extra 'script/assumptions.vo script/assumptions.glob script/assumptions.v.d' \
	    'script/assumptions.v raft-proofs/EndToEndLinearizability.vo' \
	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) script/assumptions.v' \
          -extra '$(MLFILES)' \
	    'extraction/vard/coq/ExtractVarDRaft.v extraction/vard/coq/VarDRaft.vo' \
	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) extraction/vard/coq/ExtractVarDRaft.v'

raft/RaftState.v:
	$(PYTHON) script/extract_record_notation.py raft/RaftState.v.rec raft_data > raft/RaftState.v

clean:
	if [ -f Makefile.coq ]; then \
	  $(MAKE) -f Makefile.coq cleanall; fi
	rm -f Makefile.coq raft/RaftState.v
	find . -name '*.buildtime' -delete
	$(MAKE) -C proofalytics clean
	$(MAKE) -C extraction/vard clean

vard:
	@echo "To build everything (including vard) use the default target."
	@echo "To quickly provision vard use the vard-quick target."

$(MLFILES): Makefile.coq
	$(MAKE) -f Makefile.coq $@

vard-quick:
	+$(MAKE) -C extraction/vard

vard-test:
	+$(MAKE) -C extraction/vard test

lint:
	@echo "Possible use of hypothesis names:"
	find . -name '*.v' -exec grep -Hn 'H[0-9][0-9]*' {} \;

distclean: clean
	rm -f _CoqProject extraction/vard/lib

.PHONY: default quick clean vard vard-quick vard-test lint proofalytics distclean $(MLFILES)

{'fraction_non_alphanumeric': 0.15375178900020445, 'fraction_numerical': 0.0049069719893682275, 'mean_word_length': 4.198724760892667, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3759116', 'n_tokens_mistral': 1973, 'n_tokens_neox': 1868, 'n_words': 448}