Agent/install gh cli 32f2

.cursor/environment.json

@@ -1,4 +1,5 @@
 {
   "name": "lean4",
-  "install": "bash .cursor/install.sh"
+  "install": "bash .cursor/install.sh",
+  "start": "bash .cursor/gh-auth.sh"
 }

.cursor/gh-auth.sh

@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+# Authenticate the official GitHub CLI as the operator.
+# Cursor injects a GitHub App installation token as GH_TOKEN (ghs_...); that
+# token can clone/push but often cannot create PRs as a user. A personal PAT
+# must be supplied as the Runtime Secret GH_USER_TOKEN (not GH_TOKEN).
+set -euo pipefail
+
+export PATH="${HOME}/.local/bin:/usr/bin:${PATH}"
+
+if [ -z "${GH_USER_TOKEN:-}" ]; then
+  echo "==> GH_USER_TOKEN unset; gh uses the Cursor GitHub App token"
+  exit 0
+fi
+
+echo "==> Authenticating gh with GH_USER_TOKEN"
+printf '%s\n' "${GH_USER_TOKEN}" | gh auth login --with-token --hostname github.com
+gh auth status --hostname github.com

.cursor/install.sh

@@ -34,6 +34,36 @@ done
 
 echo "==> elan $(elan --version)"
 
+# Official GitHub CLI (https://github.com/cli/cli/blob/trunk/docs/install_linux.md).
+# Ubuntu may ship an older universe package; Cloud Agent images also put
+# `/exec-daemon/gh` first on PATH. Install the GitHub apt package and prefer it.
+GH_APT_LIST="/etc/apt/sources.list.d/github-cli.list"
+GH_APT_KEY="/etc/apt/keyrings/githubcli-archive-keyring.gpg"
+if [ -f "${GH_APT_LIST}" ] && dpkg-query -W -f='${Status}' gh 2>/dev/null | grep -q "install ok installed"; then
+  echo "==> gh package already present"
+else
+  echo "==> Installing official GitHub CLI"
+  sudo mkdir -p -m 755 /etc/apt/keyrings /etc/apt/sources.list.d
+  curl -fsSL https://cli.github.com/packages/githubcli-archive-keyring.gpg \
+    | sudo tee "${GH_APT_KEY}" >/dev/null
+  sudo chmod go+r "${GH_APT_KEY}"
+  echo "deb [arch=$(dpkg --print-architecture) signed-by=${GH_APT_KEY}] https://cli.github.com/packages stable main" \
+    | sudo tee "${GH_APT_LIST}" >/dev/null
+  sudo apt-get update -y
+  sudo DEBIAN_FRONTEND=noninteractive apt-get install -y gh
+fi
+mkdir -p "${HOME}/.local/bin"
+ln -sfn /usr/bin/gh "${HOME}/.local/bin/gh"
+export PATH="${HOME}/.local/bin:${PATH}"
+LOCAL_BIN_LINE='export PATH="$HOME/.local/bin:$PATH"'
+for profile in "${HOME}/.bashrc" "${HOME}/.profile"; do
+  if [ -e "${profile}" ] && grep -Fq '.local/bin' "${profile}"; then
+    continue
+  fi
+  printf '\n# official GitHub CLI on PATH\n%s\n' "${LOCAL_BIN_LINE}" >> "${profile}"
+done
+echo "==> gh $(command -v gh) ($(gh --version | head -1))"
+
 TOOLCHAIN="$(tr -d '[:space:]' < lean-toolchain)"
 if elan toolchain list | grep -Fq "${TOOLCHAIN}"; then
   echo "==> Toolchain ${TOOLCHAIN} already installed"

AGENTS.md

@@ -13,3 +13,5 @@ Toolchain is pinned in `lean-toolchain` (elan). Mathlib is pinned to the same ta
 - Run the executable: `lake exe lean4`
 - First olympiad problem: `Lean4/Imo1959P1.lean` (IMO 1959 Q1).
 - After install, `elan`, `lean`, and `lake` are on `PATH` via `$HOME/.elan/bin`.
+- GitHub CLI: official `gh` apt package, on `PATH` via `$HOME/.local/bin`.
+- GitHub auth: add a **Runtime Secret** named `GH_USER_TOKEN` (a PAT). Do not use `GH_TOKEN`; Cursor overwrites that with the GitHub App token. `.cursor/gh-auth.sh` runs on each boot and logs `gh` in with that PAT.