From 273d05ab884eab292db5d56882f3c8eb3a5b451a Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 25 Nov 2025 23:05:49 +0000
Subject: [PATCH 01/19] [ new ] install script for the standard library

---
 stdlib-install.sh | 141 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 141 insertions(+)
 create mode 100644 stdlib-install.sh

diff --git a/stdlib-install.sh b/stdlib-install.sh
new file mode 100644
index 0000000000..b5f596d1a4
--- /dev/null
+++ b/stdlib-install.sh
@@ -0,0 +1,141 @@
+#!/bin/sh
+
+set -eu
+
+throwError() {
+  echo "\033[91m✗\033[0m $1." >&2
+  exit 1
+}
+
+logHappy() {
+  echo "\033[32m✔\033[0m $1"
+}
+
+# Pick the Agda executable to analyse
+# unless the caller has specified one
+if [ -z ${AGDA_EXEC-} ]; then
+    read -p "What's the name of your Agda executable (default: agda)? " AGDA_EXEC
+    if [ -z "$AGDA_EXEC" ]; then
+        AGDA_EXEC=agda
+    fi
+fi
+
+# Double check that the command exists
+if ! [ -x "$(command -v $AGDA_EXEC)" ]; then
+  throwError "'$AGDA_EXEC' is not a valid executable"
+fi
+
+logHappy "Agda executable: $AGDA_EXEC"
+
+# Ask the executable for its version number
+# unless the caller has specified one
+if [ -z ${AGDA_VERSION-} ]; then
+  AGDA_VERSION=$($AGDA_EXEC --version | head -n 1 | sed "s/^[a-zA-Z ]*\(2[0-9.]*\)\(-.*\)*$/\1/")
+fi
+
+# Double check that the version number is correct
+if ! echo "$AGDA_VERSION" | grep -Eq "^2(\.[0-9]+)+$"; then
+  throwError "'$AGDA_VERSION' is not a valid version number"
+fi
+
+logHappy "Agda version number: $AGDA_VERSION"
+
+# Pick the install directory
+# unless the caller has specified one
+if [ -z ${AGDA_DIR-} ]; then
+  AGDA_DIR=$($AGDA_EXEC --print-agda-app-dir | head -n 1 || true)
+  if echo "$AGDA_DIR" | grep -Eq "^Error.*$"; then
+    AGDA_DIR="$HOME/.agda"
+  fi
+  read -p "Where do you want to install the library (default: $AGDA_DIR)? " AGDA_DIR_OVERWRITE
+  if ! [ -z "$AGDA_DIR_OVERWRITE" ]; then
+    AGDA_DIR="$AGDA_DIR_OVERWRITE"
+  fi
+fi
+
+logHappy "Agda directory: $AGDA_DIR"
+
+if [ -z ${STDLIB_VERSION-} ]; then
+  case "$AGDA_VERSION" in
+    "2.8.0")
+      STDLIB_VERSION=2.3
+      ;;
+    "2.7.0.1")
+      STDLIB_VERSION=2.3
+      ;;
+    "2.7.0")
+      STDLIB_VERSION=2.2
+      ;;
+    "2.6.4.3")
+      STDLIB_VERSION=2.1
+      ;;
+    "2.6.4.2")
+      STDLIB_VERSION=2.0
+      ;;
+    "2.6.4.2")
+      STDLIB_VERSION=2.0
+      ;;
+    "2.6.4.1")
+      STDLIB_VERSION=2.0
+      ;;
+    "2.6.4")
+      STDLIB_VERSION=2.0
+      ;;
+    "2.6.3")
+      STDLIB_VERSION=1.7.3
+      ;;
+    "2.6.2.2")
+      STDLIB_VERSION=1.7.1
+      ;;
+    "2.6.2.1")
+      STDLIB_VERSION=1.7.1
+      ;;
+    "2.6.1")
+      STDLIB_VERSION=1.7.1
+      ;;
+    *)
+      STDLIB_VERSION=experimental
+      ;;
+  esac
+fi
+
+logHappy "Standard library version: $STDLIB_VERSION"
+
+case "$STDLIB_VERSION" in
+  "master")
+    STDLIB_TAG="refs/heads/master"
+    ;;
+  "experimental")
+    STDLIB_TAG="refs/heads/experimental"
+    ;;
+  *)
+    STDLIB_TAG="v$STDLIB_VERSION"
+    ;;
+esac
+
+# Setting up the Agda install directory
+mkdir -p "$AGDA_DIR"
+cd "$AGDA_DIR"
+mkdir -p logs
+
+# Downloading and extracting the standard library
+STDLIB_TARBALL_NAME="/tmp/agda-stdlib-$STDLIB_VERSION.tar.gz"
+STDLIB_TARBALL_URL="https://github.com/agda/agda-stdlib/archive/$STDLIB_TAG.tar.gz"
+wget -O "$STDLIB_TARBALL_NAME" "$STDLIB_TARBALL_URL" -o logs/wget
+tar -zxvf "$STDLIB_TARBALL_NAME" > logs/tar
+
+logHappy "Successfully downloaded the standard library"
+
+# Adding the standard library to the list of installed and default libraries
+STDLIB_PATH="$AGDA_DIR/agda-stdlib-$STDLIB_VERSION/standard-library.agda-lib"
+AGDA_LIBRARIES_FILE="libraries-$AGDA_VERSION"
+
+if ! grep -Eq "$STDLIB_PATH" "$AGDA_LIBRARIES_FILE"; then
+  echo "$STDLIB_PATH" >> "$AGDA_LIBRARIES_FILE"
+fi
+
+if ! grep -Eq "^standard-library$" "defaults-$AGDA_VERSION"; then
+  echo "standard-library" >> "defaults-$AGDA_VERSION"
+fi
+
+logHappy "Successfully installed the standard library"

From fdedd68987610d387d0544870eb4d1cfb92d7de3 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 15:38:03 +0000
Subject: [PATCH 02/19] [ cosmetic ] cleanup big cases

---
 stdlib-install.sh | 64 ++++++++++++-----------------------------------
 1 file changed, 16 insertions(+), 48 deletions(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index b5f596d1a4..2db1c87654 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -57,60 +57,28 @@ logHappy "Agda directory: $AGDA_DIR"
 
 if [ -z ${STDLIB_VERSION-} ]; then
   case "$AGDA_VERSION" in
-    "2.8.0")
-      STDLIB_VERSION=2.3
-      ;;
-    "2.7.0.1")
-      STDLIB_VERSION=2.3
-      ;;
-    "2.7.0")
-      STDLIB_VERSION=2.2
-      ;;
-    "2.6.4.3")
-      STDLIB_VERSION=2.1
-      ;;
-    "2.6.4.2")
-      STDLIB_VERSION=2.0
-      ;;
-    "2.6.4.2")
-      STDLIB_VERSION=2.0
-      ;;
-    "2.6.4.1")
-      STDLIB_VERSION=2.0
-      ;;
-    "2.6.4")
-      STDLIB_VERSION=2.0
-      ;;
-    "2.6.3")
-      STDLIB_VERSION=1.7.3
-      ;;
-    "2.6.2.2")
-      STDLIB_VERSION=1.7.1
-      ;;
-    "2.6.2.1")
-      STDLIB_VERSION=1.7.1
-      ;;
-    "2.6.1")
-      STDLIB_VERSION=1.7.1
-      ;;
-    *)
-      STDLIB_VERSION=experimental
-      ;;
+    "2.8.0")   STDLIB_VERSION="2.3" ;;
+    "2.7.0.1") STDLIB_VERSION="2.3" ;;
+    "2.7.0")   STDLIB_VERSION="2.2" ;;
+    "2.6.4.3") STDLIB_VERSION="2.1" ;;
+    "2.6.4.2") STDLIB_VERSION="2.0" ;;
+    "2.6.4.2") STDLIB_VERSION="2.0" ;;
+    "2.6.4.1") STDLIB_VERSION="2.0" ;;
+    "2.6.4")   STDLIB_VERSION="2.0" ;;
+    "2.6.3")   STDLIB_VERSION="1.7.3" ;;
+    "2.6.2.2") STDLIB_VERSION="1.7.1" ;;
+    "2.6.2.1") STDLIB_VERSION="1.7.1" ;;
+    "2.6.1")   STDLIB_VERSION="1.7.1" ;;
+    *)         STDLIB_VERSION="experimental" ;;
   esac
 fi
 
 logHappy "Standard library version: $STDLIB_VERSION"
 
 case "$STDLIB_VERSION" in
-  "master")
-    STDLIB_TAG="refs/heads/master"
-    ;;
-  "experimental")
-    STDLIB_TAG="refs/heads/experimental"
-    ;;
-  *)
-    STDLIB_TAG="v$STDLIB_VERSION"
-    ;;
+  "master")       STDLIB_TAG="refs/heads/master" ;;
+  "experimental") STDLIB_TAG="refs/heads/experimental" ;;
+  *)              STDLIB_TAG="v$STDLIB_VERSION" ;;
 esac
 
 # Setting up the Agda install directory

From 4997342403bbe5dbffe401b10c2ef01fd4b3baaf Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 15:38:24 +0000
Subject: [PATCH 03/19] [ cosmetic ] indentation

---
 stdlib-install.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 2db1c87654..4cd40ac159 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -14,10 +14,10 @@ logHappy() {
 # Pick the Agda executable to analyse
 # unless the caller has specified one
 if [ -z ${AGDA_EXEC-} ]; then
-    read -p "What's the name of your Agda executable (default: agda)? " AGDA_EXEC
-    if [ -z "$AGDA_EXEC" ]; then
-        AGDA_EXEC=agda
-    fi
+  read -p "What's the name of your Agda executable (default: agda)? " AGDA_EXEC
+  if [ -z "$AGDA_EXEC" ]; then
+    AGDA_EXEC=agda
+  fi
 fi
 
 # Double check that the command exists

From 827c2fef620c9da28d1d52f1c324c14ddb133480 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 15:38:49 +0000
Subject: [PATCH 04/19] [ fix ] touch files before grepping them

---
 stdlib-install.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 4cd40ac159..c0cc976032 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -98,10 +98,12 @@ logHappy "Successfully downloaded the standard library"
 STDLIB_PATH="$AGDA_DIR/agda-stdlib-$STDLIB_VERSION/standard-library.agda-lib"
 AGDA_LIBRARIES_FILE="libraries-$AGDA_VERSION"
 
+touch "$AGDA_LIBRARIES_FILE"
 if ! grep -Eq "$STDLIB_PATH" "$AGDA_LIBRARIES_FILE"; then
   echo "$STDLIB_PATH" >> "$AGDA_LIBRARIES_FILE"
 fi
 
+touch "defaults-$AGDA_VERSION"
 if ! grep -Eq "^standard-library$" "defaults-$AGDA_VERSION"; then
   echo "standard-library" >> "defaults-$AGDA_VERSION"
 fi

From 5e9fe26a11d1af7a1f1f723b8735ef2beddca548 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 15:50:46 +0000
Subject: [PATCH 05/19] [ doc ] explain option choice

---
 stdlib-install.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index c0cc976032..d7505da208 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -30,6 +30,8 @@ logHappy "Agda executable: $AGDA_EXEC"
 # Ask the executable for its version number
 # unless the caller has specified one
 if [ -z ${AGDA_VERSION-} ]; then
+  # There is a more recent "--numeric-version" option but old
+  # versions of Agda do not implement it!
   AGDA_VERSION=$($AGDA_EXEC --version | head -n 1 | sed "s/^[a-zA-Z ]*\(2[0-9.]*\)\(-.*\)*$/\1/")
 fi
 

From 58669105ea04dde8e3752ef01cf1ebd86d683b2e Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 15:51:14 +0000
Subject: [PATCH 06/19] [ more ] check dependencies + debug mode

---
 stdlib-install.sh | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index d7505da208..2f0e1e3531 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -2,6 +2,14 @@
 
 set -eu
 
+isDebugMode() {
+  ! [ -z ${DEBUG-} ]
+}
+
+if ! [ -z ${SHELL_DEBUG-} ]; then
+  set -x
+fi
+
 throwError() {
   echo "\033[91m✗\033[0m $1." >&2
   exit 1
@@ -11,6 +19,22 @@ logHappy() {
   echo "\033[32m✔\033[0m $1"
 }
 
+checkDependency () {
+  if ! [ -x "$(command -v $1)" ]; then
+    throwError "Missing dependency: I could not find the executable '$1'"
+  elif isDebugMode; then
+    logHappy "Found '$1'"
+  fi
+}
+
+checkDependency "grep"
+checkDependency "head"
+checkDependency "mkdir"
+checkDependency "sed"
+checkDependency "tar"
+checkDependency "touch"
+checkDependency "wget"
+
 # Pick the Agda executable to analyse
 # unless the caller has specified one
 if [ -z ${AGDA_EXEC-} ]; then

From a45495de8395ab3aafa725086f4c86fa1b4bbabd Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 15:56:02 +0000
Subject: [PATCH 07/19] [ fix ] be more careful about overwriting dirs

---
 stdlib-install.sh | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 2f0e1e3531..7bf3fa85bc 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -19,6 +19,10 @@ logHappy() {
   echo "\033[32m✔\033[0m $1"
 }
 
+logWarning() {
+  echo "\033[93m⚠\033[0m $1"
+}
+
 checkDependency () {
   if ! [ -x "$(command -v $1)" ]; then
     throwError "Missing dependency: I could not find the executable '$1'"
@@ -113,13 +117,32 @@ cd "$AGDA_DIR"
 mkdir -p logs
 
 # Downloading and extracting the standard library
-STDLIB_TARBALL_NAME="/tmp/agda-stdlib-$STDLIB_VERSION.tar.gz"
+STDLIB_DIR_NAME="agda-stdlib-$STDLIB_VERSION"
+STDLIB_TARBALL_NAME="/tmp/$STDLIB_DIR_NAME.tar.gz"
 STDLIB_TARBALL_URL="https://github.com/agda/agda-stdlib/archive/$STDLIB_TAG.tar.gz"
 wget -O "$STDLIB_TARBALL_NAME" "$STDLIB_TARBALL_URL" -o logs/wget
-tar -zxvf "$STDLIB_TARBALL_NAME" > logs/tar
 
 logHappy "Successfully downloaded the standard library"
 
+if [ -d "$STDLIB_DIR_NAME" ]; then
+  logWarning "The directory $AGDA_DIR/$STDLIB_DIR_NAME already exists."
+  while true; do
+    read -p "Do you want to overwrite it? (yN) " DIR_OVERWRITE
+    DIR_OVERWRITE=${DIR_OVERWRITE:-n}
+    case "$DIR_OVERWRITE" in
+      [yY]*) DIR_OVERWRITE="y"; break;;
+      [nN]*) DIR_OVERWRITE="n"; break;;
+      *) echo "Please answer y or n.";;
+    esac
+  done
+  if [ "$DIR_OVERWRITE" = "y" ]; then
+    rm -rf "$STDLIB_DIR_NAME"
+    tar -zxvf "$STDLIB_TARBALL_NAME" > logs/tar
+  fi
+else
+  tar -zxvf "$STDLIB_TARBALL_NAME" > logs/tar
+fi
+
 # Adding the standard library to the list of installed and default libraries
 STDLIB_PATH="$AGDA_DIR/agda-stdlib-$STDLIB_VERSION/standard-library.agda-lib"
 AGDA_LIBRARIES_FILE="libraries-$AGDA_VERSION"

From 493080f98ce4082c085fd6bfca990cfb1c1d06b5 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 15:56:21 +0000
Subject: [PATCH 08/19] [ cosmetic ] more structure

---
 stdlib-install.sh | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 7bf3fa85bc..5d4e3d29a4 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -1,5 +1,8 @@
 #!/bin/sh
 
+########################################################################
+# DEBUG AND LOGGING
+
 set -eu
 
 isDebugMode() {
@@ -23,6 +26,9 @@ logWarning() {
   echo "\033[93m⚠\033[0m $1"
 }
 
+########################################################################
+## PRELIMINARY CHECKS
+
 checkDependency () {
   if ! [ -x "$(command -v $1)" ]; then
     throwError "Missing dependency: I could not find the executable '$1'"
@@ -39,6 +45,9 @@ checkDependency "tar"
 checkDependency "touch"
 checkDependency "wget"
 
+########################################################################
+## IDENTIFY AND INSTALL THE CORRECT STDLIB VERSION
+
 # Pick the Agda executable to analyse
 # unless the caller has specified one
 if [ -z ${AGDA_EXEC-} ]; then

From eba7fa75f82af3e1715a1c4dba29e396f4885122 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 16:10:26 +0000
Subject: [PATCH 09/19] [ ergonomics ] make more of an effort

Keep asking the user until we get a valid Agda executable
---
 stdlib-install.sh | 27 ++++++++++++++++++---------
 1 file changed, 18 insertions(+), 9 deletions(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 5d4e3d29a4..68d3a82334 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -22,6 +22,10 @@ logHappy() {
   echo "\033[32m✔\033[0m $1"
 }
 
+logUnhappy() {
+  echo "\033[91m✗\033[0m $1."
+}
+
 logWarning() {
   echo "\033[93m⚠\033[0m $1"
 }
@@ -51,14 +55,19 @@ checkDependency "wget"
 # Pick the Agda executable to analyse
 # unless the caller has specified one
 if [ -z ${AGDA_EXEC-} ]; then
-  read -p "What's the name of your Agda executable (default: agda)? " AGDA_EXEC
-  if [ -z "$AGDA_EXEC" ]; then
-    AGDA_EXEC=agda
-  fi
-fi
-
-# Double check that the command exists
-if ! [ -x "$(command -v $AGDA_EXEC)" ]; then
+  while true; do
+    read -p "What's the name of your Agda executable (default: agda)? " AGDA_EXEC
+    if [ -z "$AGDA_EXEC" ]; then
+      AGDA_EXEC=agda
+    fi
+    # Double check that the command exists
+    if ! [ -x "$(command -v $AGDA_EXEC)" ]; then
+      logUnhappy "'$AGDA_EXEC' is not a valid executable"
+    else
+      break
+    fi
+  done
+elif ! [ -x "$(command -v $AGDA_EXEC)" ]; then
   throwError "'$AGDA_EXEC' is not a valid executable"
 fi
 
@@ -141,7 +150,7 @@ if [ -d "$STDLIB_DIR_NAME" ]; then
     case "$DIR_OVERWRITE" in
       [yY]*) DIR_OVERWRITE="y"; break;;
       [nN]*) DIR_OVERWRITE="n"; break;;
-      *) echo "Please answer y or n.";;
+      *) logUnhappy "Invalid answer: '$DIR_OVERWRITE'. Please answer y or n.";;
     esac
   done
   if [ "$DIR_OVERWRITE" = "y" ]; then

From b7e5775582ab1b1c48bd896537bd9ef181f9ef8c Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 16:33:39 +0000
Subject: [PATCH 10/19] [ doc ] the installation instruction

---
 README.md                 |  6 ++++++
 doc/installation-guide.md | 14 ++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/README.md b/README.md
index 4eba8bf8cd..ae44ede8da 100644
--- a/README.md
+++ b/README.md
@@ -30,6 +30,12 @@ in glorious clickable HTML.
 
 ## Installation instructions
 
+On Unix-style systems, it should be as simple as
+
+```shell
+sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh))"
+```
+
 See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/doc/installation-guide.md) for the latest version of the standard library.
 
 #### Old versions of Agda
diff --git a/doc/installation-guide.md b/doc/installation-guide.md
index 65016a1fa3..0a4c4e4d49 100644
--- a/doc/installation-guide.md
+++ b/doc/installation-guide.md
@@ -3,6 +3,20 @@ Installation instructions
 
 Note: the full story on installing Agda libraries can be found at [readthedocs](http://agda.readthedocs.io/en/latest/tools/package-system.html).
 
+
+## Automated installation on Unix-style systems
+
+Running the following command in a terminal will download the
+[installation script](../stdlib-install.sh) and run. It will
+ask you some questions about your setup and automatically install
+a version of the stdlib compatible with your version of Agda.
+
+```shell
+sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh))"
+```
+
+## Manual installation
+
 Use version v2.3 of the standard library with Agda v2.8.0 or v2.7.0.1. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
 
 1. Navigate to a suitable directory `$HERE` (replace appropriately) where

From 7c4e75f8b853845dbc55d081e06a53b94b81571c Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 16:51:27 +0000
Subject: [PATCH 11/19] [ cleanup ] follow the shellcheck advice

---
 stdlib-install.sh | 46 ++++++++++++++++++++--------------------------
 1 file changed, 20 insertions(+), 26 deletions(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 68d3a82334..75f16cf773 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -6,35 +6,27 @@
 set -eu
 
 isDebugMode() {
-  ! [ -z ${DEBUG-} ]
+  [ -n "${DEBUG-}" ]
 }
 
-if ! [ -z ${SHELL_DEBUG-} ]; then
+if [ -n "${SHELL_DEBUG-}" ]; then
   set -x
 fi
 
 throwError() {
-  echo "\033[91m✗\033[0m $1." >&2
+  printf "\033[91m✗\033[0m %s.\n" "$1" >&2
   exit 1
 }
 
-logHappy() {
-  echo "\033[32m✔\033[0m $1"
-}
-
-logUnhappy() {
-  echo "\033[91m✗\033[0m $1."
-}
-
-logWarning() {
-  echo "\033[93m⚠\033[0m $1"
-}
+logHappy()   { printf "\033[32m✔\033[0m %s.\n" "$1"; }
+logUnhappy() { printf "\033[91m✗\033[0m %s.\n" "$1"; }
+logWarning() { printf "\033[93m⚠\033[0m %s.\n" "$1"; }
 
 ########################################################################
 ## PRELIMINARY CHECKS
 
 checkDependency () {
-  if ! [ -x "$(command -v $1)" ]; then
+  if ! [ -x "$(command -v "$1")" ]; then
     throwError "Missing dependency: I could not find the executable '$1'"
   elif isDebugMode; then
     logHappy "Found '$1'"
@@ -54,20 +46,21 @@ checkDependency "wget"
 
 # Pick the Agda executable to analyse
 # unless the caller has specified one
-if [ -z ${AGDA_EXEC-} ]; then
+if [ -z "${AGDA_EXEC-}" ]; then
   while true; do
-    read -p "What's the name of your Agda executable (default: agda)? " AGDA_EXEC
+    printf "What's the name of your Agda executable (default: agda)? "
+    read -r AGDA_EXEC
     if [ -z "$AGDA_EXEC" ]; then
       AGDA_EXEC=agda
     fi
     # Double check that the command exists
-    if ! [ -x "$(command -v $AGDA_EXEC)" ]; then
+    if ! [ -x "$(command -v "$AGDA_EXEC")" ]; then
       logUnhappy "'$AGDA_EXEC' is not a valid executable"
     else
       break
     fi
   done
-elif ! [ -x "$(command -v $AGDA_EXEC)" ]; then
+elif ! [ -x "$(command -v "$AGDA_EXEC")" ]; then
   throwError "'$AGDA_EXEC' is not a valid executable"
 fi
 
@@ -75,7 +68,7 @@ logHappy "Agda executable: $AGDA_EXEC"
 
 # Ask the executable for its version number
 # unless the caller has specified one
-if [ -z ${AGDA_VERSION-} ]; then
+if [ -z "${AGDA_VERSION-}" ]; then
   # There is a more recent "--numeric-version" option but old
   # versions of Agda do not implement it!
   AGDA_VERSION=$($AGDA_EXEC --version | head -n 1 | sed "s/^[a-zA-Z ]*\(2[0-9.]*\)\(-.*\)*$/\1/")
@@ -90,27 +83,27 @@ logHappy "Agda version number: $AGDA_VERSION"
 
 # Pick the install directory
 # unless the caller has specified one
-if [ -z ${AGDA_DIR-} ]; then
+if [ -z "${AGDA_DIR-}" ]; then
   AGDA_DIR=$($AGDA_EXEC --print-agda-app-dir | head -n 1 || true)
   if echo "$AGDA_DIR" | grep -Eq "^Error.*$"; then
     AGDA_DIR="$HOME/.agda"
   fi
-  read -p "Where do you want to install the library (default: $AGDA_DIR)? " AGDA_DIR_OVERWRITE
-  if ! [ -z "$AGDA_DIR_OVERWRITE" ]; then
+  printf "Where do you want to install the library (default: %s)? " "$AGDA_DIR"
+  read -r AGDA_DIR_OVERWRITE
+  if [ -n "$AGDA_DIR_OVERWRITE" ]; then
     AGDA_DIR="$AGDA_DIR_OVERWRITE"
   fi
 fi
 
 logHappy "Agda directory: $AGDA_DIR"
 
-if [ -z ${STDLIB_VERSION-} ]; then
+if [ -z "${STDLIB_VERSION-}" ]; then
   case "$AGDA_VERSION" in
     "2.8.0")   STDLIB_VERSION="2.3" ;;
     "2.7.0.1") STDLIB_VERSION="2.3" ;;
     "2.7.0")   STDLIB_VERSION="2.2" ;;
     "2.6.4.3") STDLIB_VERSION="2.1" ;;
     "2.6.4.2") STDLIB_VERSION="2.0" ;;
-    "2.6.4.2") STDLIB_VERSION="2.0" ;;
     "2.6.4.1") STDLIB_VERSION="2.0" ;;
     "2.6.4")   STDLIB_VERSION="2.0" ;;
     "2.6.3")   STDLIB_VERSION="1.7.3" ;;
@@ -145,7 +138,8 @@ logHappy "Successfully downloaded the standard library"
 if [ -d "$STDLIB_DIR_NAME" ]; then
   logWarning "The directory $AGDA_DIR/$STDLIB_DIR_NAME already exists."
   while true; do
-    read -p "Do you want to overwrite it? (yN) " DIR_OVERWRITE
+    printf "Do you want to overwrite it? (yN) "
+    read -r DIR_OVERWRITE
     DIR_OVERWRITE=${DIR_OVERWRITE:-n}
     case "$DIR_OVERWRITE" in
       [yY]*) DIR_OVERWRITE="y"; break;;

From 1f03bf6d30718bb091166705fe1d2fe88fbf02c5 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 10 Dec 2025 17:04:15 +0000
Subject: [PATCH 12/19] [ admin ] add a step to the release guide

---
 doc/release-guide.txt | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/doc/release-guide.txt b/doc/release-guide.txt
index 393eff79f3..aa419340af 100644
--- a/doc/release-guide.txt
+++ b/doc/release-guide.txt
@@ -57,6 +57,10 @@ procedure should be followed:
 * Submit a pull request to update the version of standard library on Homebrew
   (https://github.com/Homebrew/homebrew-core/blob/master/Formula/agda.rb)
 
+* Update the [install script](../stdlib-install.sh):
+
+  ** The big `case` block mapping Agda versions to stdlib versions
+
 * Update the Agda wiki:
 
   ** The standard library page.

From 1b6ff01ecf8bfbfe42e761e1d8f3ce7e01b80675 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 11 Dec 2025 13:47:14 +0000
Subject: [PATCH 13/19] [ more ] gracefully report that wget failed

---
 stdlib-install.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 75f16cf773..ecb5330961 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -131,7 +131,8 @@ mkdir -p logs
 STDLIB_DIR_NAME="agda-stdlib-$STDLIB_VERSION"
 STDLIB_TARBALL_NAME="/tmp/$STDLIB_DIR_NAME.tar.gz"
 STDLIB_TARBALL_URL="https://github.com/agda/agda-stdlib/archive/$STDLIB_TAG.tar.gz"
-wget -O "$STDLIB_TARBALL_NAME" "$STDLIB_TARBALL_URL" -o logs/wget
+
+wget -O "$STDLIB_TARBALL_NAME" "$STDLIB_TARBALL_URL" -o logs/wget || throwError "Download of $STDLIB_TARBALL_URL failed"
 
 logHappy "Successfully downloaded the standard library"
 

From 6e055c0869500c6e356523078602c81dd4c78a6a Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 11 Dec 2025 22:46:07 +0000
Subject: [PATCH 14/19] [ cleanup ] wording

---
 README.md                 | 3 ++-
 doc/installation-guide.md | 5 +++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index ae44ede8da..47e966f1d8 100644
--- a/README.md
+++ b/README.md
@@ -30,7 +30,8 @@ in glorious clickable HTML.
 
 ## Installation instructions
 
-On Unix-style systems, it should be as simple as
+On Unix-style systems, it should be as simple as running the following command in
+a shell:
 
 ```shell
 sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh))"
diff --git a/doc/installation-guide.md b/doc/installation-guide.md
index 0a4c4e4d49..c7cb1d93fb 100644
--- a/doc/installation-guide.md
+++ b/doc/installation-guide.md
@@ -7,9 +7,10 @@ Note: the full story on installing Agda libraries can be found at [readthedocs](
 ## Automated installation on Unix-style systems
 
 Running the following command in a terminal will download the
-[installation script](../stdlib-install.sh) and run. It will
+[installation script](../stdlib-install.sh) and run it. It will
 ask you some questions about your setup and automatically install
-a version of the stdlib compatible with your version of Agda.
+a version of the standard library compatible with your installed
+version of Agda.
 
 ```shell
 sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh))"

From d0eca1f9586553ec6246be296012339109cc6a89 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 11 Dec 2025 22:51:32 +0000
Subject: [PATCH 15/19] [ cleanup ] use variable rather than repetition

---
 stdlib-install.sh | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index ecb5330961..d7f8e5beed 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -156,18 +156,20 @@ else
   tar -zxvf "$STDLIB_TARBALL_NAME" > logs/tar
 fi
 
+
 # Adding the standard library to the list of installed and default libraries
 STDLIB_PATH="$AGDA_DIR/agda-stdlib-$STDLIB_VERSION/standard-library.agda-lib"
 AGDA_LIBRARIES_FILE="libraries-$AGDA_VERSION"
+AGDA_DEFAULTS_FILE="defaults-$AGDA_VERSION"
 
 touch "$AGDA_LIBRARIES_FILE"
 if ! grep -Eq "$STDLIB_PATH" "$AGDA_LIBRARIES_FILE"; then
   echo "$STDLIB_PATH" >> "$AGDA_LIBRARIES_FILE"
 fi
 
-touch "defaults-$AGDA_VERSION"
-if ! grep -Eq "^standard-library$" "defaults-$AGDA_VERSION"; then
-  echo "standard-library" >> "defaults-$AGDA_VERSION"
+touch "$AGDA_DEFAULTS_FILE"
+if ! grep -Eq "^standard-library$" "$AGDA_DEFAULTS_FILE"; then
+  echo "standard-library" >> "$AGDA_DEFAULTS_FILE"
 fi
 
 logHappy "Successfully installed the standard library"

From 4a762a6cc150d00c08014f62723a9820e1cda179 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 11 Dec 2025 22:56:31 +0000
Subject: [PATCH 16/19] [ doc ] more structure in the README

---
 README.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/README.md b/README.md
index 47e966f1d8..efdbd9bbb4 100644
--- a/README.md
+++ b/README.md
@@ -30,6 +30,8 @@ in glorious clickable HTML.
 
 ## Installation instructions
 
+### Automated installation (currently experimental)
+
 On Unix-style systems, it should be as simple as running the following command in
 a shell:
 
@@ -37,6 +39,8 @@ a shell:
 sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh))"
 ```
 
+### Manual installation
+
 See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/doc/installation-guide.md) for the latest version of the standard library.
 
 #### Old versions of Agda

From 732160fc72b8d0faa99b02fb265942c8def0e237 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 12 Dec 2025 00:59:26 +0000
Subject: [PATCH 17/19] [ fix ] remove redundant full stop

---
 stdlib-install.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index d7f8e5beed..70f425fa31 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -137,7 +137,7 @@ wget -O "$STDLIB_TARBALL_NAME" "$STDLIB_TARBALL_URL" -o logs/wget || throwError
 logHappy "Successfully downloaded the standard library"
 
 if [ -d "$STDLIB_DIR_NAME" ]; then
-  logWarning "The directory $AGDA_DIR/$STDLIB_DIR_NAME already exists."
+  logWarning "The directory $AGDA_DIR/$STDLIB_DIR_NAME already exists"
   while true; do
     printf "Do you want to overwrite it? (yN) "
     read -r DIR_OVERWRITE
@@ -145,7 +145,7 @@ if [ -d "$STDLIB_DIR_NAME" ]; then
     case "$DIR_OVERWRITE" in
       [yY]*) DIR_OVERWRITE="y"; break;;
       [nN]*) DIR_OVERWRITE="n"; break;;
-      *) logUnhappy "Invalid answer: '$DIR_OVERWRITE'. Please answer y or n.";;
+      *) logUnhappy "Invalid answer: '$DIR_OVERWRITE'. Please answer y or n";;
     esac
   done
   if [ "$DIR_OVERWRITE" = "y" ]; then

From 664159eac28a43622c3b7a1ae9b5cd31500256fe Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 12 Dec 2025 14:36:58 +0000
Subject: [PATCH 18/19] [ fix ] defaults-X.Y.Z is not supported yet

I'll open a PR to Agda to add it to the next releases.
---
 stdlib-install.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/stdlib-install.sh b/stdlib-install.sh
index 70f425fa31..2043f01ec1 100644
--- a/stdlib-install.sh
+++ b/stdlib-install.sh
@@ -160,7 +160,9 @@ fi
 # Adding the standard library to the list of installed and default libraries
 STDLIB_PATH="$AGDA_DIR/agda-stdlib-$STDLIB_VERSION/standard-library.agda-lib"
 AGDA_LIBRARIES_FILE="libraries-$AGDA_VERSION"
-AGDA_DEFAULTS_FILE="defaults-$AGDA_VERSION"
+# For now we shove it in the 'defaults' file as using a version-specific
+# "defaults-$AGDA_VERSION" is not supported yet by Agda :(
+AGDA_DEFAULTS_FILE="defaults"
 
 touch "$AGDA_LIBRARIES_FILE"
 if ! grep -Eq "$STDLIB_PATH" "$AGDA_LIBRARIES_FILE"; then

From 04ebb84fceaf4c0ab963a66484528fb0dbaa47f2 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 17 Dec 2025 13:24:09 +0000
Subject: [PATCH 19/19] [ fix ] nasty typo

---
 README.md                 | 2 +-
 doc/installation-guide.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index efdbd9bbb4..dae4178e23 100644
--- a/README.md
+++ b/README.md
@@ -36,7 +36,7 @@ On Unix-style systems, it should be as simple as running the following command i
 a shell:
 
 ```shell
-sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh))"
+sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh)"
 ```
 
 ### Manual installation
diff --git a/doc/installation-guide.md b/doc/installation-guide.md
index c7cb1d93fb..adc96301ba 100644
--- a/doc/installation-guide.md
+++ b/doc/installation-guide.md
@@ -13,7 +13,7 @@ a version of the standard library compatible with your installed
 version of Agda.
 
 ```shell
-sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh))"
+sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh)"
 ```
 
 ## Manual installation