Merge remote-tracking branch 'origin/main' into son/tutorial

backends/lean/Base/Diverge/Elab.lean

@@ -10,9 +10,6 @@ namespace Diverge
 /- Automating the generation of the encoding and the proofs so as to use nice
    syntactic sugar. -/
 
-syntax (name := divergentDef)
-  declModifiers "divergent" "def" declId ppIndent(optDeclSig) declVal : command
-
 open Lean Elab Term Meta Primitives Lean.Meta
 open Utils
 
@@ -1389,17 +1386,43 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
         else return ()
       catch _ => s.restore
 
--- The following two functions are copy-pasted from Lean.Elab.MutualDef
-
+-- The following three functions are copy-pasted from Lean.Elab.MutualDef.lean
 open private elabHeaders levelMVarToParamHeaders getAllUserLevelNames withFunLocalDecls elabFunValues
   instantiateMVarsAtHeader instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes withUsed from Lean.Elab.MutualDef
 
+-- Copy/pasted from Lean.Elab.Term.withHeaderSecVars (because the definition is private)
+private def Term.withHeaderSecVars {α} (vars : Array Expr) (includedVars : List Name) (headers : Array DefViewElabHeader)
+    (k : Array Expr → TermElabM α) : TermElabM α := do
+  let (_, used) ← collectUsed.run {}
+  let (lctx, localInsts, vars) ← removeUnused vars used
+  withLCtx lctx localInsts <| k vars
+where
+  collectUsed : StateRefT CollectFVars.State MetaM Unit := do
+    -- directly referenced in headers
+    headers.forM (·.type.collectFVars)
+    -- included by `include`
+    vars.forM fun var => do
+      let ldecl ← getFVarLocalDecl var
+      if includedVars.contains ldecl.userName then
+        modify (·.add ldecl.fvarId)
+    -- transitively referenced
+    get >>= (·.addDependencies) >>= set
+    -- instances (`addDependencies` unnecessary as by definition they may only reference variables
+    -- already included)
+    vars.forM fun var => do
+      let ldecl ← getFVarLocalDecl var
+      let st ← get
+      if ldecl.binderInfo.isInstImplicit && (← getFVars ldecl.type).all st.fvarSet.contains then
+        modify (·.add ldecl.fvarId)
+  getFVars (e : Expr) : MetaM (Array FVarId) :=
+    (·.2.fvarIds) <$> e.collectFVars.run {}
+
 -- Comes from Term.isExample
 def isExample (views : Array DefView) : Bool :=
   views.any (·.kind.isExample)
 
 open Language in
-def Term.elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
+def Term.elabMutualDef (vars : Array Expr) (includedVars : List Name) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
       -- save correct environment in info tree
@@ -1418,7 +1441,7 @@ where
       withFunLocalDecls headers fun funFVars => do
         for view in views, funFVar in funFVars do
           addLocalVarInfo view.declId funFVar
-          -- Modification 1:
+          -- MODIFICATION 1:
           -- Add fake use site to prevent "unused variable" warning (if the
           -- function is actually not recursive, Lean would print this warning).
           -- Remark: we could detect this case and encode the function without
@@ -1428,7 +1451,7 @@ where
           addTermInfo' view.declId funFVar
         let values ←
           try
-            let values ← elabFunValues headers
+            let values ← elabFunValues headers vars includedVars
             Term.synthesizeSyntheticMVarsNoPostponing
             values.mapM (instantiateMVars ·)
           catch ex =>
@@ -1438,18 +1461,23 @@ where
         let letRecsToLift ← getLetRecsToLift
         let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
         checkLetRecsToLiftTypes funFVars letRecsToLift
-        withUsed vars headers values letRecsToLift fun vars => do
+        (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars headers else withUsed vars headers values letRecsToLift) fun vars => do
           let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
           for preDef in preDefs do
             trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
           let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
           let preDefs ← instantiateMVarsAtPreDecls preDefs
+          let preDefs ← shareCommonPreDefs preDefs
           let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
           for preDef in preDefs do
             trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
           checkForHiddenUnivLevels allUserLevelNames preDefs
-          addPreDefinitions preDefs -- Modification 2: we use our custom function here
+          addPreDefinitions preDefs -- MODIFICATION 2: we use our custom function here
           processDeriving headers
+      for view in views, header in headers do
+        -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
+        -- that depends only on a part of the ref
+        addDeclarationRanges header.declName view.ref
 
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do
@@ -1460,22 +1488,61 @@ where
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"
 
+#check Command.elabMutualDef
+
+-- Copy/pasted from Lean.Elab.MutualDef
 open Command in
+open Language in
 def Command.elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
-  let views ← ds.mapM fun d => do
-    let `($mods:declModifiers divergent def $id:declId $sig:optDeclSig $val:declVal) := d
-      | throwUnsupportedSyntax
-    let modifiers ← elabModifiers mods
-    let (binders, type) := expandOptDeclSig sig
-    let deriving? := none
-    let headerRef := Syntax.missing -- Not sure what to put here
-    pure { ref := d, kind := DefKind.def, headerRef, modifiers,
-           declId := id, binders, type? := type, value := val, deriving? }
-  runTermElabM fun vars => Term.elabMutualDef vars views
+  let opts ← getOptions
+  withAlwaysResolvedPromises ds.size fun headerPromises => do
+    let snap? := (← read).snap?
+    let mut views := #[]
+    let mut defs := #[]
+    let mut reusedAllHeaders := true
+    for h : i in [0:ds.size], headerPromise in headerPromises do
+      let d := ds[i]
+      let modifiers ← elabModifiers d[0]
+      if ds.size > 1 && modifiers.isNonrec then
+        throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
+      let mut view ← mkDefView modifiers d[2] -- MODIFICATION: changed the index to 2
+      let fullHeaderRef := mkNullNode #[d[0], view.headerRef]
+      if let some snap := snap? then
+        view := { view with headerSnap? := some {
+          old? := do
+            -- transitioning from `Context.snap?` to `DefView.headerSnap?` invariant: if the
+            -- elaboration context and state are unchanged, and the syntax of this as well as all
+            -- previous headers is unchanged, then the elaboration result for this header (which
+            -- includes state from elaboration of previous headers!) should be unchanged.
+            guard reusedAllHeaders
+            let old ← snap.old?
+            -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick
+            let old ← old.val.get.toTyped? DefsParsedSnapshot
+            let oldParsed ← old.defs[i]?
+            guard <| fullHeaderRef.eqWithInfoAndTraceReuse opts oldParsed.fullHeaderRef
+            -- no syntax guard to store, we already did the necessary checks
+            return ⟨.missing, oldParsed.headerProcessedSnap⟩
+          new := headerPromise
+        } }
+        defs := defs.push {
+          fullHeaderRef
+          headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result }
+        }
+        reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
+      views := views.push view
+    if let some snap := snap? then
+      -- no non-fatal diagnostics at this point
+      snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
+    let includedVars := (← getScope).includedVars
+    runTermElabM fun vars => Term.elabMutualDef vars includedVars views
+
+syntax (name := divergentDef)
+  declModifiers "divergent" Lean.Parser.Command.definition : command
 
 -- Special command so that we don't fall back to the built-in mutual when we produce an error.
 local syntax "_divergent" Parser.Command.mutual : command
-elab_rules : command | `(_divergent mutual $decls* end) => Command.elabMutualDef decls
+elab_rules : command
+  | `(_divergent mutual $decls* end) => Command.elabMutualDef decls
 
 macro_rules
   | `(mutual $decls* end) => do
@@ -1501,6 +1568,8 @@ namespace Tests
 
   /- Some examples of partial functions -/
 
+  -- set_option trace.Diverge true
+  -- set_option pp.rawOnError true
   --set_option trace.Diverge.def true
   --set_option trace.Diverge.def.genBody true
   --set_option trace.Diverge.def.valid true

backends/lean/Base/Primitives/Core.lean

@@ -74,3 +74,10 @@ end core
 
 /- [core::option::Option::is_none] -/
 @[simp] def core.option.Option.is_none (T: Type) (self: Option T): Bool := self.isNone
+
+/- [core::clone::Clone::clone_from]:
+   Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43
+   Name pattern: core::clone::Clone::clone_from -/
+@[simp] def core.clone.Clone.clone_from
+  {Self : Type} (cloneInst : core.clone.Clone Self) (_self : Self) (source : Self) : Result Self :=
+  cloneInst.clone source

backends/lean/Base/Utils.lean

@@ -869,7 +869,7 @@ def evalAesopSaturate (options : Aesop.Options') (ruleSets : Array Name) : Tacti
   let rss ← Aesop.Frontend.getGlobalRuleSets ruleSets
   let rs ← Aesop.mkLocalRuleSet rss options
     |> Aesop.ElabM.runForwardElab (← getMainGoal)
-  tryLiftMetaTactic1 (Aesop.saturate rs · |>.run { options }) "Aesop.saturate failed"
+  tryLiftMetaTactic1 (Aesop.saturate rs · options) "Aesop.saturate failed"
 
 /-- Normalize the let-bindings by inlining them -/
 def normalizeLetBindings (e : Expr) : MetaM Expr :=

backends/lean/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e242f1edcacf917f40fae9b81f57f4bd0a4e45ac",
+   "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

backends/lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.11.0-rc2

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-962f26311ccdf09a6a3cfeacbccafba22bf3d405
+cdc1dcde447a50cbc20336c79b21b42ac977b7fd

compiler/Assumed.ml

@@ -200,8 +200,7 @@ module Sig = struct
     mk_sig generics inputs output
 end
 
-type raw_assumed_fun_info =
-  assumed_fun_id * fun_sig * bool * string * bool list option
+type raw_assumed_fun_info = assumed_fun_id * fun_sig * bool * bool list option
 
 type assumed_fun_info = {
   fun_id : assumed_fun_id;
@@ -217,7 +216,8 @@ type assumed_fun_info = {
 }
 
 let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info =
-  let fun_id, fun_sig, can_fail, name, keep_types = raw in
+  let fun_id, fun_sig, can_fail, keep_types = raw in
+  let name = Charon.PrintExpressions.assumed_fun_id_to_string fun_id in
   { fun_id; fun_sig; can_fail; name; keep_types }
 
 (** The list of assumed functions and all their information:
@@ -235,44 +235,29 @@ let raw_assumed_fun_infos : raw_assumed_fun_info list =
   [
     (* TODO: the names are not correct ("Box" should be an impl elem for instance)
        but it's not important) *)
-    ( BoxNew,
-      Sig.box_new_sig,
-      false,
-      "alloc::boxed::Box::new",
-      Some [ true; false ] );
-    (* BoxFree shouldn't be used *)
-    ( BoxFree,
-      Sig.box_free_sig,
-      false,
-      "alloc::boxed::Box::free",
-      Some [ true; false ] );
-    (* Array Index *)
-    ( ArrayIndexShared,
+    (BoxNew, Sig.box_new_sig, false, Some [ true; false ]);
+    (* Array to slice*)
+    (ArrayToSliceShared, Sig.array_to_slice_sig false, true, None);
+    (ArrayToSliceMut, Sig.array_to_slice_sig true, true, None);
+    (* Array Repeat *)
+    (ArrayRepeat, Sig.array_repeat_sig, false, None);
+    (* Indexing *)
+    ( Index { is_array = true; mutability = RShared; is_range = false },
       Sig.array_index_sig false,
       true,
-      "@ArrayIndexShared",
       None );
-    (ArrayIndexMut, Sig.array_index_sig true, true, "@ArrayIndexMut", None);
-    (* Array to slice*)
-    ( ArrayToSliceShared,
-      Sig.array_to_slice_sig false,
+    ( Index { is_array = true; mutability = RMut; is_range = false },
+      Sig.array_index_sig true,
       true,
-      "@ArrayToSliceShared",
       None );
-    ( ArrayToSliceMut,
-      Sig.array_to_slice_sig true,
+    ( Index { is_array = false; mutability = RShared; is_range = false },
+      Sig.slice_index_sig false,
       true,
-      "@ArrayToSliceMut",
       None );
-    (* Array Repeat *)
-    (ArrayRepeat, Sig.array_repeat_sig, false, "@ArrayRepeat", None);
-    (* Slice Index *)
-    ( SliceIndexShared,
-      Sig.slice_index_sig false,
+    ( Index { is_array = false; mutability = RMut; is_range = false },
+      Sig.slice_index_sig true,
       true,
-      "@SliceIndexShared",
       None );
-    (SliceIndexMut, Sig.slice_index_sig true, true, "@SliceIndexMut", None);
   ]
 
 let assumed_fun_infos : assumed_fun_info list =

compiler/Extract.ml

@@ -2774,6 +2774,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
      * Extract the items
      *)
     let trait_decl_id = impl.impl_trait.trait_decl_id in
+    let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.crate.trait_decls in
 
     (* The constants *)
     List.iter
@@ -2810,19 +2811,19 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
       impl.types;
 
     (* The parent clauses *)
-    TraitClauseId.iteri
-      (fun clause_id trait_ref ->
+    List.iter
+      (fun (clause, trait_ref) ->
         let item_name =
           ctx_get_trait_parent_clause impl.item_meta.span trait_decl_id
-            clause_id ctx
+            clause.T.clause_id ctx
         in
         let ty () =
           F.pp_print_space fmt ();
           extract_trait_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty
             false trait_ref
         in
         extract_trait_impl_item ctx fmt item_name ty)
-      impl.parent_trait_refs;
+      (List.combine trait_decl.parent_clauses impl.parent_trait_refs);
 
     (* The required methods *)
     List.iter