<commit_before>FSTAR_HOME=..
include Makefile.include

# Note: native_tactics is not included in the list below, it is called
# explicitly by the uexamples rule from the Makefile in ../src/Makefile.
# These examples are excluded since the binary package can't verify
# them.

ALL_EXAMPLE_DIRS=\
bug-reports \
data_structures \
algorithms \
crypto \
termination \
software_foundations \
maths \
rel \
paradoxes \
printf \
metatheory \
verifythis \
preorders \
dm4free \
incl \
struct \
micro-benchmarks \
friends \
tactics \
typeclasses \
miniparse \
kv_parsing \
low-mitls-experiments \
seplogic \
csl \
hello \
extraction \
demos \
refinement \
indexed_effects \
doublylinkedlist \
regional \
generic \
calc \
layeredeffects

# low-level \  ... NS: removing from CI for this branch

all: $(addsuffix .all, $(ALL_EXAMPLE_DIRS))

%.all: %
	+$(MAKE) -C $^ all

test: all

stdlib: $(addprefix ../lib/, FStar.List.fst FStar.String.fsti partialmap.fst FStar.ST.fst)
	mkdir -p ../cache
	$(FSTAR) $^ --serialize_mods

clean:
	rm ../cache/*.cache

wc:
	find . -name "*.fst" | grep -v -e to_be_ported | xargs sloccount<commit_msg>disable layered effects tests temporarily<commit_after>FSTAR_HOME=..
include Makefile.include

# Note: native_tactics is not included in the list below, it is called
# explicitly by the uexamples rule from the Makefile in ../src/Makefile.
# These examples are excluded since the binary package can't verify
# them.

ALL_EXAMPLE_DIRS=\
bug-reports \
data_structures \
algorithms \
crypto \
termination \
software_foundations \
maths \
rel \
paradoxes \
printf \
metatheory \
verifythis \
preorders \
dm4free \
incl \
struct \
micro-benchmarks \
friends \
tactics \
typeclasses \
miniparse \
kv_parsing \
low-mitls-experiments \
seplogic \
csl \
hello \
extraction \
demos \
refinement \
indexed_effects \
doublylinkedlist \
regional \
generic \
calc

#layeredeffects

# low-level \  ... NS: removing from CI for this branch

all: $(addsuffix .all, $(ALL_EXAMPLE_DIRS))

%.all: %
	+$(MAKE) -C $^ all

test: all

stdlib: $(addprefix ../lib/, FStar.List.fst FStar.String.fsti partialmap.fst FStar.ST.fst)
	mkdir -p ../cache
	$(FSTAR) $^ --serialize_mods

clean:
	rm ../cache/*.cache

wc:
	find . -name "*.fst" | grep -v -e to_be_ported | xargs sloccount
{'fraction_non_alphanumeric': 0.1171806167400881, 'fraction_numerical': 0.000881057268722467, 'mean_word_length': 3.3505747126436782, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, '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': '2176973', 'n_tokens_mistral': 867, 'n_tokens_neox': 811, 'n_words': 233}