chore: update to Lean v4.3.0

.gitignore

@@ -1,2 +1 @@
-/build
-/lakefile.olean
+/.lake

Alloy/Util/ShimElab.lean

@@ -47,7 +47,7 @@ where
   go stx :=
     withRef stx <| withIncRecDepth <| withFreshMacroScope do
       withTraceNode `ShimElab.step (fun _ => return stx) do
-        liftCoreM <| checkMaxHeartbeats "elaborator"
+        liftCoreM <| checkSystem "elaborator"
         if let some (decl, stxNew?) ← liftMacroM <| expandMacroImpl? (← getEnv) stx then
           withInfoTreeContext (mkInfoTree := mkCommandElabInfoTree decl stx) do
             let stxNew ← liftMacroM <| liftExcept stxNew?

examples/S/.gitignore

@@ -1,4 +1,2 @@
-/build
-/lakefile.olean
-/lake-packages/*
+/.lake
 lake-manifest.json

examples/S/lakefile.lean

@@ -8,14 +8,12 @@ package s {
 require alloy from ".."/".."
 
 module_data alloy.c.o : BuildJob FilePath
-lean_lib S {
+lean_lib S where
   precompileModules := true
   nativeFacets := #[Module.oFacet, `alloy.c.o]
-}
 
 @[default_target]
-lean_exe s {
+lean_exe s where
   root := `Main
-}
 
 lean_lib Test

examples/S/test.sh

@@ -1,6 +1,6 @@
 set -ex
-rm -rf build
+rm -rf .lake
 LAKE=${LAKE:-lake}
 $LAKE build -U
 $LAKE build Test -v
-#build/bin/s # TODO: Segfaults for some reason
+#.lake/build/bin/s # TODO: Segfaults for some reason

examples/my_add/.gitignore

@@ -1,4 +1,2 @@
-/build
-/lakefile.olean
-/lake-packages/*
+/.lake
 lake-manifest.json

examples/my_add/lakefile.lean

@@ -6,14 +6,12 @@ package my_add
 require alloy from ".."/".."
 
 module_data alloy.c.o : BuildJob FilePath
-lean_lib MyAdd {
+lean_lib MyAdd where
   precompileModules := true
   nativeFacets := #[Module.oFacet, `alloy.c.o]
-}
 
 lean_lib Test
 
 @[default_target]
-lean_exe my_add {
+lean_exe my_add where
   root := `Main
-}

examples/my_add/test.sh

@@ -1,6 +1,6 @@
 set -ex
-rm -rf build
+rm -rf .lake
 LAKE=${LAKE:-lake}
 $LAKE build -U
 $LAKE build Test -v
-build/bin/my_add
+.lake/build/bin/my_add

lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "alloy",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -15,10 +15,9 @@ package alloy
 lean_lib Alloy
 
 @[default_target]
-lean_exe alloy {
+lean_exe alloy where
   root := `Main
   supportInterpreter := true
-}
 
 --------------------------------------------------------------------------------
 -- # Module Facets

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.1.0
+leanprover/lean4:4.3.0

test.sh

@@ -15,6 +15,6 @@ pushd tests/compile
 ./test.sh
 popd
 
-find tests/run -type f -exec ${LAKE:-lake} env lean {} \;
+find tests/run -type f | xargs -n1 ${LAKE:-lake} env lean
 
 echo "all done"

tests/compile/.gitignore

@@ -1,4 +1,2 @@
-/build
-/lake-packages/*
+/.lake
 lake-manifest.json
-lakefile.olean

tests/compile/test.sh

@@ -3,4 +3,4 @@ rm -rf build
 LAKE=${LAKE:-lake}
 $LAKE build -U
 $LAKE build Eval -v
-build/bin/run
+.lake/build/bin/run

tests/run/parseLeanH.lean

@@ -3,21 +3,27 @@ import Lean.Elab.Command
 
 open Lean Parser Elab Command
 
-/- By  Mario: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Undefine.20lambda/near/393694214-/
-def Lean.Parser.Trie.isEmpty {α} (t : Trie α) : Bool := t matches .Node none .leaf
-partial def Lean.Parser.Trie.erase {α} (t : Trie α) (s : String) : Trie α :=
-  let rec loop : Trie α → String.Pos → Option (Trie α)
-    | ⟨val, m⟩, i =>
-      match s.atEnd i with
-      | true  => some (Trie.Node none m)
-      | false => do
-        let c := s.get i
-        let i := s.next i
-        let t ← m.find compare c
-        let t ← loop t i
-        let m := if t.isEmpty then m.erase compare c else m.insert compare c t
-        some ⟨val, m⟩
-  (loop t 0).getD t
+partial def Lean.Data.Trie.erase {α} (t : Trie α) (s : String) : Trie α :=
+  let rec loop : Nat → Trie α → Trie α
+    | i, leaf v =>
+      if i < s.utf8ByteSize then leaf v else leaf none
+    | i, node1 v c' t' =>
+      if h : i < s.utf8ByteSize then
+        if c' = s.getUtf8Byte i h then
+          loop (i+1) t'
+        else
+          node1 v c' t'
+      else
+        node1 none c' t'
+    | i, node v cs ts =>
+      if h : i < s.utf8ByteSize then
+        let c := s.getUtf8Byte i h
+        match cs.findIdx? (· == c) with
+        | none => node v cs ts
+        | some idx => node v cs <| ts.setD idx <| loop (i+1) (ts.get! idx)
+      else
+        node none cs ts
+  loop 0 t
 
 syntax "LEAN_CASSERT" "(" cExpr ")" ";" : cCmd
 syntax "extern" str "{" : cCmd