Open euprunin opened 5 days ago
Here’s some additional context that might be helpful for anyone looking to fix this issue. The only difference between the two scripts is the use of echo
and read
.
% diff -u scripts/run_before_push.sh scripts/pre-push.sh
--- scripts/run_before_push.sh 2024-10-10 23:34:42
+++ scripts/pre-push.sh 2024-10-10 23:34:42
@@ -16,11 +16,10 @@
if [ ! -f lakefile.toml ]; then
echo "❌ Error: This doesn't appear to be the outermost 'equational_theories' directory.
Please run this script from the correct folder."
- echo "Press any key to exit..."
- read
exit 1
+else
+ echo "✅ Correct directory detected."
fi
-echo "✅ Correct directory detected."
# Get Mathlib cache
echo "Attempting to get Mathlib cache..."
@@ -34,8 +33,6 @@
echo "Building the project..."
if ! lake build equational_theories; then
echo "❌ Error: Project build failed. Please check the code for errors."
- echo "Press any key to exit..."
- read
exit 1
else
echo "✅ Project build completed successfully."
@@ -45,8 +42,6 @@
echo "Generating PDF version of the blueprint..."
if ! leanblueprint pdf; then
echo "❌ Error: Failed to generate PDF version of the blueprint."
- echo "Press any key to exit..."
- read
exit 1
else
echo "✅ PDF version of the blueprint generated successfully."
@@ -56,8 +51,6 @@
echo "Generating web version of the blueprint..."
if ! leanblueprint web; then
echo "❌ Error: Failed to generate web version of the blueprint."
- echo "Press any key to exit..."
- read
exit 1
else
echo "✅ Web version of the blueprint generated successfully."
@@ -67,8 +60,6 @@
echo "Checking if Lean declarations in the blueprint match the codebase..."
if ! lake exe checkdecls blueprint/lean_decls; then
echo "❌ Error: Some declarations in the blueprint do not match Lean declarations in the codebase."
- echo "Press any key to exit..."
- read
exit 1
else
echo "✅ All declarations match successfully."
Combine
run_before_push.sh
andpre-push.sh
into a single script.Rationale: DRY