|
| 1 | +#!/bin/bash |
| 2 | +# |
| 3 | +# Install external tools for LODA testing (Linux only) |
| 4 | +# This script installs: |
| 5 | +# - PARI/GP (from source) |
| 6 | +# - Lean (from official installation script) |
| 7 | +# |
| 8 | + |
| 9 | +set -e |
| 10 | + |
| 11 | +# Check if running on Linux |
| 12 | +if [[ "$(uname -s)" != "Linux" ]]; then |
| 13 | + echo "Error: This script only supports Linux systems" |
| 14 | + exit 1 |
| 15 | +fi |
| 16 | + |
| 17 | +# Create temporary directory for downloads |
| 18 | +TEMP_DIR=$(mktemp -d) |
| 19 | +trap "rm -rf $TEMP_DIR" EXIT |
| 20 | + |
| 21 | +echo "Installing external tools for LODA tests..." |
| 22 | +echo "Temporary directory: $TEMP_DIR" |
| 23 | +echo "" |
| 24 | + |
| 25 | +# Install PARI/GP |
| 26 | +echo "=== Installing PARI/GP ===" |
| 27 | +echo "" |
| 28 | + |
| 29 | +# PARI/GP version to install |
| 30 | +PARI_VERSION="2.17.3" |
| 31 | +PARI_TAR="pari-${PARI_VERSION}.tar.gz" |
| 32 | +PARI_URL="https://pari.math.u-bordeaux.fr/pub/pari/unix/${PARI_TAR}" |
| 33 | + |
| 34 | +echo "Downloading PARI/GP ${PARI_VERSION}..." |
| 35 | +cd "$TEMP_DIR" |
| 36 | +wget -q --show-progress "$PARI_URL" || curl -L -O "$PARI_URL" |
| 37 | + |
| 38 | +echo "Extracting PARI/GP..." |
| 39 | +tar -xzf "$PARI_TAR" |
| 40 | +cd "pari-${PARI_VERSION}" |
| 41 | + |
| 42 | +echo "Configuring PARI/GP..." |
| 43 | +./Configure --prefix=/usr/local |
| 44 | + |
| 45 | +echo "Building PARI/GP (this may take several minutes)..." |
| 46 | +make -j$(nproc) |
| 47 | + |
| 48 | +echo "Installing PARI/GP..." |
| 49 | +sudo make install |
| 50 | + |
| 51 | +echo "PARI/GP installation complete!" |
| 52 | +echo "" |
| 53 | + |
| 54 | +# Verify PARI/GP installation |
| 55 | +if command -v gp &> /dev/null; then |
| 56 | + echo "PARI/GP version:" |
| 57 | + gp --version-short |
| 58 | + echo "" |
| 59 | +else |
| 60 | + echo "Warning: gp command not found in PATH" |
| 61 | + echo "" |
| 62 | +fi |
| 63 | + |
| 64 | +# Install Lean |
| 65 | +echo "=== Installing Lean ===" |
| 66 | +echo "" |
| 67 | + |
| 68 | +# Check if elan (Lean version manager) is already installed |
| 69 | +if command -v elan &> /dev/null; then |
| 70 | + echo "Elan (Lean version manager) is already installed" |
| 71 | + echo "Updating Lean..." |
| 72 | + elan self update |
| 73 | + elan update |
| 74 | +else |
| 75 | + echo "Installing Lean via elan (Lean version manager)..." |
| 76 | + cd "$TEMP_DIR" |
| 77 | + |
| 78 | + # Download and run the elan installation script |
| 79 | + curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o elan-init.sh |
| 80 | + chmod +x elan-init.sh |
| 81 | + |
| 82 | + # Run the installer with default options (non-interactive) |
| 83 | + ./elan-init.sh -y --default-toolchain stable |
| 84 | + |
| 85 | + # Source the environment |
| 86 | + if [ -f "$HOME/.elan/env" ]; then |
| 87 | + source "$HOME/.elan/env" |
| 88 | + fi |
| 89 | +fi |
| 90 | + |
| 91 | +echo "Lean installation complete!" |
| 92 | +echo "" |
| 93 | + |
| 94 | +# Verify Lean installation |
| 95 | +if command -v lean &> /dev/null; then |
| 96 | + echo "Lean version:" |
| 97 | + lean --version |
| 98 | + echo "" |
| 99 | +else |
| 100 | + echo "Warning: lean command not found in PATH" |
| 101 | + echo "You may need to add ~/.elan/bin to your PATH:" |
| 102 | + echo " export PATH=\"\$HOME/.elan/bin:\$PATH\"" |
| 103 | + echo "" |
| 104 | +fi |
| 105 | + |
| 106 | +echo "=== Installation Summary ===" |
| 107 | +echo "" |
| 108 | +echo "All external tools have been installed successfully!" |
| 109 | +echo "" |
| 110 | +echo "PARI/GP: $(command -v gp &> /dev/null && echo 'Installed' || echo 'Not found in PATH')" |
| 111 | +echo "Lean: $(command -v lean &> /dev/null && echo 'Installed' || echo 'Not found in PATH')" |
| 112 | +echo "" |
| 113 | +echo "To enable external tool tests, set the environment variable:" |
| 114 | +echo " export LODA_TEST_WITH_EXTERNAL_TOOLS=1" |
| 115 | +echo "" |
| 116 | +echo "Then run tests with:" |
| 117 | +echo " ./loda test" |
| 118 | +echo "" |
0 commit comments