From 9a7e068c74025feb38964adc8981f25e3369c71d Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 21 Dec 2023 14:24:44 +1100
Subject: [PATCH] nightly-2023-12-20

---
 lean-toolchain                  | 2 +-
 test/Mathlib/lake-manifest.json | 8 ++++----
 test/Mathlib/lakefile.lean      | 2 +-
 test/Mathlib/lean-toolchain     | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/lean-toolchain b/lean-toolchain
index 91ccf6a..2b934e4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4:nightly-2023-12-20
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
index 58b01c1..00b2872 100644
--- a/test/Mathlib/lake-manifest.json
+++ b/test/Mathlib/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "baf6defee1fe881ae535519c0776f37f6ef08603",
+   "rev": "f6dd208c78ee34449a029951d16a8fd161959385",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -49,10 +49,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "561ab0981d6df710afb3d34423378152195e3440",
+   "rev": "ae134c75cbc18b879764b22634291ad95afcb7fe",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing-2023-12-20",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«repl-mathlib-tests»",
diff --git a/test/Mathlib/lakefile.lean b/test/Mathlib/lakefile.lean
index a08a1df..8d41325 100644
--- a/test/Mathlib/lakefile.lean
+++ b/test/Mathlib/lakefile.lean
@@ -3,7 +3,7 @@ open Lake DSL
 
 package «repl-mathlib-tests» where
   -- add package configuration options here
-  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "nightly-testing-2023-12-20"
 
 lean_lib «ReplMathlibTests» where
   -- add library configuration options here
diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
index 91ccf6a..2b934e4 100644
--- a/test/Mathlib/lean-toolchain
+++ b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4:nightly-2023-12-20