From 0bf66c1cb19c8f9bb00db32cac04540ce64f34af Mon Sep 17 00:00:00 2001 From: "David A. Wheeler" Date: Wed, 7 Jun 2023 12:50:00 -0400 Subject: [PATCH] Add spellcheck workflow Signed-off-by: David A. Wheeler --- .github/actions/spelling/README.md | 17 + .github/actions/spelling/advice.md | 31 + .github/actions/spelling/allow.txt | 5 + .github/actions/spelling/candidate.patterns | 575 ++++++++++++++++++ .github/actions/spelling/excludes.txt | 85 +++ .github/actions/spelling/expect.txt | 9 + .../actions/spelling/line_forbidden.patterns | 88 +++ .github/actions/spelling/patterns.txt | 46 ++ .github/actions/spelling/reject.txt | 11 + .github/workflows/spelling.yml | 141 +++++ docs/index.md | 83 +-- 11 files changed, 1050 insertions(+), 41 deletions(-) create mode 100644 .github/actions/spelling/README.md create mode 100644 .github/actions/spelling/advice.md create mode 100644 .github/actions/spelling/allow.txt create mode 100644 .github/actions/spelling/candidate.patterns create mode 100644 .github/actions/spelling/excludes.txt create mode 100644 .github/actions/spelling/expect.txt create mode 100644 .github/actions/spelling/line_forbidden.patterns create mode 100644 .github/actions/spelling/patterns.txt create mode 100644 .github/actions/spelling/reject.txt create mode 100644 .github/workflows/spelling.yml diff --git a/.github/actions/spelling/README.md b/.github/actions/spelling/README.md new file mode 100644 index 00000000..1f699f3d --- /dev/null +++ b/.github/actions/spelling/README.md @@ -0,0 +1,17 @@ +# check-spelling/check-spelling configuration + +File | Purpose | Format | Info +-|-|-|- +[dictionary.txt](dictionary.txt) | Replacement dictionary (creating this file will override the default dictionary) | one word per line | [dictionary](https://github.com/check-spelling/check-spelling/wiki/Configuration#dictionary) +[allow.txt](allow.txt) | Add words to the dictionary | one word per line (only letters and `'`s allowed) | [allow](https://github.com/check-spelling/check-spelling/wiki/Configuration#allow) +[reject.txt](reject.txt) | Remove words from the dictionary (after allow) | grep pattern matching whole dictionary words | [reject](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-reject) +[excludes.txt](excludes.txt) | Files to ignore entirely | perl regular expression | [excludes](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-excludes) +[only.txt](only.txt) | Only check matching files (applied after excludes) | perl regular expression | [only](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-only) +[patterns.txt](patterns.txt) | Patterns to ignore from checked lines | perl regular expression (order matters, first match wins) | [patterns](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-patterns) +[candidate.patterns](candidate.patterns) | Patterns that might be worth adding to [patterns.txt](patterns.txt) | perl regular expression with optional comment block introductions (all matches will be suggested) | [candidates](https://github.com/check-spelling/check-spelling/wiki/Feature:-Suggest-patterns) +[line_forbidden.patterns](line_forbidden.patterns) | Patterns to flag in checked lines | perl regular expression (order matters, first match wins) | [patterns](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-patterns) +[expect.txt](expect.txt) | Expected words that aren't in the dictionary | one word per line (sorted, alphabetically) | [expect](https://github.com/check-spelling/check-spelling/wiki/Configuration#expect) +[advice.md](advice.md) | Supplement for GitHub comment when unrecognized words are found | GitHub Markdown | [advice](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-advice) + +Note: you can replace any of these files with a directory by the same name (minus the suffix) +and then include multiple files inside that directory (with that suffix) to merge multiple files together. diff --git a/.github/actions/spelling/advice.md b/.github/actions/spelling/advice.md new file mode 100644 index 00000000..a32d1090 --- /dev/null +++ b/.github/actions/spelling/advice.md @@ -0,0 +1,31 @@ + +
If the flagged items are :exploding_head: false positives + +If items relate to a ... +* binary file (or some other file you wouldn't want to check at all). + + Please add a file path to the `excludes.txt` file matching the containing file. + + File paths are Perl 5 Regular Expressions - you can [test]( +https://www.regexplanet.com/advanced/perl/) yours before committing to verify it will match your files. + + `^` refers to the file's path from the root of the repository, so `^README\.md$` would exclude [README.md]( +../tree/HEAD/README.md) (on whichever branch you're using). + +* well-formed pattern. + + If you can write a [pattern]( +https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples:-patterns +) that would match it, + try adding it to the `patterns.txt` file. + + Patterns are Perl 5 Regular Expressions - you can [test]( +https://www.regexplanet.com/advanced/perl/) yours before committing to verify it will match your lines. + + Note that patterns can't match multiline strings. + +
+ + +:steam_locomotive: If you're seeing this message and your PR is from a branch that doesn't have check-spelling, +please merge to your PR's base branch to get the version configured for your repository. diff --git a/.github/actions/spelling/allow.txt b/.github/actions/spelling/allow.txt new file mode 100644 index 00000000..61567618 --- /dev/null +++ b/.github/actions/spelling/allow.txt @@ -0,0 +1,5 @@ +github +https +ssh +ubuntu +workarounds diff --git a/.github/actions/spelling/candidate.patterns b/.github/actions/spelling/candidate.patterns new file mode 100644 index 00000000..4b8c70f9 --- /dev/null +++ b/.github/actions/spelling/candidate.patterns @@ -0,0 +1,575 @@ +# marker to ignore all code on line +^.*/\* #no-spell-check-line \*/.*$ +# marker to ignore all code on line +^.*\bno-spell-check(?:-line|)(?:\s.*|)$ + +# https://cspell.org/configuration/document-settings/ +# cspell inline +^.*\b[Cc][Ss][Pp][Ee][Ll]{2}:\s*[Dd][Ii][Ss][Aa][Bb][Ll][Ee]-[Ll][Ii][Nn][Ee]\b + +# patch hunk comments +^\@\@ -\d+(?:,\d+|) \+\d+(?:,\d+|) \@\@ .* +# git index header +index (?:[0-9a-z]{7,40},|)[0-9a-z]{7,40}\.\.[0-9a-z]{7,40} + +# css url wrappings +\burl\([^)]*\) + +# cid urls +(['"])cid:.*?\g{-1} + +# data url in parens +\(data:(?:[^) ][^)]*?|)(?:[A-Z]{3,}|[A-Z][a-z]{2,}|[a-z]{3,})[^)]*\) +# data url in quotes +([`'"])data:(?:[^ `'"].*?|)(?:[A-Z]{3,}|[A-Z][a-z]{2,}|[a-z]{3,}).*\g{-1} +# data url +data:[-a-zA-Z=;:/0-9+]*,\S* + +# https/http/file urls +(?:\b(?:https?|ftp|file)://)[-A-Za-z0-9+&@#/%?=~_|!:,.;]+[-A-Za-z0-9+&@#/%=~_|] + +# mailto urls +mailto:[-a-zA-Z=;:/?%&0-9+@.]{3,} + +# magnet urls +magnet:[?=:\w]+ + +# magnet urls +"magnet:[^"]+" + +# obs: +"obs:[^"]*" + +# The `\b` here means a break, it's the fancy way to handle urls, but it makes things harder to read +# In this examples content, I'm using a number of different ways to match things to show various approaches +# asciinema +\basciinema\.org/a/[0-9a-zA-Z]+ + +# asciinema v2 +^\[\d+\.\d+, "[io]", ".*"\]$ + +# apple +\bdeveloper\.apple\.com/[-\w?=/]+ +# Apple music +\bembed\.music\.apple\.com/fr/playlist/usr-share/[-\w.]+ + +# appveyor api +\bci\.appveyor\.com/api/projects/status/[0-9a-z]+ +# appveyor project +\bci\.appveyor\.com/project/(?:[^/\s"]*/){2}builds?/\d+/job/[0-9a-z]+ + +# Amazon + +# Amazon +\bamazon\.com/[-\w]+/(?:dp/[0-9A-Z]+|) +# AWS S3 +\b\w*\.s3[^.]*\.amazonaws\.com/[-\w/&#%_?:=]* +# AWS execute-api +\b[0-9a-z]{10}\.execute-api\.[-0-9a-z]+\.amazonaws\.com\b +# AWS ELB +\b\w+\.[-0-9a-z]+\.elb\.amazonaws\.com\b +# AWS SNS +\bsns\.[-0-9a-z]+.amazonaws\.com/[-\w/&#%_?:=]* +# AWS VPC +vpc-\w+ + +# While you could try to match `http://` and `https://` by using `s?` in `https?://`, sometimes there +# YouTube url +\b(?:(?:www\.|)youtube\.com|youtu.be)/(?:channel/|embed/|user/|playlist\?list=|watch\?v=|v/|)[-a-zA-Z0-9?&=_%]* +# YouTube music +\bmusic\.youtube\.com/youtubei/v1/browse(?:[?&]\w+=[-a-zA-Z0-9?&=_]*) +# YouTube tag +<\s*youtube\s+id=['"][-a-zA-Z0-9?_]*['"] +# YouTube image +\bimg\.youtube\.com/vi/[-a-zA-Z0-9?&=_]* +# Google Accounts +\baccounts.google.com/[-_/?=.:;+%&0-9a-zA-Z]* +# Google Analytics +\bgoogle-analytics\.com/collect.[-0-9a-zA-Z?%=&_.~]* +# Google APIs +\bgoogleapis\.(?:com|dev)/[a-z]+/(?:v\d+/|)[a-z]+/[-@:./?=\w+|&]+ +# Google Storage +\b[-a-zA-Z0-9.]*\bstorage\d*\.googleapis\.com(?:/\S*|) +# Google Calendar +\bcalendar\.google\.com/calendar(?:/u/\d+|)/embed\?src=[@./?=\w&%]+ +\w+\@group\.calendar\.google\.com\b +# Google DataStudio +\bdatastudio\.google\.com/(?:(?:c/|)u/\d+/|)(?:embed/|)(?:open|reporting|datasources|s)/[-0-9a-zA-Z]+(?:/page/[-0-9a-zA-Z]+|) +# The leading `/` here is as opposed to the `\b` above +# ... a short way to match `https://` or `http://` since most urls have one of those prefixes +# Google Docs +/docs\.google\.com/[a-z]+/(?:ccc\?key=\w+|(?:u/\d+|d/(?:e/|)[0-9a-zA-Z_-]+/)?(?:edit\?[-\w=#.]*|/\?[\w=&]*|)) +# Google Drive +\bdrive\.google\.com/(?:file/d/|open)[-0-9a-zA-Z_?=]* +# Google Groups +\bgroups\.google\.com(?:/[a-z]+/(?:#!|)[^/\s"]+)* +# Google Maps +\bmaps\.google\.com/maps\?[\w&;=]* +# Google themes +themes\.googleusercontent\.com/static/fonts/[^/\s"]+/v\d+/[^.]+. +# Google CDN +\bclients2\.google(?:usercontent|)\.com[-0-9a-zA-Z/.]* +# Goo.gl +/goo\.gl/[a-zA-Z0-9]+ +# Google Chrome Store +\bchrome\.google\.com/webstore/detail/[-\w]*(?:/\w*|) +# Google Books +\bgoogle\.(?:\w{2,4})/books(?:/\w+)*\?[-\w\d=&#.]* +# Google Fonts +\bfonts\.(?:googleapis|gstatic)\.com/[-/?=:;+&0-9a-zA-Z]* +# Google Forms +\bforms\.gle/\w+ +# Google Scholar +\bscholar\.google\.com/citations\?user=[A-Za-z0-9_]+ +# Google Colab Research Drive +\bcolab\.research\.google\.com/drive/[-0-9a-zA-Z_?=]* + +# GitHub SHAs (api) +\bapi.github\.com/repos(?:/[^/\s"]+){3}/[0-9a-f]+\b +# GitHub SHAs (markdown) +(?:\[`?[0-9a-f]+`?\]\(https:/|)/(?:www\.|)github\.com(?:/[^/\s"]+){2,}(?:/[^/\s")]+)(?:[0-9a-f]+(?:[-0-9a-zA-Z/#.]*|)\b|) +# GitHub SHAs +\bgithub\.com(?:/[^/\s"]+){2}[@#][0-9a-f]+\b +# GitHub wiki +\bgithub\.com/(?:[^/]+/){2}wiki/(?:(?:[^/]+/|)_history|[^/]+(?:/_compare|)/[0-9a-f.]{40,})\b +# githubusercontent +/[-a-z0-9]+\.githubusercontent\.com/[-a-zA-Z0-9?&=_\/.]* +# githubassets +\bgithubassets.com/[0-9a-f]+(?:[-/\w.]+) +# gist github +\bgist\.github\.com/[^/\s"]+/[0-9a-f]+ +# git.io +\bgit\.io/[0-9a-zA-Z]+ +# GitHub JSON +"node_id": "[-a-zA-Z=;:/0-9+]*" +# Contributor +\[[^\]]+\]\(https://github\.com/[^/\s"]+\) +# GHSA +GHSA(?:-[0-9a-z]{4}){3} + +# GitLab commit +\bgitlab\.[^/\s"]*/\S+/\S+/commit/[0-9a-f]{7,16}#[0-9a-f]{40}\b +# GitLab merge requests +\bgitlab\.[^/\s"]*/\S+/\S+/-/merge_requests/\d+/diffs#[0-9a-f]{40}\b +# GitLab uploads +\bgitlab\.[^/\s"]*/uploads/[-a-zA-Z=;:/0-9+]* +# GitLab commits +\bgitlab\.[^/\s"]*/(?:[^/\s"]+/){2}commits?/[0-9a-f]+\b + +# binance +accounts\.binance\.com/[a-z/]*oauth/authorize\?[-0-9a-zA-Z&%]* + +# bitbucket diff +\bapi\.bitbucket\.org/\d+\.\d+/repositories/(?:[^/\s"]+/){2}diff(?:stat|)(?:/[^/\s"]+){2}:[0-9a-f]+ +# bitbucket repositories commits +\bapi\.bitbucket\.org/\d+\.\d+/repositories/(?:[^/\s"]+/){2}commits?/[0-9a-f]+ +# bitbucket commits +\bbitbucket\.org/(?:[^/\s"]+/){2}commits?/[0-9a-f]+ + +# bit.ly +\bbit\.ly/\w+ + +# bitrise +\bapp\.bitrise\.io/app/[0-9a-f]*/[\w.?=&]* + +# bootstrapcdn.com +\bbootstrapcdn\.com/[-./\w]+ + +# cdn.cloudflare.com +\bcdnjs\.cloudflare\.com/[./\w]+ + +# circleci +\bcircleci\.com/gh(?:/[^/\s"]+){1,5}.[a-z]+\?[-0-9a-zA-Z=&]+ + +# gitter +\bgitter\.im(?:/[^/\s"]+){2}\?at=[0-9a-f]+ + +# gravatar +\bgravatar\.com/avatar/[0-9a-f]+ + +# ibm +[a-z.]*ibm\.com/[-_#=:%!?~.\\/\d\w]* + +# imgur +\bimgur\.com/[^.]+ + +# Internet Archive +\barchive\.org/web/\d+/(?:[-\w.?,'/\\+&%$#_:]*) + +# discord +/discord(?:app\.com|\.gg)/(?:invite/)?[a-zA-Z0-9]{7,} + +# Disqus +\bdisqus\.com/[-\w/%.()!?&=_]* + +# medium link +\blink\.medium\.com/[a-zA-Z0-9]+ +# medium +\bmedium\.com/\@?[^/\s"]+/[-\w]+ + +# microsoft +\b(?:https?://|)(?:(?:download\.visualstudio|docs|msdn2?|research)\.microsoft|blogs\.msdn)\.com/[-_a-zA-Z0-9()=./%]* +# powerbi +\bapp\.powerbi\.com/reportEmbed/[^"' ]* +# vs devops +\bvisualstudio.com(?::443|)/[-\w/?=%&.]* +# microsoft store +\bmicrosoft\.com/store/apps/\w+ + +# mvnrepository.com +\bmvnrepository\.com/[-0-9a-z./]+ + +# now.sh +/[0-9a-z-.]+\.now\.sh\b + +# oracle +\bdocs\.oracle\.com/[-0-9a-zA-Z./_?#&=]* + +# chromatic.com +/\S+.chromatic.com\S*[")] + +# codacy +\bapi\.codacy\.com/project/badge/Grade/[0-9a-f]+ + +# compai +\bcompai\.pub/v1/png/[0-9a-f]+ + +# mailgun api +\.api\.mailgun\.net/v3/domains/[0-9a-z]+\.mailgun.org/messages/[0-9a-zA-Z=@]* +# mailgun +\b[0-9a-z]+.mailgun.org + +# /message-id/ +/message-id/[-\w@./%]+ + +# Reddit +\breddit\.com/r/[/\w_]* + +# requestb.in +\brequestb\.in/[0-9a-z]+ + +# sched +\b[a-z0-9]+\.sched\.com\b + +# Slack url +slack://[a-zA-Z0-9?&=]+ +# Slack +\bslack\.com/[-0-9a-zA-Z/_~?&=.]* +# Slack edge +\bslack-edge\.com/[-a-zA-Z0-9?&=%./]+ +# Slack images +\bslack-imgs\.com/[-a-zA-Z0-9?&=%.]+ + +# shields.io +\bshields\.io/[-\w/%?=&.:+;,]* + +# stackexchange -- https://stackexchange.com/feeds/sites +\b(?:askubuntu|serverfault|stack(?:exchange|overflow)|superuser).com/(?:questions/\w+/[-\w]+|a/) + +# Sentry +[0-9a-f]{32}\@o\d+\.ingest\.sentry\.io\b + +# Twitter markdown +\[\@[^[/\]:]*?\]\(https://twitter.com/[^/\s"')]*(?:/status/\d+(?:\?[-_0-9a-zA-Z&=]*|)|)\) +# Twitter hashtag +\btwitter\.com/hashtag/[\w?_=&]* +# Twitter status +\btwitter\.com/[^/\s"')]*(?:/status/\d+(?:\?[-_0-9a-zA-Z&=]*|)|) +# Twitter profile images +\btwimg\.com/profile_images/[_\w./]* +# Twitter media +\btwimg\.com/media/[-_\w./?=]* +# Twitter link shortened +\bt\.co/\w+ + +# facebook +\bfburl\.com/[0-9a-z_]+ +# facebook CDN +\bfbcdn\.net/[\w/.,]* +# facebook watch +\bfb\.watch/[0-9A-Za-z]+ + +# dropbox +\bdropbox\.com/sh?/[^/\s"]+/[-0-9A-Za-z_.%?=&;]+ + +# ipfs protocol +ipfs://[0-9a-zA-Z]{3,} +# ipfs url +/ipfs/[0-9a-zA-Z]{3,} + +# w3 +\bw3\.org/[-0-9a-zA-Z/#.]+ + +# loom +\bloom\.com/embed/[0-9a-f]+ + +# regex101 +\bregex101\.com/r/[^/\s"]+/\d+ + +# figma +\bfigma\.com/file(?:/[0-9a-zA-Z]+/)+ + +# freecodecamp.org +\bfreecodecamp\.org/[-\w/.]+ + +# image.tmdb.org +\bimage\.tmdb\.org/[/\w.]+ + +# mermaid +\bmermaid\.ink/img/[-\w]+|\bmermaid-js\.github\.io/mermaid-live-editor/#/edit/[-\w]+ + +# Wikipedia +\ben\.wikipedia\.org/wiki/[-\w%.#]+ + +# gitweb +[^"\s]+/gitweb/\S+;h=[0-9a-f]+ + +# HyperKitty lists +/archives/list/[^@/]+\@[^/\s"]*/message/[^/\s"]*/ + +# lists +/thread\.html/[^"\s]+ + +# list-management +\blist-manage\.com/subscribe(?:[?&](?:u|id)=[0-9a-f]+)+ + +# kubectl.kubernetes.io/last-applied-configuration +"kubectl.kubernetes.io/last-applied-configuration": ".*" + +# pgp +\bgnupg\.net/pks/lookup[?&=0-9a-zA-Z]* + +# Spotify +\bopen\.spotify\.com/embed/playlist/\w+ + +# Mastodon +\bmastodon\.[-a-z.]*/(?:media/|\@)[?&=0-9a-zA-Z_]* + +# scastie +\bscastie\.scala-lang\.org/[^/]+/\w+ + +# images.unsplash.com +\bimages\.unsplash\.com/(?:(?:flagged|reserve)/|)[-\w./%?=%&.;]+ + +# pastebin +\bpastebin\.com/[\w/]+ + +# heroku +\b\w+\.heroku\.com/source/archive/\w+ + +# quip +\b\w+\.quip\.com/\w+(?:(?:#|/issues/)\w+)? + +# badgen.net +\bbadgen\.net/badge/[^")\]'\s]+ + +# statuspage.io +\w+\.statuspage\.io\b + +# media.giphy.com +\bmedia\.giphy\.com/media/[^/]+/[\w.?&=]+ + +# tinyurl +\btinyurl\.com/\w+ + +# codepen +\bcodepen\.io/[\w/]+ + +# registry.npmjs.org +\bregistry\.npmjs\.org/(?:@[^/"']+/|)[^/"']+/-/[-\w@.]+ + +# getopts +\bgetopts\s+(?:"[^"]+"|'[^']+') + +# ANSI color codes +(?:\\(?:u00|x)1[Bb]|\x1b|\\u\{1[Bb]\})\[\d+(?:;\d+|)m + +# URL escaped characters +\%[0-9A-F][A-F] +# IPv6 +\b(?:[0-9a-fA-F]{0,4}:){3,7}[0-9a-fA-F]{0,4}\b +# c99 hex digits (not the full format, just one I've seen) +0x[0-9a-fA-F](?:\.[0-9a-fA-F]*|)[pP] +# Punycode +\bxn--[-0-9a-z]+ +# sha +sha\d+:[0-9]*[a-f]{3,}[0-9a-f]* +# sha-... -- uses a fancy capture +(\\?['"]|")[0-9a-f]{40,}\g{-1} +# hex runs +\b[0-9a-fA-F]{16,}\b +# hex in url queries +=[0-9a-fA-F]*?(?:[A-F]{3,}|[a-f]{3,})[0-9a-fA-F]*?& +# ssh +(?:ssh-\S+|-nistp256) [-a-zA-Z=;:/0-9+]{12,} + +# PGP +\b(?:[0-9A-F]{4} ){9}[0-9A-F]{4}\b +# GPG keys +\b(?:[0-9A-F]{4} ){5}(?: [0-9A-F]{4}){5}\b +# Well known gpg keys +.well-known/openpgpkey/[\w./]+ + +# pki +-----BEGIN.*-----END + +# uuid: +\b[0-9a-fA-F]{8}-(?:[0-9a-fA-F]{4}-){3}[0-9a-fA-F]{12}\b +# hex digits including css/html color classes: +(?:[\\0][xX]|\\u|[uU]\+|#x?|\%23)[0-9_a-fA-FgGrR]*?[a-fA-FgGrR]{2,}[0-9_a-fA-FgGrR]*(?:[uUlL]{0,3}|[iu]\d+)\b +# integrity +integrity=(['"])sha\d+-[-a-zA-Z=;:/0-9+]{40,}\g{-1} + +# https://www.gnu.org/software/groff/manual/groff.html +# man troff content +\\f[BCIPR] +# '/" +\\\([ad]q + +# .desktop mime types +^MimeTypes?=.*$ +# .desktop localized entries +^[A-Z][a-z]+\[[a-z]+\]=.*$ +# Localized .desktop content +Name\[[^\]]+\]=.* + +# IServiceProvider +\bI(?=(?:[A-Z][a-z]{2,})+\b) + +# crypt +(['"])\$2[ayb]\$.{56}\g{-1} + +# scrypt / argon +\$(?:scrypt|argon\d+[di]*)\$\S+ + +# Input to GitHub JSON +content: (['"])[-a-zA-Z=;:/0-9+]*=\g{-1} + +# This does not cover multiline strings, if your repository has them, +# you'll want to remove the `(?=.*?")` suffix. +# The `(?=.*?")` suffix should limit the false positives rate +# printf +%(?:(?:(?:hh?|ll?|[jzt])?[diuoxn]|l?[cs]|L?[fega]|p)(?=[a-z]{2,})|(?:X|L?[FEGA]|p)(?=[a-zA-Z]{2,}))(?=[_a-zA-Z]+\b)(?!%)(?=.*?['"]) + +# Python string prefix / binary prefix +# Note that there's a high false positive rate, remove the `?=` and search for the regex to see if the matches seem like reasonable strings +(?v# +(?:(?<=[A-Z]{2})V|(?<=[a-z]{2}|[A-Z]{2})v)\d+(?:\b|(?=[a-zA-Z_])) +# Compiler flags (Scala) +(?:^|[\t ,>"'`=(])-J-[DPWXY](?=[A-Z]{2,}|[A-Z][a-z]|[a-z]{2,}) +# Compiler flags +(?:^|[\t ,>"'`=(])-[DPWXYLlf](?=[A-Z]{2,}|[A-Z][a-z]|[a-z]{2,}) +# Compiler flags (linker) +,-B +# curl arguments +\b(?:\\n|)curl(?:\s+-[a-zA-Z]{1,2}\b)*(?:\s+-[a-zA-Z]{3,})(?:\s+-[a-zA-Z]+)* +# set arguments +\bset(?:\s+-[abefimouxE]{1,2})*\s+-[abefimouxE]{3,}(?:\s+-[abefimouxE]+)* +# tar arguments +\b(?:\\n|)g?tar(?:\.exe|)(?:(?:\s+--[-a-zA-Z]+|\s+-[a-zA-Z]+|\s[ABGJMOPRSUWZacdfh-pr-xz]+\b)(?:=[^ ]*|))+ +# tput arguments -- https://man7.org/linux/man-pages/man5/terminfo.5.html -- technically they can be more than 5 chars long... +\btput\s+(?:(?:-[SV]|-T\s*\w+)\s+)*\w{3,5}\b +# macOS temp folders +/var/folders/\w\w/[+\w]+/(?:T|-Caches-)/ diff --git a/.github/actions/spelling/excludes.txt b/.github/actions/spelling/excludes.txt new file mode 100644 index 00000000..552d4464 --- /dev/null +++ b/.github/actions/spelling/excludes.txt @@ -0,0 +1,85 @@ +# See https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples:-excludes +(?:^|/)(?i)COPYRIGHT +(?:^|/)(?i)LICEN[CS]E +(?:^|/)3rdparty/ +(?:^|/)go\.sum$ +(?:^|/)package(?:-lock|)\.json$ +(?:^|/)Pipfile$ +(?:^|/)pyproject.toml +(?:^|/)requirements(?:-dev|-doc|-test|)\.txt$ +(?:^|/)vendor/ +\.a$ +\.ai$ +\.all-contributorsrc$ +\.avi$ +\.bmp$ +\.bz2$ +\.cer$ +\.class$ +\.coveragerc$ +\.crl$ +\.crt$ +\.csr$ +\.dll$ +\.docx?$ +\.drawio$ +\.DS_Store$ +\.eot$ +\.eps$ +\.exe$ +\.gif$ +\.git-blame-ignore-revs$ +\.gitattributes$ +\.gitkeep$ +\.graffle$ +\.gz$ +\.icns$ +\.ico$ +\.ipynb$ +\.jar$ +\.jks$ +\.jpe?g$ +\.key$ +\.lib$ +\.lock$ +\.map$ +\.min\.. +\.mo$ +\.mod$ +\.mp[34]$ +\.o$ +\.ocf$ +\.otf$ +\.p12$ +\.parquet$ +\.pdf$ +\.pem$ +\.pfx$ +\.png$ +\.psd$ +\.pyc$ +\.pylintrc$ +\.qm$ +\.s$ +\.sig$ +\.so$ +\.svgz?$ +\.sys$ +\.tar$ +\.tgz$ +\.tiff?$ +\.ttf$ +\.wav$ +\.webm$ +\.webp$ +\.woff2?$ +\.xcf$ +\.xlsx?$ +\.xpm$ +\.xz$ +\.zip$ +^\.github/actions/spelling/ +^\Q.github/workflows/spelling.yml\E$ +^\Qcharters/README.md\E$ +^\Qprocess/project-lifecycle-documents/.keep\E$ +ignore$ diff --git a/.github/actions/spelling/expect.txt b/.github/actions/spelling/expect.txt new file mode 100644 index 00000000..a5d1ab58 --- /dev/null +++ b/.github/actions/spelling/expect.txt @@ -0,0 +1,9 @@ +aspirational +backported +blogging +CEOs +curating +Debian +hyperlinks +Mozilla +Unicode diff --git a/.github/actions/spelling/line_forbidden.patterns b/.github/actions/spelling/line_forbidden.patterns new file mode 100644 index 00000000..6a8dfc55 --- /dev/null +++ b/.github/actions/spelling/line_forbidden.patterns @@ -0,0 +1,88 @@ +# If you have a framework that uses `it()` for testing and `fit()` for debugging a specific test, +# you might not want to check in code where you were debugging w/ `fit()`, in which case, you might want +# to use this: +#\bfit\( + +# s.b. GitHub +(?]*>|[^<]*)\s*$ + +# Autogenerated revert commit message +^This reverts commit [0-9a-f]{40}\.$ + +# ignore long runs of a single character: +\b([A-Za-z])\g{-1}{3,}\b diff --git a/.github/actions/spelling/reject.txt b/.github/actions/spelling/reject.txt new file mode 100644 index 00000000..e5e4c3ee --- /dev/null +++ b/.github/actions/spelling/reject.txt @@ -0,0 +1,11 @@ +^attache$ +^bellow$ +benefitting +occurences? +^dependan.* +^oer$ +Sorce +^[Ss]pae.* +^untill$ +^untilling$ +^wether.* diff --git a/.github/workflows/spelling.yml b/.github/workflows/spelling.yml new file mode 100644 index 00000000..d1af81f5 --- /dev/null +++ b/.github/workflows/spelling.yml @@ -0,0 +1,141 @@ +name: Check Spelling + +# See: https://github.com/check-spelling/check-spelling + +# Comment management is handled through a secondary job, for details see: +# https://github.com/check-spelling/check-spelling/wiki/Feature%3A-Restricted-Permissions +# +# `jobs.comment-push` runs when a push is made to a repository and the `jobs.spelling` job needs to make a comment +# (in odd cases, it might actually run just to collapse a comment, but that's fairly rare) +# it needs `contents: write` in order to add a comment. +# +# `jobs.comment-pr` runs when a pull_request is made to a repository and the `jobs.spelling` job needs to make a comment +# or collapse a comment (in the case where it had previously made a comment and now no longer needs to show a comment) +# it needs `pull-requests: write` in order to manipulate those comments. + +# Updating pull request branches is managed via comment handling. +# For details, see: https://github.com/check-spelling/check-spelling/wiki/Feature:-Update-expect-list +# +# These elements work together to make it happen: +# +# `on.issue_comment` +# This event listens to comments by users asking to update the metadata. +# +# `jobs.update` +# This job runs in response to an issue_comment and will push a new commit +# to update the spelling metadata. +# +# `with.experimental_apply_changes_via_bot` +# Tells the action to support and generate messages that enable it +# to make a commit to update the spelling metadata. +# +# `with.ssh_key` +# In order to trigger workflows when the commit is made, you can provide a +# secret (typically, a write-enabled github deploy key). +# +# For background, see: https://github.com/check-spelling/check-spelling/wiki/Feature:-Update-with-deploy-key + +# Sarif reporting +# +# Access to Sarif reports is generally restricted (by GitHub) to members of the repository. +# +# Requires enabling `security-events: write` +# and configuring the action with `use_sarif: 1` +# +# For information on the feature, see: https://github.com/check-spelling/check-spelling/wiki/Feature:-Sarif-output + +# Minimal workflow structure: +# +# on: +# push: +# ... +# pull_request_target: +# ... +# jobs: +# # you only want the spelling job, all others should be omitted +# spelling: +# # remove `security-events: write` and `use_sarif: 1` +# # remove `experimental_apply_changes_via_bot: 1` +# ... otherwise adjust the `with:` as you wish + +# Based on: +# https://github.com/ossf/tac/pull/174 + +on: + push: + branches: + - "**" + tags-ignore: + - "**" + pull_request_target: + branches: + - "**" + types: + - 'opened' + - 'reopened' + - 'synchronize' + issue_comment: + types: + - 'created' + +jobs: + spelling: + name: Check Spelling + permissions: + contents: read + pull-requests: read + actions: read + security-events: write + outputs: + followup: ${{ steps.spelling.outputs.followup }} + runs-on: ubuntu-latest + if: ${{ contains(github.event_name, 'pull_request') || github.event_name == 'push' }} + concurrency: + group: spelling-${{ github.event.pull_request.number || github.ref }} + # note: If you use only_check_changed_files, you do not want cancel-in-progress + cancel-in-progress: true + steps: + - name: check-spelling + id: spelling + uses: check-spelling/check-spelling@v0.0.21 + with: + suppress_push_for_open_pull_request: 1 + checkout: true + check_file_names: 1 + spell_check_this: ossf/tac@main + post_comment: 0 + use_magic_file: 1 + experimental_apply_changes_via_bot: ${{ github.repository_owner != 'ossf' && 1 }} + use_sarif: ${{ (!github.event.pull_request || (github.event.pull_request.head.repo.full_name == github.repository)) && 1 }} + extra_dictionary_limit: 10 + dictionary_source_prefixes: | + {"cspell": "https://raw.githubusercontent.com/check-spelling/cspell-dicts/v20220816/dictionaries/", "cspell1": "https://raw.githubusercontent.com/check-spelling/cspell-dicts/v20230509/dictionaries/"} + extra_dictionaries: + cspell1:software-terms/dict/softwareTerms.txt + cspell1:aws/aws.txt + cspell1:k8s/dict/k8s.txt + cspell1:filetypes/filetypes.txt + + update: + name: Update PR + permissions: + contents: write + pull-requests: write + actions: read + runs-on: ubuntu-latest + if: ${{ + github.repository_owner != 'ossf' && + github.event_name == 'issue_comment' && + github.event.issue.pull_request && + contains(github.event.comment.body, '@check-spelling-bot apply') + }} + concurrency: + group: spelling-update-${{ github.event.issue.number }} + cancel-in-progress: false + steps: + - name: apply spelling updates + uses: check-spelling/check-spelling@v0.0.21 + with: + experimental_apply_changes_via_bot: 1 + checkout: true + ssh_key: "${{ secrets.CHECK_SPELLING }}" diff --git a/docs/index.md b/docs/index.md index 9c8a5699..6c42bcb0 100644 --- a/docs/index.md +++ b/docs/index.md @@ -42,7 +42,7 @@ Note that metamath-lamp changes over time, so some of this guide may not exactly match what you see. If you see a difference, please let us know so we can fix this guide. We try to make this guide match the tool it's describing. -This guide was written for release version v10. +This guide was written for release version `v10`. You can get the latest version of this *Metamath-lamp guide* at <[https://lamp-guide.metamath.org/](https://lamp-guide.metamath.org/)>. @@ -60,7 +60,7 @@ To use metamath-lamp, do the following: 1. Load the proof context (the databases you'll use and their scope). 2. Set the fundamental proof information where desired (its description, variables, and disjoints). -3. Add the goal ("qed") and any hypotheses to the list of statements. +3. Add the goal (`qed`) and any hypotheses to the list of statements. Set their ids to what you want them to be in the final database. 4. Now create the proof. To do this, you add other statements and repeatedly unify them @@ -74,7 +74,7 @@ To use metamath-lamp, do the following: (text file). Throughout metamath-lamp there are various tooltips. -So if you hover over an iteractive item, +So if you hover over an interactive item, in most cases the tool will provide a brief explanation of what that item does. You don't need to memorize this guide! @@ -117,7 +117,7 @@ Let's show how to use metamath-lamp to create a simple proof, namely, that 2 + 2 = 4. This has already been proved in the set.mm database as theorem `2p2e4`. -#### Selecting the proof context for 2p2e4 +#### Selecting the proof context for `2p2e4` We first need to decide on the proof context, that is, the database(s) of axioms and proven theorems we'll use. In this case we'll use the most @@ -130,10 +130,10 @@ would simply reuse that existing proof. > Select Source type "Web", Alias "set.mm:latest"; after confirmation this > loads the given database. -> Now under scope select "Stop before" and enter the label "2p2e4". +> Now under scope select "Stop before" and enter the label `2p2e4`. > Finally, apply changes to the context. -#### Setting the goal for 2p2e4 +#### Setting the goal for `2p2e4` For this example we'll leave the proof description, variables, and disjoints blank. We do need to tell metamath-lamp our goal. @@ -167,9 +167,10 @@ label metamath-lamp suggested. But renaming some of the statements (especially the target one) makes them easier to distinguish for you and eventually this name will appear in the final generated proof. If you don't know what else to name the goal, we suggest using the name -"qed" to reduce confusion. +`qed` to reduce confusion. -In general, if you plan to eventually add this proof to the set.mm or iset.mm +In general, if you plan to eventually add this proof to the +`set.mm` or `iset.mm` databases, then you need to follow the [set.mm database conventions](https://us.metamath.org/mpeuni/conventions.html), including the @@ -182,14 +183,14 @@ So let's rename this goal statement to `2p2e4`: > Left click the label of the first statement > (you have to click directly on the number "1" > to the left of the first statement). -> Change the name of the statement from "1" to "2p2e4" and press Enter (Return). +> Change the name of the statement from "1" to `2p2e4` and press Enter (Return). #### Interlude: Brief review of metamath-lamp user interface Let's look at the display we have so far (your screen may look somewhat different): -![Metamath-lamp display with just the 2p2e4 goal](2p2e4_goal.png) +![Metamath-lamp display with just the `2p2e4` goal](2p2e4_goal.png) The top line summarizes the context - we loaded the `set.mm` database (classical logic and ZFC set theory) and stopped reading the database before @@ -235,7 +236,7 @@ Every statement has a box on its far left, which lets you select Now that we've had a brief introduction to the metamath-lamp user interface, let's decide how to use it to create our proof. -#### Deciding on a proof strategy for 2p2e4 +#### Deciding on a proof strategy for `2p2e4` Now we need to figure out how to prove this goal. @@ -301,14 +302,14 @@ We don't want to add this statement as the *last* statement, so we'll select the last statement before adding it (so we'll insert that statement before it). -> Select the checkbox to the left of the "2p2e4" goal statement. +> Select the checkbox to the left of the `2p2e4` goal statement. > Then select "+" (add new statement). > Notice that because a statement was selected, the new statement will -> be inserted before "2p2e4". +> be inserted before `2p2e4`. > Enter the new statement > `|- ( 3 + 1 ) = ( ( 2 + 1 ) + 1 )` > and press Enter (Return). -> Unselect the checkbox to the left of the "2p2e4" statement. +> Unselect the checkbox to the left of the `2p2e4` statement. > Now, while no statements are selected, > press unify (the multiple-connected dots symbol). Since there > was no specific statement selected, it will try to justify all statements. @@ -330,7 +331,7 @@ use the "duplicate" command to get us started: > `|- 4 = ( ( 2 + 1 ) + 1 )` > press Enter (Return). > Press unify, which will produce a green checkmark next to all the statements -> except our final "2p2e4" statement. +> except our final `2p2e4` statement. #### Expanding the meaning of ( 2 + 2 ) @@ -379,11 +380,11 @@ equal to very similar expressions. If we could prove that those expressions are equal to each other, we could trivially prove our goal. Let's try to do that. -> Select the checkbox to the left of the "2p2e4" goal statement. +> Select the checkbox to the left of the `2p2e4` goal statement. > Select "+" (add new statement). Enter the new statement > `|- ( ( 2 + 1 ) + 1 ) = ( 2 + ( 1 + 1 ) )` > and press Enter (Return). -> Unselect the "2p2e4" statement. +> Unselect the `2p2e4` statement. > As an experiment, select Unify while there's no statement selected; > you'll see that in this case it did *not* find a justification > for our new statement. @@ -420,8 +421,8 @@ and then selecting unify. > of this statement. For now, we'll just accept the defaults and press the > "Prove" button at the bottom of the dialogue. > After a moment it will present a list, and one of the first options -> (probably the first one) should use "addassi". -> The theorem "addassi" is a pre-existing theorem showing that +> (probably the first one) should use `addassi`. +> The theorem `addassi` is a pre-existing theorem showing that > addition is associative. > This requires multiple lines, because using this associativity > theorem requires showing that `1` and `2` are complex numbers. @@ -438,7 +439,7 @@ namely that `1 e. CC` (`1` is a complex number) and `2 e. CC` We now have a green checkmark next to all our statements, showing that all statements are have been proven. -Most importantly, the final statement "2p2e4" has a green checkmark, which +Most importantly, the final statement `2p2e4` has a green checkmark, which means we have proven our goal. Metamath-lamp automatically unified all the statements, and was able to complete the rest of the proof given what we had provided. @@ -459,7 +460,7 @@ Before we do, let's briefly talk about how to generate and import information. We can now show the compressed proof. This is the final proof we can add to a Metamath database. -> Select the green checkmark (*not* "P") on the "2p2e4" goal statement. +> Select the green checkmark (*not* "P") on the `2p2e4` goal statement. > > You can select "Copy" to copy the compressed proof into the clipboard. > Press "Close" @@ -598,7 +599,7 @@ Metamath-lamp will display error messages if statements are moved to make them depend on statements that have not been proved yet. -### Proof: The reciprocal of the cotangent is tangent (reccot) +### Proof: The reciprocal of the cotangent is tangent (`reccot`) Let's use metamath-lamp to create another proof, namely, that the reciprocal of the cotangent is tangent. @@ -613,9 +614,9 @@ This exercise is based on the video showing how to prove the same theorem using the mmj2 tool (["Introduction to Metamath and mmj2" by David A. Wheeler](https://www.youtube.com/watch?v=Rst2hZpWUbU)) and an earlier video of -[reccot being proved using metamath-lamp (no sound)](https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view). +[`reccot` being proved using metamath-lamp (no sound)](https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view). -#### Selecting the proof context for reccot +#### Selecting the proof context for `reccot` We first need to decide on the proof context, that is, the database(s) of axioms and proven theorems we'll use. In this case we'll again use the most @@ -628,9 +629,9 @@ means we need to erase the proof steps we have and change the context. Here's how to do that: > Select the checkbox on the editor bar above the field name "Description" -> to select *all* statements. select the trash can with an X +> to select *all* statements. Select the trash can with an X > ("delete selected statements") to delete them all. -> At the top of the browser window, select the dropdown arrow with the +> At the top of the browser window, select the drop-down arrow with the > "Loaded:..." text that hints at the context. > Make sure we are loading from the web the file "set.mm:latest", > and change the scope to "Stop before" the label `reccot` by typing it in @@ -642,7 +643,7 @@ context as usual. Here's how to do that instead: > Select Source type "Web", Alias "set.mm:latest"; after confirmation this > loads the given database. -> Now under scope select "Stop before" and enter the label "reccot". +> Now under scope select "Stop before" and enter the label `reccot`. > Finally, apply changes to the context. #### Setting the goal for reccot @@ -672,7 +673,7 @@ about where the parenthesis go. Now modify the label of this goal to `reccot`. > Select the statement number (1) using the left mouse button. -> Change the name of the statement to "reccot" and press Enter (Return). +> Change the name of the statement to `reccot` and press Enter (Return). Let's take a brief look at this goal. It illustrates several symbols in the set.mm database: @@ -699,7 +700,7 @@ It illustrates several symbols in the set.mm database: the tan(A) notation used by others but without context-dependent notational ambiguity. -#### Deciding on a proof strategy for reccot +#### Deciding on a proof strategy for `reccot` Now we need to figure out how to prove this goal. @@ -765,14 +766,14 @@ The fundamental issue is that although a theorem or axiom may use a variable (such as `A`), those variables can be replaced with other expressions when they are used. In this case, -the original "tanval" showed what the results are when `A` is the argument, +the original `tanval` showed what the results are when `A` is the argument, but we aren't limited to using `A`; we can use any expression that produces a class. In cases where metamath-lamp cannot be certain of exactly what you want, it will create work variables that you can then replace (substitute) with whatever you *do* want. -When using set.mm or iset.mm, you'll see work variables of certain forms: +When using `set.mm` or `iset.mm`, you'll see work variables of certain forms: * &Wnumber : an expression that is a well-formed formula (wff), in short, some value that is true or false. @@ -996,7 +997,7 @@ We now have several statements. All the statements are proved Our goal is about the reciprocal of the tangent, not the tangent itself. So let's modify the definition of the value of the cotangent to show -the value of the reciprocal of the tanget. +the value of the reciprocal of the tangent. Remember, in algebra you can do what you want on the left-hand-side of an equality, as long as you do the same thing on the right-hand side. @@ -1143,7 +1144,7 @@ If there are intermediate statements you need to prove to lead to the goal, just apply the same process - repeatedly work to prove those intermediate statements. -### Proof: Principle of the syllogism (syl) +### Proof: Principle of the syllogism (`syl`) @@ -1223,7 +1224,7 @@ Metamath-lamp validates labels you use [will soon validate goals](https://github.com/expln/metamath-lamp/issues/81)), and it will show an error message if the id is in use in the current context. -#### Easy proof of syl +#### Easy proof of `syl` Let's prove `syl` the easy way. Metamath-lamp's bottom-up proof tool can't automatically prove all @@ -1248,7 +1249,7 @@ meaning the goal is fully proved! You can left-click on its green checkmark to get a final proof that could be used in a final database. -#### Hard mode: Proving syl using only axioms +#### Hard mode: Proving `syl` using only axioms If you thought that was too easy, let's make it more challenging. Let's prove `syl` using *only* axioms. @@ -2372,13 +2373,13 @@ that shows details the proof of that theorem: Let's try that out next. -#### Viewing proof of mp2 +#### Viewing proof of `mp2` In the explorer view, scroll down to theorem `mp2`, and click on the *name* mp2. This will create a *new* tab that shows details about the proof of `mp2`. -Many capabiliities are available in a displayed proof. +Many capabilities are available in a displayed proof. Again, you can use the fragment selector to copy useful portions of any statement. @@ -2399,7 +2400,7 @@ Clicking on a reference to an assertion will show an individual assertion tab of that assertion (creating the tab if necessary). That tab will provide detailed information about the assertion. -#### Gaining an understanding on set.mm's beginnings +#### Gaining an understanding on `set.mm`'s beginnings You can use the explorer to gain many insights into a database (and mathematics in general). @@ -2411,7 +2412,7 @@ Let's go back to the explorer tab: > Click on the "Explorer" text in the tab bar, and scroll to the top. -Let's gain a brief understading of the first theorems and axioms. +Let's gain a brief understanding of the first theorems and axioms. We are entering the foundations of the foundations - the very basement - of the "typical" mathematics of classical logic and ZFC set theory. @@ -2429,7 +2430,7 @@ This also lets us restate truths; this is again only useful in special technical situations, but it's hard to argue with the conclusion. This theorem was contributed by Alan Sare, which you can see by clicking on the ">" next to the name. The names of people who formalized and -proposed various statements are included in their dscription. +proposed various statements are included in their description. Assertion 3 is our first axiom, but it's not an assertion of truth (`|-`), it's an assertion that something is a well-formed formula (`wff`). @@ -2444,7 +2445,7 @@ Assertion 4 is a similar axiom, stating that Notice the parentheses; since they are specified as part of the axiom allowing the use of `->`, the parentheses are required when using `->`. -Assrtion 5 is axiom `ax-mp`, aka modus ponens. +Assertion 5 is axiom `ax-mp`, aka modus ponens. If `ph` is true, and `ph` implies `ps`, then `ps` is true. The next 3 axioms define the axioms of propositional logic, that is,