diff --git a/scripts/install_pre-push.sh b/scripts/install_pre-push.sh deleted file mode 100755 index c070096..0000000 --- a/scripts/install_pre-push.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/usr/bin/env bash - -# Rename the pre-push sample file if it exists -if [ -f ".git/hooks/pre-push.sample" ]; then - mv .git/hooks/pre-push.sample .git/hooks/pre-push -fi - -# Copy the content of scripts/pre-push into .git/hooks/pre-push -cp scripts/pre-push.sh .git/hooks/pre-push - -# Make the pre-push hook executable -chmod +x .git/hooks/pre-push - -echo "Pre-push hook installed." diff --git a/scripts/pre-push.sh b/scripts/pre-push.sh deleted file mode 100644 index 2afe925..0000000 --- a/scripts/pre-push.sh +++ /dev/null @@ -1,67 +0,0 @@ -################################################################################ -# TEST SCRIPT TO RUN BEFORE PUSHING CHANGES -# -# This script ensures that the key components of the Lean project are functional -# before changes are pushed to the repository by checking that: -# 1. You are in the correct directory; -# 2. The project builds successfully; -# 3. The blueprint is successfully generated in both PDF and web versions; -# 4. LaTeX declarations in the blueprint match Lean declarations in the codebase. -################################################################################ - -# Ensure the script is in the outermost 'equational_theories' folder -echo "Checking if you are in the correct directory..." -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." - exit 1 -else - echo "✅ Correct directory detected." -fi - -# Get Mathlib cache -echo "Attempting to get Mathlib cache..." -if ! lake exe cache get; then - echo "❌ Error: Failed to get Mathlib cache. Continuing without cache." -else - echo "✅ Mathlib cache successfully retrieved." -fi - -# Build the project -echo "Building the project..." -if ! lake build equational_theories; then - echo "❌ Error: Project build failed. Please check the code for errors." - exit 1 -else - echo "✅ Project build completed successfully." -fi - -# Generate the PDF version of the blueprint -echo "Generating PDF version of the blueprint..." -if ! leanblueprint pdf; then - echo "❌ Error: Failed to generate PDF version of the blueprint." - exit 1 -else - echo "✅ PDF version of the blueprint generated successfully." -fi - -# Generate the web version of the blueprint -echo "Generating web version of the blueprint..." -if ! leanblueprint web; then - echo "❌ Error: Failed to generate web version of the blueprint." - exit 1 -else - echo "✅ Web version of the blueprint generated successfully." -fi - -# Check declarations -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." - exit 1 -else - echo "✅ All declarations match successfully." -fi - -# Final message on test completion -echo "🎉 All steps completed successfully! You are ready to push." diff --git a/scripts/run_before_push.sh b/scripts/run_before_push.sh deleted file mode 100755 index a6b4242..0000000 --- a/scripts/run_before_push.sh +++ /dev/null @@ -1,78 +0,0 @@ -#!/usr/bin/env bash - -################################################################################ -# TEST SCRIPT TO RUN BEFORE PUSHING CHANGES -# -# This script ensures that the key components of the Lean project are functional -# before changes are pushed to the repository by checking that: -# 1. You are in the correct directory; -# 2. The project builds successfully; -# 3. The blueprint is successfully generated in both PDF and web versions; -# 4. LaTeX declarations in the blueprint match Lean declarations in the codebase. -################################################################################ - -# Ensure the script is in the outermost 'equational_theories' folder -echo "Checking if you are in the correct directory..." -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 -fi -echo "✅ Correct directory detected." - -# Get Mathlib cache -echo "Attempting to get Mathlib cache..." -if ! lake exe cache get; then - echo "❌ Error: Failed to get Mathlib cache. Continuing without cache." -else - echo "✅ Mathlib cache successfully retrieved." -fi - -# Build the project -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." -fi - -# Generate the PDF version of the blueprint -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." -fi - -# Generate the web version of the blueprint -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." -fi - -# Check declarations -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." -fi - -# Final message on test completion -echo "🎉 All steps completed successfully! You are ready to push."