chore: clean up after update-stage0

leanprover · Nov 19, 2024 · e0353ed · e0353ed
1 parent 3d6a644
commit e0353ed
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -705,7 +705,7 @@ if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     DEPENDS lake_lib
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
     VERBATIM)
-  add_custom_target(lake #ALL
+  add_custom_target(lake ALL
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS lake_shared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake

diff --git a/tests/lean/prvCtor.lean b/tests/lean/prvCtor.lean
@@ -22,7 +22,7 @@ open Lean in
 open Lean in
 #eval id (α := CoreM Unit) do
   -- this implementation is no longer allowed because of a private constructor
-  modifyEnv fun env => { env with header.mainModule := `foo }
+  modifyEnv fun env => { env with base.header.mainModule := `foo }
 
 #check a -- Error
 

diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean
@@ -24,7 +24,7 @@ inductive D
   | mk (x y z : Nat) : D
 
 /--
-info: #[base, const2ModIdx, extensions, extraConstNames, header]
+info: #[constants, quotInit, diagnostics, const2ModIdx, extensions, extraConstNames, header]
 #[toS2, toS1, x, y, z, toS3, w, s]
 (some [S4.toS2, S2.toS1])
 #[S2, S3]
@@ -33,7 +33,7 @@ info: #[base, const2ModIdx, extensions, extraConstNames, header]
 #guard_msgs in
 #eval show CoreM Unit from do
   let env ← getEnv
-  IO.println (getStructureFields env `Lean.Environment)
+  IO.println (getStructureFields env ``Kernel.Environment)
   check $ getStructureFields env `S4 == #[`toS2, `toS3, `s]
   check $ getStructureFields env `S1 == #[`x, `y]
   check $ isSubobjectField? env `S4 `toS2 == some `S2