From 25fe4a6f4d8ee98bebf33697c9fc3e753a26b90c Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 20 Oct 2022 12:20:57 -0400
Subject: [PATCH] chore: update Lean version + attr fixes

---
 README.md                        | 4 ++--
 examples/bootstrap/lakefile.lean | 2 +-
 lakefile.lean                    | 2 +-
 lean-toolchain                   | 2 +-
 test/62/test.sh                  | 7 +++++++
 5 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 28715b50af..ae7505b777 100644
--- a/README.md
+++ b/README.md
@@ -86,7 +86,7 @@ lean_lib Hello {
   -- add library configuration options here
 }
 
-@[defaultTarget]
+@[default_target]
 lean_exe hello {
   root := `Main
 }
@@ -164,7 +164,7 @@ The archive's full file name will end up being `nameToArchive buildArchive?`.
 
 ## Defining Build Targets
 
-A Lake package can have many build targets, such as different Lean libraries and multiple binary executables. Any number of these declarations can be marked with the `@[defaultTarget]` attribute to tell Lake to build them on a bare `lake build` of the package.
+A Lake package can have many build targets, such as different Lean libraries and multiple binary executables. Any number of these declarations can be marked with the `@[default_target]` attribute to tell Lake to build them on a bare `lake build` of the package.
 
 ### Lean Libraries
 
diff --git a/examples/bootstrap/lakefile.lean b/examples/bootstrap/lakefile.lean
index 2403582b61..3b44e08530 100644
--- a/examples/bootstrap/lakefile.lean
+++ b/examples/bootstrap/lakefile.lean
@@ -6,7 +6,7 @@ package lake where
 
 lean_lib Lake
 
-@[defaultTarget]
+@[default_target]
 lean_exe lake where
   root := `Lake.Main
   supportInterpreter := true
diff --git a/lakefile.lean b/lakefile.lean
index d13369d86b..e43a7760e1 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,7 +5,7 @@ package lake
 
 lean_lib Lake
 
-@[defaultTarget]
+@[default_target]
 lean_exe lake where
   root := `Lake.Main
   supportInterpreter := true
diff --git a/lean-toolchain b/lean-toolchain
index f06bd53924..253e2446c5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-08-05
+leanprover/lean4:nightly-2022-10-20
diff --git a/test/62/test.sh b/test/62/test.sh
index 8074d2bd59..df28e46389 100755
--- a/test/62/test.sh
+++ b/test/62/test.sh
@@ -4,9 +4,16 @@ set -euxo pipefail
 # skip if no elan found
 command -v elan > /dev/null || (echo "elan not found; skipping test"; exit 0)
 
+if [ "`uname`" = Darwin ]; then
+  sed_i() { sed -i '' "$@"; }
+else
+  sed_i() { sed -i "$@"; }
+fi
+
 ./clean.sh
 lake +leanprover/lean4:nightly-2022-06-30 new foo
 cd foo
 lake +leanprover/lean4:nightly-2022-06-30 build | grep -m1 foo
 cp ../../../lean-toolchain lean-toolchain
+sed_i 's/defaultTarget/default_target/g' lakefile.lean
 ${LAKE:-../../../build/bin/lake} build -v | grep -m1 foo