<commit_before>#######################################################################
#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
# <O___,, #     INRIA-Rocquencourt  &  CNRS-Universite Paris Diderot  #
#   \VV/  #############################################################
#    //   #      This file is distributed under the terms of the      #
#         #       GNU Lesser General Public License Version 2.1       #
#######################################################################

# This is a standalone Makefile to run the test-suite. It can be used
# outside of the Coq source tree (if BIN is overridden).

# There is one %.v.log target per %.v test file. The target will be
# filled with the output, timings and status of the test. There is
# also one target per directory containing %.v files, that runs all
# the tests in it. As convenience, there is also the "bugs" target
# that runs all bug-related tests.

# The "summary" target outputs a summary of all tests that were run
# (but doesn't run them)

# The "run" target runs all tests that have not been run yet. To force
# all tests to be run, use the "clean" target.

#######################################################################
# Variables
#######################################################################

# Default value when called from a freshly compiled Coq, but can be
# easily overridden
BIN := ../bin/
LIB := ..

ifeq ($(BEST),byte)
  coqtop := $(BIN)coqtop.byte -boot -q -batch -I prerequisite
  bincoqc := $(BIN)coqc -coqlib $(LIB) -byte -I prerequisite
else
  coqtop := $(BIN)coqtop -boot -q -batch -I prerequisite
  bincoqc := $(BIN)coqc -coqlib $(LIB) -I prerequisite
endif

command := $(coqtop) -top Top -load-vernac-source
coqc := $(coqtop) -compile
coqdep := $(BIN)coqdep

SHOW := $(if $(VERBOSE),@true,@echo)
HIDE := $(if $(VERBOSE),,@)
REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)

ifneq (,$(wildcard /proc/cpuinfo))
  sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
  sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc
  sedbogo += -e "s/BogoMIPS.*: \([0-9]*\).*/\1/p" # alpha
  bogomips := $(shell sed -n $(sedbogo) /proc/cpuinfo | head -1)
endif

ifeq (,$(bogomips))
  $(warning cannot run complexity tests (no bogomips found))
endif

log_success = "==========> SUCCESS <=========="
log_failure = "==========> FAILURE <=========="
log_intro = "==========> TESTING $(1) <=========="

#######################################################################
# Testing subsystems
#######################################################################

# Apart so that it can be easily skipped with overriding
COMPLEXITY := $(if $(bogomips),complexity)

BUGS := bugs/opened/shouldnotfail bugs/opened/shouldnotsucceed \<commit_msg>Fix missing -coqlib argument to coqdep in test-suite<commit_after>#######################################################################
#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
# <O___,, #     INRIA-Rocquencourt  &  CNRS-Universite Paris Diderot  #
#   \VV/  #############################################################
#    //   #      This file is distributed under the terms of the      #
#         #       GNU Lesser General Public License Version 2.1       #
#######################################################################

# This is a standalone Makefile to run the test-suite. It can be used
# outside of the Coq source tree (if BIN is overridden).

# There is one %.v.log target per %.v test file. The target will be
# filled with the output, timings and status of the test. There is
# also one target per directory containing %.v files, that runs all
# the tests in it. As convenience, there is also the "bugs" target
# that runs all bug-related tests.

# The "summary" target outputs a summary of all tests that were run
# (but doesn't run them)

# The "run" target runs all tests that have not been run yet. To force
# all tests to be run, use the "clean" target.

#######################################################################
# Variables
#######################################################################

# Default value when called from a freshly compiled Coq, but can be
# easily overridden
BIN := ../bin/
LIB := ..

ifeq ($(BEST),byte)
  coqtop := $(BIN)coqtop.byte -boot -q -batch -I prerequisite
  bincoqc := $(BIN)coqc -coqlib $(LIB) -byte -I prerequisite
else
  coqtop := $(BIN)coqtop -boot -q -batch -I prerequisite
  bincoqc := $(BIN)coqc -coqlib $(LIB) -I prerequisite
endif

command := $(coqtop) -top Top -load-vernac-source
coqc := $(coqtop) -compile
coqdep := $(BIN)coqdep -coqlib $(LIB)

SHOW := $(if $(VERBOSE),@true,@echo)
HIDE := $(if $(VERBOSE),,@)
REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)

ifneq (,$(wildcard /proc/cpuinfo))
  sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
  sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc
  sedbogo += -e "s/BogoMIPS.*: \([0-9]*\).*/\1/p" # alpha
  bogomips := $(shell sed -n $(sedbogo) /proc/cpuinfo | head -1)
endif

ifeq (,$(bogomips))
  $(warning cannot run complexity tests (no bogomips found))
endif

log_success = "==========> SUCCESS <=========="
log_failure = "==========> FAILURE <=========="
log_intro = "==========> TESTING $(1) <=========="

#######################################################################
# Testing subsystems
#######################################################################

# Apart so that it can be easily skipped with overriding
COMPLEXITY := $(if $(bogomips),complexity)

BUGS := bugs/opened/shouldnotfail bugs/opened/shouldnotsucceed \
{'fraction_non_alphanumeric': 0.31314570716066975, 'fraction_numerical': 0.006768792304951906, 'mean_word_length': 4.21355617455896, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5589103', 'n_tokens_mistral': 1798, 'n_tokens_neox': 1666, 'n_words': 573}