chore: update stage0

stage0/src/Init/Prelude.lean

@@ -196,6 +196,8 @@ theorem ne_true_of_eq_false : {b : Bool} → Eq b false → Not (Eq b true)
 class Inhabited (α : Sort u) where
   mk {} :: (default : α)
 
+export Inhabited (default)
+
 class inductive Nonempty (α : Sort u) : Prop where
   | intro (val : α) : Nonempty α
 
@@ -242,12 +244,12 @@ theorem PLift.down_up {α : Sort u} (a : α) : Eq (down (up a)) a :=
   rfl
 
 /- Pointed types -/
-def PointedType := Subtype fun α : Type u => Nonempty α
+def NonemptyType := Subtype fun α : Type u => Nonempty α
 
-abbrev PointedType.type (type : PointedType.{u}) : Type u :=
+abbrev NonemptyType.type (type : NonemptyType.{u}) : Type u :=
   type.val
 
-instance : Inhabited PointedType.{u} where
+instance : Inhabited NonemptyType.{u} where
   default := ⟨PUnit.{u+1}, Nonempty.intro ⟨⟩⟩
 
 /-- Universe lifting operation -/
@@ -2164,7 +2166,7 @@ def maxRecDepthErrorMessage : String :=
 namespace Macro
 
 /- References -/
-private constant MethodsRefPointed : PointedType.{0}
+private constant MethodsRefPointed : NonemptyType.{0}
 
 private def MethodsRef : Type := MethodsRefPointed.type
 

stage0/src/Init/System/ST.lean

@@ -42,7 +42,7 @@ instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s =>
 namespace ST
 
 /- References -/
-constant RefPointed : PointedType.{0}
+constant RefPointed : NonemptyType.{0}
 
 structure Ref (σ : Type) (α : Type) : Type where
   ref : RefPointed.type

stage0/src/Lean/Environment.lean

@@ -43,6 +43,21 @@ constant CompactedRegion.isMemoryMapped : CompactedRegion → Bool
 @[extern "lean_compacted_region_free"]
 unsafe constant CompactedRegion.free : CompactedRegion → IO Unit
 
+/- Opaque persistent environment extension entry. -/
+constant EnvExtensionEntrySpec : NonemptyType.{0}
+def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type
+instance : Nonempty EnvExtensionEntry := EnvExtensionEntrySpec.property
+
+/- Content of a .olean file.
+   We use `compact.cpp` to generate the image of this object in disk. -/
+structure ModuleData where
+  imports    : Array Import
+  constants  : Array ConstantInfo
+  entries    : Array (Name × Array EnvExtensionEntry)
+
+instance : Inhabited ModuleData :=
+  ⟨{imports := arbitrary, constants := arbitrary, entries := arbitrary }⟩
+
 /- Environment fields that are not used often. -/
 structure EnvironmentHeader where
   trustLevel   : UInt32       := 0
@@ -51,6 +66,7 @@ structure EnvironmentHeader where
   imports      : Array Import := #[] -- direct imports
   regions      : Array CompactedRegion := #[] -- compacted regions of all imported modules
   moduleNames  : Array Name   := #[] -- names of all imported modules
+  moduleData   : Array ModuleData := #[] -- ModuleData of all imported modules
   deriving Inhabited
 
 open Std (HashMap)
@@ -318,11 +334,6 @@ structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) where
   exportEntriesFn : σ → Array α
   statsFn         : σ → Format
 
-/- Opaque persistent environment extension entry. -/
-constant EnvExtensionEntrySpec : PointedType.{0}
-def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type
-instance : Nonempty EnvExtensionEntry := EnvExtensionEntrySpec.property
-
 instance {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
   ⟨{importedEntries := #[], state := arbitrary }⟩
 
@@ -496,16 +507,6 @@ def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environmen
 
 end MapDeclarationExtension
 
-/- Content of a .olean file.
-   We use `compact.cpp` to generate the image of this object in disk. -/
-structure ModuleData where
-  imports    : Array Import
-  constants  : Array ConstantInfo
-  entries    : Array (Name × Array EnvExtensionEntry)
-
-instance : Inhabited ModuleData :=
-  ⟨{imports := arbitrary, constants := arbitrary, entries := arbitrary }⟩
-
 @[extern "lean_save_module_data"]
 constant saveModuleData (fname : @& System.FilePath) (mod : @& Name) (data : @& ModuleData) : IO Unit
 @[extern "lean_read_module_data"]
@@ -642,6 +643,7 @@ partial def importModules (imports : List Import) (opts : Options) (trustLevel :
         imports      := imports.toArray,
         regions      := s.regions,
         moduleNames  := s.moduleNames
+        moduleData   := s.moduleData
       }
     }
     let env ← setImportedEntries env s.moduleData

stage0/src/Lean/Parser/Term.lean

@@ -243,6 +243,7 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 @[builtinTermParser] def waitIfContainsMVar     := leading_parser "wait_if_contains_mvar% " >> "?" >> ident >> "; " >> termParser
 
 @[builtinTermParser] def arbitraryOrOfNonempty := leading_parser "arbitrary_or_ofNonempty%"
+@[builtinTermParser] def defaultOrOfNonempty   := leading_parser "default_or_ofNonempty%"
 
 def namedArgument  := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
 def ellipsis       := leading_parser ".."

stage0/src/Std/ShareCommon.lean

@@ -86,7 +86,7 @@ unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : O
   @PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
 
 /- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/
-constant StatePointed : PointedType
+constant StatePointed : NonemptyType
 abbrev State : Type u := StatePointed.type
 @[extern "lean_sharecommon_mk_state"]
 constant mkState : Unit → State := fun _ => Classical.choice StatePointed.property
@@ -94,7 +94,7 @@ def State.empty : State := mkState ()
 instance State.inhabited : Inhabited State := ⟨State.empty⟩
 
 /- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/
-constant PersistentStatePointed : PointedType
+constant PersistentStatePointed : NonemptyType
 abbrev PersistentState : Type u := PersistentStatePointed.type
 @[extern "lean_sharecommon_mk_pstate"]
 constant mkPersistentState : Unit → PersistentState := fun _ => Classical.choice PersistentStatePointed.property

stage0/stdlib/Init/Prelude.c

@@ -517,6 +517,7 @@ uint8_t lean_uint32_dec_eq(uint32_t, uint32_t);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_EStateM_nonBacktrackable___closed__3;
 LEAN_EXPORT lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux(lean_object*);
+LEAN_EXPORT lean_object* l_instInhabitedNonemptyType;
 LEAN_EXPORT lean_object* l_instHMul(lean_object*);
 LEAN_EXPORT lean_object* l_Substring_bsize___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_List_redLength___rarg(lean_object*);
@@ -555,7 +556,6 @@ LEAN_EXPORT lean_object* l_max(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Macro_withIncRecDepth(lean_object*);
 static lean_object* l_Lean_Name_instBEqName___closed__1;
 LEAN_EXPORT lean_object* l_EStateM_adaptExcept___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_instInhabitedPointedType;
 LEAN_EXPORT lean_object* l_Lean_Syntax_getArgs(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Name_append(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Applicative_map___default(lean_object*);
@@ -1180,7 +1180,7 @@ x_1 = 0;
 return x_1;
 }
 }
-static lean_object* _init_l_instInhabitedPointedType() {
+static lean_object* _init_l_instInhabitedNonemptyType() {
 _start:
 {
 return lean_box(0);
@@ -10476,7 +10476,7 @@ l_Unit_unit = _init_l_Unit_unit();
 lean_mark_persistent(l_Unit_unit);
 l_instInhabitedSort = _init_l_instInhabitedSort();
 l_instInhabitedBool = _init_l_instInhabitedBool();
-l_instInhabitedPointedType = _init_l_instInhabitedPointedType();
+l_instInhabitedNonemptyType = _init_l_instInhabitedNonemptyType();
 l_instInhabitedNat = _init_l_instInhabitedNat();
 lean_mark_persistent(l_instInhabitedNat);
 l_instAddNat___closed__1 = _init_l_instAddNat___closed__1();

stage0/stdlib/Lean/CoreM.c

@@ -523,13 +523,14 @@ x_1 = l_Lean_Core_instInhabitedState___closed__7;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Core_instInhabitedState___closed__6;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }

stage0/stdlib/Lean/Elab/Command.c

@@ -1033,13 +1033,14 @@ x_1 = l_Lean_Elab_Command_instInhabitedState___closed__4;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Elab_Command_Scope_varDecls___default___closed__1;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }

stage0/stdlib/Lean/Elab/InfoTree.c

@@ -551,13 +551,14 @@ x_1 = l_Lean_Elab_instInhabitedContextInfo___closed__4;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Elab_instInhabitedContextInfo___closed__3;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }

stage0/stdlib/Lean/Elab/Term.c

@@ -2173,13 +2173,14 @@ x_1 = l_Lean_Elab_Term_instInhabitedSavedState___closed__4;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Elab_Term_instInhabitedState___closed__1;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }

stage0/stdlib/Lean/Meta/Basic.c

@@ -1940,13 +1940,14 @@ x_1 = l_Lean_Meta_instInhabitedSavedState___closed__3;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Meta_ParamInfo_backDeps___default___closed__1;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }

stage0/stdlib/Lean/Server/Snapshots.c

@@ -220,13 +220,14 @@ x_1 = l_Lean_Server_Snapshots_instInhabitedSnapshot___closed__8;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Server_Snapshots_instInhabitedSnapshot___closed__7;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }

stage0/stdlib/Lean/Widget/InteractiveCode.c

@@ -225,13 +225,14 @@ x_1 = l_Lean_Widget_instInhabitedInfoWithCtx___closed__7;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Widget_instInhabitedInfoWithCtx___closed__6;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }

stage0/stdlib/Lean/Widget/InteractiveDiagnostic.c

@@ -13298,13 +13298,14 @@ x_1 = l_Lean_Widget_instInhabitedEmbedFmt___closed__7;
 x_2 = 0;
 x_3 = lean_box(0);
 x_4 = l_Lean_Widget_instInhabitedEmbedFmt___closed__6;
-x_5 = lean_alloc_ctor(0, 4, 5);
+x_5 = lean_alloc_ctor(0, 5, 5);
 lean_ctor_set(x_5, 0, x_3);
 lean_ctor_set(x_5, 1, x_4);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set(x_5, 3, x_4);
-lean_ctor_set_uint32(x_5, sizeof(void*)*4, x_1);
-lean_ctor_set_uint8(x_5, sizeof(void*)*4 + 4, x_2);
+lean_ctor_set(x_5, 4, x_4);
+lean_ctor_set_uint32(x_5, sizeof(void*)*5, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5 + 4, x_2);
 return x_5;
 }
 }