chore: update Lean version + attr fixes

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
 

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

lakefile.lean

@@ -5,7 +5,7 @@ package lake
 
 lean_lib Lake
 
-@[defaultTarget]
+@[default_target]
 lean_exe lake where
   root := `Lake.Main
   supportInterpreter := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-08-05
+leanprover/lean4:nightly-2022-10-20

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