my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	#!/bin/bash
#2	set -e
#3
#4	# ── Rust / Cargo ────────────────────────────────────────────────────────────
#5	if ! command -v cargo &> /dev/null; then
#6	echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
#7	echo " Rust toolchain not found. Installing via rustup..."
#8	echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
#9	curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh -s -- -y
#10	source "$HOME/.cargo/env"
#11	fi
#12
#13	# ── Lean / elan ─────────────────────────────────────────────────────────────
#14	if ! command -v lean &> /dev/null && ! command -v elan &> /dev/null; then
#15	echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
#16	echo " Lean toolchain not found. Installing via elan..."
#17	echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
#18	curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \| sh -s -- -y --default-toolchain leanprover/lean4:v4.15.0
#19	export PATH="$HOME/.elan/bin:$PATH"
#20	fi
#21
#22	# ── Build qedgen binary ──────────────────────────────────────────────────
#23	if [ -f "bin/qedgen" ] && [ -x "bin/qedgen" ]; then
#24	echo "✓ Pre-built qedgen binary found"
#25	if ./bin/qedgen --version &> /dev/null; then
#26	echo "✓ Binary is compatible with this platform"
#27	else
#28	echo " Pre-built binary is not compatible, rebuilding..."
#29	cargo build --release
#30	mkdir -p bin
#31	cp target/release/qedgen bin/
#32	chmod +x bin/qedgen
#33	fi
#34	else
#35	echo "Building qedgen binary..."
#36	cargo build --release
#37	mkdir -p bin
#38	cp target/release/qedgen bin/
#39	chmod +x bin/qedgen
#40	fi
#41
#42	echo "✓ qedgen binary built successfully"
#43
#44	# ── Set up global validation workspace ──────────────────────────────────────
#45	# Pre-fetch Mathlib cache so the first `qedgen verify --validate` is fast.
#46	# This runs in the background so it doesn't block npm install.
#47
#48	setup_global_workspace() {
#49	local ws_dir
#50	if [ -n "$QEDGEN_VALIDATION_WORKSPACE" ]; then
#51	ws_dir="$QEDGEN_VALIDATION_WORKSPACE"
#52	elif [ "$(uname)" = "Darwin" ]; then
#53	ws_dir="$HOME/Library/Caches/qedgen-solana-skills/validation-workspace"
#54	elif [ -n "$XDG_CACHE_HOME" ]; then
#55	ws_dir="$XDG_CACHE_HOME/qedgen-solana-skills/validation-workspace"
#56	else
#57	ws_dir="$HOME/.cache/qedgen-solana-skills/validation-workspace"
#58	fi
#59
#60	# Skip if already set up
#61	if [ -f "$ws_dir/lakefile.lean" ] && [ -d "$ws_dir/.lake/packages/mathlib" ]; then
#62	echo "✓ Global validation workspace already exists at $ws_dir"
#63	return 0
#64	fi
#65
#66	echo "Setting up global validation workspace at $ws_dir..."
#67	echo " This downloads and caches Mathlib (~1-2 min with cache, 25+ min without)."
#68	echo " Running in background — qedgen will work once this completes."
#69
#70	mkdir -p "$ws_dir"
#71
#72	# Use qedgen setup command if available
#73	if [ -x "bin/qedgen" ]; then
#74	bin/qedgen setup --workspace "$ws_dir" &
#75	echo " Background PID: $!"
#76	else
#77	echo " Warning: binary not available, workspace will be set up on first use."
#78	fi
#79	}
#80
#81	setup_global_workspace
#82
#83	echo ""
#84	echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
#85	echo " qedgen-solana-skills installed successfully!"
#86	echo ""
#87	echo " Requirements:"
#88	echo " - MISTRAL_API_KEY environment variable must be set"
#89	echo " - Lean toolchain (auto-installed via elan)"
#90	echo ""
#91	echo " The global Mathlib cache may still be downloading in the background."
#92	echo " First run of 'qedgen verify --validate' may be slow if not ready."
#93	echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
#94

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public