From 291dc89e448a73cdb7c1f4e17e961fe48d4e8d42 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Sep 2022 15:58:23 +0200
Subject: [PATCH] avoid deprecated fgrep/egrep
fixes #486
---
Makefile.coq.local | 6 +++---
coq-lint.sh | 2 +-
make-package | 8 ++++----
3 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 136633147..479e4c0a1 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -11,11 +11,11 @@ style: $(VFILES) coq-lint.sh
# Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
$(SHOW)"COQLINT"
$(HIDE)for FILE in $(VFILES); do \
- if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+ if ! grep -F -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
./coq-lint.sh "$$FILE" || exit 1; \
done
# Make sure main Iris does not import other Iris packages.
- $(HIDE)if egrep 'iris\.(heap_lang|deprecated|unstable)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
+ $(HIDE)if grep -E 'iris\.(heap_lang|deprecated|unstable)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
.PHONY: style
# the test suite
@@ -27,7 +27,7 @@ test: $(TESTFILES:.v=.vo)
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
+COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | grep -E '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES'
diff --git a/coq-lint.sh b/coq-lint.sh
index 50d5f26f5..f80f90aef 100755
--- a/coq-lint.sh
+++ b/coq-lint.sh
@@ -4,7 +4,7 @@ set -e
FILE="$1"
-if egrep -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|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
diff --git a/make-package b/make-package
index 55c051a9f..5bf541bca 100755
--- a/make-package
+++ b/make-package
@@ -9,7 +9,7 @@ shift
COQFILE="_CoqProject.$PROJECT"
MAKEFILE="Makefile.package.$PROJECT"
-if ! egrep -q "^$PROJECT/" _CoqProject; then
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
exit 1
fi
@@ -17,11 +17,11 @@ fi
# Generate _CoqProject file and Makefile
rm -f "$COQFILE"
# Get the right "-Q" line.
-egrep "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
# Get everything until the first empty line except for the "-Q" lines.
-sed -n '/./!q;p' _CoqProject | egrep -v "^-Q " >> "$COQFILE"
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
# Get the files.
-egrep "^$PROJECT/" _CoqProject >> "$COQFILE"
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
# Now we can run coq_makefile.
"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
--
GitLab