Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/dev/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 1 kB image not shown  

Quelle  lint-repository.sh   Sprache: Shell

 
#!/usr/bin/env bash

# A script to check prettyness over the repository.

# lint-commits.sh seeks to prevent the worsening of already present
# problems, such as tab indentation in ml files. lint-repository.sh
# also seeks to prevent the (re-)introduction of solved problems, such
# as newlines at the end of .v files.

CODE=0

# if COQ_CI_COLOR is set (from the environment) keep it intact (even when it's the empty string)'
if ! [ "${COQ_CI_COLOR+1}" ]; then
  # NB: in CI TERM is unset in the environment
  # when TERM is unset, bash sets it to "dumb" as a bash variable (not exported?)
  if { [ -t 1 ] && ! [ "$TERM" = dumb ]; } || [ "$CI" ]
  then export COQ_CI_COLOR=1
  else export COQ_CI_COLOR=
  fi
fi

if [[ $(git log -n 1 --pretty='format:%s') == "[CI merge]"* ]]; then
    # The second parent of bot merges is from the PR, the first is
    # current master
    head=$(git rev-parse HEAD^2)
else
    head=$(git rev-parse HEAD)
fi

# We assume that all non-bot merge commits are from the main branch
# For Rocq it is extremely rare for this assumption to be broken
read -r base < <(git log -n 1 --merges --pretty='format:%H' "$head")

dev/lint-commits.sh "$base" "$head" || CODE=1

# Check that the files with 'whitespace' gitattribute end in a newline.
# xargs exit status is 123 if any file failed the test
echo Checking end of file newlines
find . "(" -path ./.git -prune ")" -o -type f -print0 |
    xargs -0 dev/tools/check-eof-newline.sh || CODE=1

echo Checking overlays
dev/tools/check-overlays.sh || CODE=1

echo Checking CACHEKEY
dev/tools/check-cachekey.sh || CODE=1

# Check that doc/tools/docgram/fullGrammar is up-to-date
echo Checking grammar files
make SHOW='@true ""' doc_gram_verify || CODE=1

exit $CODE

100%


¤ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.