config.example.sh

# config.example.sh -- copy to `config.sh` and fill in, then `source config.sh`.
#
# `config.sh` is gitignored, so your machine-specific settings never reach the repository.
# Every setting is OPTIONAL: the Lean side of this project works with none of them.
# They are only needed if you want the computer-algebra bridge.

# ---------------------------------------------------------------------------
# Magma (optional)
# ---------------------------------------------------------------------------
# Magma is commercial and is usually installed on a departmental server rather than
# your laptop, so this project drives it over SSH. Set the host you can reach with
# passwordless SSH (i.e. `ssh $LEAN_MAGMA_HOST true` succeeds without a prompt).
#
# Leave unset to disable the Magma bridge entirely; tools/magma_run.sh will then tell
# you what to configure rather than failing obscurely.

# export LEAN_MAGMA_HOST="magma.your-institution.example"

# Path to the magma binary ON THAT HOST. Find it with:
#     ssh $LEAN_MAGMA_HOST 'bash -lc "command -v magma"'
# Note the login shell: many installations put magma on the PATH only for login
# shells, which is why this project invokes it via `bash -lc`.

# export LEAN_MAGMA_BIN="$LEAN_MAGMA_BIN"

# ---------------------------------------------------------------------------
# Local Magma instead (optional)
# ---------------------------------------------------------------------------
# If magma is installed locally, point the host at localhost and the binary at it:
#
# export LEAN_MAGMA_HOST="localhost"
# export LEAN_MAGMA_BIN="$(command -v magma)"