<commit_before>
OTHERFLAGS+=$(FLAGS) $(LIB) --include ../dm4free
FSTAR_HOME=../..
include ../Makefile.include

uall: all

.PHONY: benton2004 uall all benton2004 test pack clean

all:\
  benton2004\
  Bijection.uver\
  Equivalence.uver\
  IfcComposeReify.uver\
  IfcDeclassify.uver\
  IfcDelimitedRelease.uver\
  IfcDelimitedReleaseReify.uver\
  IfcExample.uver\
  IfcExampleReify0.uver\
  IfcExampleReify1.uver\
  IfcExampleReify2.uver\
  IfcExampleReify3.uver\
  IfcRecursiveHeapReify.uver\
  IfcRecursiveReify.uver\
  IfcReificationRegressionTest.uver\
  IfcRules.uver\
  IfcRulesReify.uver\
  IfcTypechecker.uver\
  Loops.uver\
  Memo.uver\
  NetKat.uver\
  OneTimePad.uver\
  Point.uver\
  ProgramEquivalence.uver\
  ProgramOptimizations.uver\
  RandomTapes.uver\
  Recursive.uver\
  ReifyLong.uver\
  Rel.uver\
  StRel.uver\
  Swap.uver\
  UnionFind.Forest.uver\
  UnionFind.uver\
  UnionFind.Functions.uver\
  While.uver\
  WhileReify.uver \
  OTP.uver \
  ElGamal.uver


benton2004:\
  Benton2004.Aux.uver\
  Benton2004.uver\
  Benton2004.DDCC.uver\
  Benton2004.DDCC.Examples.uver\
  Benton2004.SmithVolpano.uver\
  Benton2004.RHL.uver\
  Benton2004.RHL.Examples.uver\
  Benton2004.RHL.Derived.uver\
  Benton2004.RHL.Examples2.uver\

test :\
  Loops.uver \
  Memo.uver\
  NetKat.uver\
  OneTimePad.uver\
  Point.uver\
  ProgramEquivalence.uver\
  ProgramOptimizations.uver\
  RandomTapes.uver


%.fst-in:
	@echo $(OTHERFLAGS)

pack:
	cd ../..; zip -r relational.zip examples/rel examples/dm4free

FIND=$(shell which gfind > /dev/null 2>&1 && echo gfind || echo find)
SED=$(shell which gsed > /dev/null 2>&1 && echo gsed || echo sed)

MODULES=$(shell $(SED) -e 's!^\([^,]*\).*$$!\1!' < sections.csv | xargs echo)

sections-sorted.csv:
	sort -t , -k 1,1 < sections.csv > sections-sorted.csv

modules-sorted.csv:
	i=0; for f in $(MODULES) ; do echo $$i,$$f ; i=$$(($$i + 1)) ; done | sort -t , -k 2,2 > modules-sorted.csv

results_without_hints:
	+HINTS_ENABLED='' OTHERFLAGS='--record_hints' make -k $(addsuffix .uver,$(MODULES)) > results_without_hints || :

results_with_hints:
	+make -k $(addsuffix .uver,$(MODULES)) > results_with_hints || :

timings_without_hints.csv: results_without_hints
	$(SED) -n results_without_hints -e '/Verified/s/.*: \([^ ]*\) (\([0-9]*\) .*/\1,\2/p' \
		| sort -t , -k 1,1 \
		 > timings_without_hints.csv

timings_with_hints.csv: results_with_hints
	$(SED) -n results_with_hints -e '/Verified/s/.*: \([^ ]*\) (\([0-9]*\) .*/\1,\2/p' \
		| sort -t , -k 1,1 \
		 > timings_with_hints.csv

loc.csv:
	for f in $(MODULES) ; do echo -n $$f, ; wc -l < $$f.fst ; done \
		| sort -t , -k 1,1 \
		 > loc.csv

timings0.csv: timings_without_hints.csv timings_with_hints.csv
	join --check-order -t , -1 1 -2 1 timings_without_hints.csv timings_with_hints.csv > timings0.csv

timings1.csv: timings0.csv loc.csv
	join --check-order -t , -1 1 -2 1 timings0.csv loc.csv > timings1.csv
	#rm results_without_hints results_with_hints timings_without_hints.csv timings_with_hints.csv loc.csv timings0.csv

timings2.csv: timings1.csv sections-sorted.csv
	join --check-order -t , -1 1 -2 1 sections-sorted.csv timings1.csv | sort -t , -k 1,1 > timings2.csv

timings.csv: timings2.csv modules-sorted.csv
	echo 'filename,section,timings (no hints),timings (with hints),loc' > timings.csv
	join --check-order -t , -1 1 -2 2 timings2.csv modules-sorted.csv | sort -n -t , -k 6,6 | $(SED) 's!,[0-9]*$$!!' >> timings.csv

clean:
	rm -f sections-sorted.csv modules-sorted.csv results_without_hints results_with_hints timings_without_hints.csv timings_with_hints.csv loc.csv timings0.csv timings1.csv timings2.csv timings.csv<commit_msg>Table headers as in the paper<commit_after>
OTHERFLAGS+=$(FLAGS) $(LIB) --include ../dm4free
FSTAR_HOME=../..
include ../Makefile.include

uall: all

.PHONY: benton2004 uall all benton2004 test pack clean

all:\
  benton2004\
  Bijection.uver\
  Equivalence.uver\
  IfcComposeReify.uver\
  IfcDeclassify.uver\
  IfcDelimitedRelease.uver\
  IfcDelimitedReleaseReify.uver\
  IfcExample.uver\
  IfcExampleReify0.uver\
  IfcExampleReify1.uver\
  IfcExampleReify2.uver\
  IfcExampleReify3.uver\
  IfcRecursiveHeapReify.uver\
  IfcRecursiveReify.uver\
  IfcReificationRegressionTest.uver\
  IfcRules.uver\
  IfcRulesReify.uver\
  IfcTypechecker.uver\
  Loops.uver\
  Memo.uver\
  NetKat.uver\
  OneTimePad.uver\
  Point.uver\
  ProgramEquivalence.uver\
  ProgramOptimizations.uver\
  RandomTapes.uver\
  Recursive.uver\
  ReifyLong.uver\
  Rel.uver\
  StRel.uver\
  Swap.uver\
  UnionFind.Forest.uver\
  UnionFind.uver\
  UnionFind.Functions.uver\
  While.uver\
  WhileReify.uver \
  OTP.uver \
  ElGamal.uver


benton2004:\
  Benton2004.Aux.uver\
  Benton2004.uver\
  Benton2004.DDCC.uver\
  Benton2004.DDCC.Examples.uver\
  Benton2004.SmithVolpano.uver\
  Benton2004.RHL.uver\
  Benton2004.RHL.Examples.uver\
  Benton2004.RHL.Derived.uver\
  Benton2004.RHL.Examples2.uver\

test :\
  Loops.uver \
  Memo.uver\
  NetKat.uver\
  OneTimePad.uver\
  Point.uver\
  ProgramEquivalence.uver\
  ProgramOptimizations.uver\
  RandomTapes.uver


%.fst-in:
	@echo $(OTHERFLAGS)

pack:
	cd ../..; zip -r relational.zip examples/rel examples/dm4free

FIND=$(shell which gfind > /dev/null 2>&1 && echo gfind || echo find)
SED=$(shell which gsed > /dev/null 2>&1 && echo gsed || echo sed)

MODULES=$(shell $(SED) -e 's!^\([^,]*\).*$$!\1!' < sections.csv | xargs echo)

sections-sorted.csv:
	sort -t , -k 1,1 < sections.csv > sections-sorted.csv

modules-sorted.csv:
	i=0; for f in $(MODULES) ; do echo $$i,$$f ; i=$$(($$i + 1)) ; done | sort -t , -k 2,2 > modules-sorted.csv

results_without_hints:
	+HINTS_ENABLED='' OTHERFLAGS='--record_hints' make -k $(addsuffix .uver,$(MODULES)) > results_without_hints || :

results_with_hints:
	+make -k $(addsuffix .uver,$(MODULES)) > results_with_hints || :

timings_without_hints.csv: results_without_hints
	$(SED) -n results_without_hints -e '/Verified/s/.*: \([^ ]*\) (\([0-9]*\) .*/\1,\2/p' \
		| sort -t , -k 1,1 \
		 > timings_without_hints.csv

timings_with_hints.csv: results_with_hints
	$(SED) -n results_with_hints -e '/Verified/s/.*: \([^ ]*\) (\([0-9]*\) .*/\1,\2/p' \
		| sort -t , -k 1,1 \
		 > timings_with_hints.csv

loc.csv:
	for f in $(MODULES) ; do echo -n $$f, ; wc -l < $$f.fst ; done \
		| sort -t , -k 1,1 \
		 > loc.csv

timings0.csv: timings_without_hints.csv timings_with_hints.csv
	join --check-order -t , -1 1 -2 1 timings_without_hints.csv timings_with_hints.csv > timings0.csv

timings1.csv: timings0.csv loc.csv
	join --check-order -t , -1 1 -2 1 timings0.csv loc.csv > timings1.csv
	#rm results_without_hints results_with_hints timings_without_hints.csv timings_with_hints.csv loc.csv timings0.csv

timings2.csv: timings1.csv sections-sorted.csv
	join --check-order -t , -1 1 -2 1 sections-sorted.csv timings1.csv | sort -t , -k 1,1 > timings2.csv

timings.csv: timings2.csv modules-sorted.csv
	echo 'filename,section,1st run (ms),proof replay (ms),loc' > timings.csv
	join --check-order -t , -1 1 -2 2 timings2.csv modules-sorted.csv | sort -n -t , -k 6,6 | $(SED) 's!,[0-9]*$$!!' >> timings.csv

clean:
	rm -f sections-sorted.csv modules-sorted.csv results_without_hints results_with_hints timings_without_hints.csv timings_with_hints.csv loc.csv timings0.csv timings1.csv timings2.csv timings.csv
{'fraction_non_alphanumeric': 0.15344567749006713, 'fraction_numerical': 0.03356624195095219, 'mean_word_length': 3.4242424242424243, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 37, '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': '5071358', 'n_tokens_mistral': 3302, 'n_tokens_neox': 3142, 'n_words': 576}