<commit_before>FSTAR_HOME=../..
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)
FSTARTACLIB=$(FSTAR_HOME)/bin/fstar-tactics-lib/fstartaclib.cmxs

# Tests for which the native tactics used in module named Sample.Test.fst are
# declared in a corresponding module named Sample.fst
TAC_MODULES=Print\
    Split\
    BV\
    UnitTests\
    Bane\
    Canon\
    Simple\
    SimpleTactic\
    Evens\
    Embeddings\
    Plugins

# Tests for which the native tatics are declared and used in the same module
ALL=Apply\
    Arith\
    CanonDeep\
    Clear\
    Cut\
    DependentSynth\
    Fail\
    Imp\
    Logic\
    Nest\
    Pruning\
    Rename\
    Retype\
    Sequences\
    Simplifier\
    Tutorial\
    Unify

all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))

# .depend:
# 	$(FSTAR) --dep full $(addsuffix .Test.fst, $(ALL)) > .depend

# include .depend

.PHONY: %.test $(FSTARTACLIB)
.PRECIOUS: %.ml

$(FSTARTACLIB):
	$(MAKE) -C $(FSTAR_HOME)/ulib install-fstar-tactics

%.test: %.fst %.ml
	$(FSTAR) $*.fst --load $*
	touch $@

%.sep.test: %.fst %.ml
	$(FSTAR) $*.Test.fst --load $*
	touch $@

%.ml: %.fst $(FSTARTACLIB)
	$(FSTAR) $*.fst --cache_checked_modules --codegen Plugin --extract $*
	touch $@

clean:
	rm -f *.test *.ml *.o *.cm[ix] *.cmxs<commit_msg>native_tactics: assume fstartaclib.cmxs already built<commit_after>FSTAR_HOME=../..
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)
FSTARTACLIB=$(FSTAR_HOME)/bin/fstar-tactics-lib/fstartaclib.cmxs

# Tests for which the native tactics used in module named Sample.Test.fst are
# declared in a corresponding module named Sample.fst
TAC_MODULES=Print\
    Split\
    BV\
    UnitTests\
    Bane\
    Canon\
    Simple\
    SimpleTactic\
    Evens\
    Embeddings\
    Plugins

# Tests for which the native tatics are declared and used in the same module
ALL=Apply\
    Arith\
    CanonDeep\
    Clear\
    Cut\
    DependentSynth\
    Fail\
    Imp\
    Logic\
    Nest\
    Pruning\
    Rename\
    Retype\
    Sequences\
    Simplifier\
    Tutorial\
    Unify

all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))

# .depend:
# 	$(FSTAR) --dep full $(addsuffix .Test.fst, $(ALL)) > .depend

# include .depend

.PHONY: %.test
.PRECIOUS: %.ml

%.test: %.fst %.ml
	$(FSTAR) $*.fst --load $*
	touch $@

%.sep.test: %.fst %.ml
	$(FSTAR) $*.Test.fst --load $*
	touch $@

%.ml: %.fst
	$(FSTAR) $*.fst --cache_checked_modules --codegen Plugin --extract $*
	touch $@

clean:
	rm -f *.test *.ml *.o *.cm[ix] *.cmxs
{'fraction_non_alphanumeric': 0.1573482428115016, 'fraction_numerical': 0.0, 'mean_word_length': 2.6147186147186146, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, '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': '4531734', 'n_tokens_mistral': 1025, 'n_tokens_neox': 978, 'n_words': 244}