<commit_before>.PHONY: all

FSTAR_HOME=..

# Makefile.verify has been split off because it is the actual
# Makefile that is distributed in the binary package. This
# Makefile here is not.

all: .cache
	+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-core

benchmark: .cache
	+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-benchmark

extra: .cache
	+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-extra

.cache:
	mkdir -p .cache

include $(FSTAR_HOME)/ulib/ml/Makefile.include
include $(FSTAR_HOME)/.common.mk

fstarlib.mgen: *.fst *.fsti
	mkdir -p ml/extracted
	rm -f .depend.extract
	+OUTPUT_DIRECTORY=ml/extracted \
	    EXTRACT_MODULES="--extract '-Prims +FStar +LowStar +Steel -FStar.Tactics -FStar.Reflection -Steel.Tactics $(NOEXTRACT_MODULES)'" \
	    $(MAKE) -f Makefile.extract all-ml
	# the next cp is done because FStar_Pervasives.ml is needed to bootstrap the compiler
	# we could follow this style for other files too, e.g., FStar_Option.ml
	cp ../src/ocaml-output/FStar_Pervasives.ml ml/extracted
	touch fstarlib.mgen

# NOTE: fstarlib_leftovers.ml takes directories that MUST NOT end with /
FSTARLIB_LEFTOVERS=$(shell ocaml fstarlib_leftovers.ml +ml +ml/extracted -../bin/fstar-compiler-lib)
fstartaclib.mgen: fstarlib.mgen
	mkdir -p tactics_ml/extracted
	rm -f .depend.extract
	+OUTPUT_DIRECTORY=tactics_ml/extracted \
	    CODEGEN=Plugin \
	    EXTRACT_MODULES="--extract '+FStar.Tactics +FStar.Reflection $(NOEXTRACT_MODULES)'" \
	    $(MAKE) -f Makefile.extract all-ml
	mkdir -p tactics_ml/fstarlib_leftovers
	cp $(FSTARLIB_LEFTOVERS) tactics_ml/fstarlib_leftovers
	touch fstartaclib.mgen

######################################################
# OCaml extraction of fstarlib and fstar-tactics-lib #
######################################################
<commit_msg>Update the Makefile<commit_after>.PHONY: all

FSTAR_HOME=..

# Makefile.verify has been split off because it is the actual
# Makefile that is distributed in the binary package. This
# Makefile here is not.

all: .cache
	+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-core

benchmark: .cache
	+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-benchmark

extra: .cache
	+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-extra

.cache:
	mkdir -p .cache

include $(FSTAR_HOME)/ulib/ml/Makefile.include
include $(FSTAR_HOME)/.common.mk

fstarlib.mgen: *.fst *.fsti
	mkdir -p ml/extracted
	rm -f .depend.extract
	+OUTPUT_DIRECTORY=ml/extracted \
	    EXTRACT_MODULES="--extract '-Prims +FStar +LowStar +Steel -FStar.Tactics -FStar.Reflection -Steel.Tactics -FStar.Interactive $(NOEXTRACT_MODULES)'" \
	    $(MAKE) -f Makefile.extract all-ml
	# the next cp is done because FStar_Pervasives.ml is needed to bootstrap the compiler
	# we could follow this style for other files too, e.g., FStar_Option.ml
	cp ../src/ocaml-output/FStar_Pervasives.ml ml/extracted
	touch fstarlib.mgen

# NOTE: fstarlib_leftovers.ml takes directories that MUST NOT end with /
FSTARLIB_LEFTOVERS=$(shell ocaml fstarlib_leftovers.ml +ml +ml/extracted -../bin/fstar-compiler-lib)
fstartaclib.mgen: fstarlib.mgen
	mkdir -p tactics_ml/extracted
	rm -f .depend.extract
	+OUTPUT_DIRECTORY=tactics_ml/extracted \
	    CODEGEN=Plugin \
	    EXTRACT_MODULES="--extract '+FStar.Tactics +FStar.Reflection $(NOEXTRACT_MODULES) +FStar.Interactive'" \
	    $(MAKE) -f Makefile.extract all-ml
	mkdir -p tactics_ml/fstarlib_leftovers
	cp $(FSTARLIB_LEFTOVERS) tactics_ml/fstarlib_leftovers
	touch fstartaclib.mgen

######################################################
# OCaml extraction of fstarlib and fstar-tactics-lib #
######################################################

{'fraction_non_alphanumeric': 0.16476964769647698, 'fraction_numerical': 0.0, 'mean_word_length': 4.678461538461539, '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': '2169597', 'n_tokens_mistral': 1398, 'n_tokens_neox': 1287, 'n_words': 312}