File: coq-lint.sh

package info (click to toggle)
coq-stdpp 1.12.0-1
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 1,724 kB
  • sloc: makefile: 53; sh: 35; sed: 1
file content (12 lines) | stat: -rwxr-xr-x 547 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
 
#!/bin/sh
set -e
## A simple shell script checking for some common Coq issues.

FILE="$1"

if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
    echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
    echo "Please add 'Global' or 'Local' as appropriate."
    echo
    exit 1
fi