<commit_before>SHELL    :=/bin/bash
PWD      :=$(realpath .)
SRC_DIR  =src
TEST_DIR =test

ATHENA   =athena
AGDA     =agda

.PHONY : default
default: install

# -----------------------------------------------------------------------------
# Naive way to alert the user about the Agda version or GHC version.
# -----------------------------------------------------------------------------

AGDA_VERSION := $(shell agda --version 2>/dev/null)
TESTED_AGDA_VERSION1 =Agda version 2.5.3

agdaversion:

ifneq ($(AGDA_VERSION),$(TESTED_AGDA_VERSION1))
	@echo "==================================================================="
	@echo "===================  WARNING: AGDA VERSION! ======================="
	@echo "==================================================================="
	@echo "[!] ATHENA was tested with:"
	@echo "    * ${TESTED_AGDA_VERSION1}"
	@echo "    Your system has a different version:"
	@echo "    * ${AGDA_VERSION}"
endif

GHC_VERSION := $(shell ghc --version 2>/dev/null)
TESTED_GHC_VERSION1 :=The Glorious Glasgow Haskell Compilation System, version 8.0.2
TESTED_GHC_VERSION2 :=The Glorious Glasgow Haskell Compilation System, version 8.2.1

ghcversion:

ifneq ($(GHC_VERSION),$(TESTED_GHC_VERSION1))
ifneq ($(GHC_VERSION),$(TESTED_GHC_VERSION2))
	@echo "==================================================================="
	@echo "====================  WARNING: GHC VERSION! ======================="
	@echo "==================================================================="
	@echo "[!] ATHENA was tested with:"
	@echo "    * ${TESTED_GHC_VERSION1}"
	@echo "    * ${TESTED_GHC_VERSION2}"
	@echo "    Your system has a different version:"
	@echo "    * ${GHC_VERSION}"
endif
endif

# -----------------------------------------------------------------------------
# Targets and variables to generate test problems and type-checking.
# -----------------------------------------------------------------------------

ATP             ?=online-atps --atp=metis
ATHENA_LIB      =$(addprefix $(PWD), /lib)
ATHENA_AGDA_LIB =$(addprefix $(ATHENA_LIB),/.agda)

TIME_BIN        := $(shell which time)
TIMELIMIT       =timeout 10m
# timelimit -T60 -t60 -S9
SEP='-------------------------------------------------------------------'


ifdef MSVC     # Avoid the MingW/Cygwin sections
		uname_S := Windows
else                          # If uname not available => 'not'
		uname_S := $(shell sh -c 'uname -s 2>/dev/null || echo not')
endif

# https://stackoverflow.com/questions/3466166/how-to-check-if-running-in-cygwin-mac-or-linux

ifeq ($(uname_S),OSF1)
		TIMELIMIT =timelimit -T60 -t60 -S9
		TIME_BIN  := $(shell which gtime) # install gnu-time
endif
ifeq ($(uname_S),Darwin)
		TIMELIMIT =timelimit -T60 -t60 -S9
		TIME_BIN  := $(shell which gtime)
endif
ifeq ($(uname_S),Linux)
		TIMELIMIT =timeout 10m
endif
ifeq ($(uname_S),GNU/kFreeBSD)
		TIMELIMIT =timelimit -T60 -t60 -S9
		TIME_BIN  := $(shell which gtime)
endif
ifeq ($(uname_S),UnixWare)
		TIMELIMIT =timeout 10m
endif


# ============================================================================
# Propositional problems in TPTP format from
# http://github.com/jonaprieto/prop-pack

PROP_PACK =test/prop-pack
PROBLEMS  =$(addprefix $(PROP_PACK),/problems)

BASIC     =$(addprefix $(PROBLEMS),/basic)
CONJ      =$(addprefix $(PROBLEMS),/conjunction)
DISJ      =$(addprefix $(PROBLEMS),/disjunction)
IMPL      =$(addprefix $(PROBLEMS),/implication)
NEG       =$(addprefix $(PROBLEMS),/negation)
PMETIS    =$(addprefix $(PROBLEMS),/prop-metis)

TPTP_BASIC := $(wildcard $(BASIC)/*.tptp)
TSTP_BASIC := $(addprefix $(BASIC)/,$(notdir $(TPTP_BASIC:.tptp=.tstp)))
AGDA_BASIC := $(addprefix $(BASIC)/,$(notdir $(TSTP_BASIC:.tstp=.agda)))

TPTP_CONJ := $(wildcard $(CONJ)/*.tptp)
TSTP_CONJ := $(addprefix $(CONJ)/,$(notdir $(TPTP_CONJ:.tptp=.tstp)))
AGDA_CONJ := $(addprefix $(CONJ)/,$(notdir $(TSTP_CONJ:.tstp=.agda)))

TPTP_DISJ := $(wildcard $(DISJ)/*.tptp)
TSTP_DISJ := $(addprefix $(DISJ)/,$(notdir $(TPTP_DISJ:.tptp=.tstp)))
AGDA_DISJ := $(addprefix $(DISJ)/,$(notdir $(TSTP_DISJ:.tstp=.agda)))

TPTP_IMPL := $(wildcard $(IMPL)/*.tptp)<commit_msg>[ Makefile ] 180min for type-checking.<commit_after>SHELL    :=/bin/bash
PWD      :=$(realpath .)
SRC_DIR  =src
TEST_DIR =test

ATHENA   =athena
AGDA     =agda

.PHONY : default
default: install

# -----------------------------------------------------------------------------
# Naive way to alert the user about the Agda version or GHC version.
# -----------------------------------------------------------------------------

AGDA_VERSION := $(shell agda --version 2>/dev/null)
TESTED_AGDA_VERSION1 =Agda version 2.5.3

agdaversion:

ifneq ($(AGDA_VERSION),$(TESTED_AGDA_VERSION1))
	@echo "==================================================================="
	@echo "===================  WARNING: AGDA VERSION! ======================="
	@echo "==================================================================="
	@echo "[!] ATHENA was tested with:"
	@echo "    * ${TESTED_AGDA_VERSION1}"
	@echo "    Your system has a different version:"
	@echo "    * ${AGDA_VERSION}"
endif

GHC_VERSION := $(shell ghc --version 2>/dev/null)
TESTED_GHC_VERSION1 :=The Glorious Glasgow Haskell Compilation System, version 8.0.2
TESTED_GHC_VERSION2 :=The Glorious Glasgow Haskell Compilation System, version 8.2.1

ghcversion:

ifneq ($(GHC_VERSION),$(TESTED_GHC_VERSION1))
ifneq ($(GHC_VERSION),$(TESTED_GHC_VERSION2))
	@echo "==================================================================="
	@echo "====================  WARNING: GHC VERSION! ======================="
	@echo "==================================================================="
	@echo "[!] ATHENA was tested with:"
	@echo "    * ${TESTED_GHC_VERSION1}"
	@echo "    * ${TESTED_GHC_VERSION2}"
	@echo "    Your system has a different version:"
	@echo "    * ${GHC_VERSION}"
endif
endif

# -----------------------------------------------------------------------------
# Targets and variables to generate test problems and type-checking.
# -----------------------------------------------------------------------------

ATP             ?=online-atps --atp=metis
ATHENA_LIB      =$(addprefix $(PWD), /lib)
ATHENA_AGDA_LIB =$(addprefix $(ATHENA_LIB),/.agda)

TIME_BIN        := $(shell which time)
TIMELIMIT       =timeout 10m
# timelimit -T60 -t60 -S9
SEP='-------------------------------------------------------------------'


ifdef MSVC     # Avoid the MingW/Cygwin sections
		uname_S := Windows
else                          # If uname not available => 'not'
		uname_S := $(shell sh -c 'uname -s 2>/dev/null || echo not')
endif

# https://stackoverflow.com/questions/3466166/how-to-check-if-running-in-cygwin-mac-or-linux

ifeq ($(uname_S),OSF1)
		TIMELIMIT =timelimit -T60 -t60 -S9
		TIME_BIN  := $(shell which gtime) # install gnu-time
endif
ifeq ($(uname_S),Darwin)
		TIMELIMIT =timelimit -T60 -t60 -S9
		TIME_BIN  := $(shell which gtime)
endif
ifeq ($(uname_S),Linux)
		TIMELIMIT =timeout 180m
endif
ifeq ($(uname_S),GNU/kFreeBSD)
		TIMELIMIT =timelimit -T60 -t60 -S9
		TIME_BIN  := $(shell which gtime)
endif
ifeq ($(uname_S),UnixWare)
		TIMELIMIT =timeout 180m
endif


# ============================================================================
# Propositional problems in TPTP format from
# http://github.com/jonaprieto/prop-pack

PROP_PACK =test/prop-pack
PROBLEMS  =$(addprefix $(PROP_PACK),/problems)

BASIC     =$(addprefix $(PROBLEMS),/basic)
CONJ      =$(addprefix $(PROBLEMS),/conjunction)
DISJ      =$(addprefix $(PROBLEMS),/disjunction)
IMPL      =$(addprefix $(PROBLEMS),/implication)
NEG       =$(addprefix $(PROBLEMS),/negation)
PMETIS    =$(addprefix $(PROBLEMS),/prop-metis)

TPTP_BASIC := $(wildcard $(BASIC)/*.tptp)
TSTP_BASIC := $(addprefix $(BASIC)/,$(notdir $(TPTP_BASIC:.tptp=.tstp)))
AGDA_BASIC := $(addprefix $(BASIC)/,$(notdir $(TSTP_BASIC:.tstp=.agda)))

TPTP_CONJ := $(wildcard $(CONJ)/*.tptp)
TSTP_CONJ := $(addprefix $(CONJ)/,$(notdir $(TPTP_CONJ:.tptp=.tstp)))
AGDA_CONJ := $(addprefix $(CONJ)/,$(notdir $(TSTP_CONJ:.tstp=.agda)))

TPTP_DISJ := $(wildcard $(DISJ)/*.tptp)
TSTP_DISJ := $(addprefix $(DISJ)/,$(notdir $(TPTP_DISJ:.tptp=.tstp)))
AGDA_DISJ := $(addprefix $(DISJ)/,$(notdir $(TSTP_DISJ:.tstp=.agda)))

TPTP_IMPL := $(wildcard $(IMPL)/*.tptp)
{'fraction_non_alphanumeric': 0.3286908077994429, 'fraction_numerical': 0.013927576601671309, 'mean_word_length': 3.040117416829746, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 2, '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': '4161816', 'n_tokens_mistral': 2932, 'n_tokens_neox': 2711, 'n_words': 583}