diff --git a/src/Init/Dynamic.lean b/src/Init/Dynamic.lean index 0d4b2d0007..a414d6ffb4 100644 --- a/src/Init/Dynamic.lean +++ b/src/Init/Dynamic.lean @@ -14,7 +14,8 @@ public section open Lean -- Implementation detail of TypeName, since classes cannot be opaque -private opaque TypeNameData (α : Type u) : NonemptyType.{0} := +-- TODO: should be private; #10098 +opaque TypeNameData (α : Type u) : NonemptyType.{0} := ⟨Name, inferInstance⟩ /-- diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index a4029c7360..f36e65ea1d 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -94,6 +94,10 @@ def addDecl (decl : Declaration) : CoreM Unit := do if (← getEnv).header.isModule && !(← getEnv).isExporting then exportedInfo? := some <| .axiomInfo { defn with isUnsafe := defn.safety == .unsafe } pure (defn.name, .defnInfo defn, .defn) + | .opaqueDecl op => + if (← getEnv).header.isModule && !(← getEnv).isExporting then + exportedInfo? := some <| .axiomInfo { op with } + pure (op.name, .opaqueInfo op, .opaque) | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom) | _ => return (← doAdd) diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index ead4715b6a..b149b37362 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -102,9 +102,7 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U let env ← getEnv if ps.isEmpty then if isExternal then emit "extern " - -- The first half is a pre-module system approximation, we keep it around for the benefit of - -- unported code. - else if isClosedTermName env decl.name || !Compiler.LCNF.isDeclPublic env decl.name then emit "static " + else if isClosedTermName env decl.name then emit "static " else emit "LEAN_EXPORT " else if !isExternal then emit "LEAN_EXPORT " diff --git a/tests/bench/identifier_completion.lean b/tests/bench/identifier_completion.lean index 5d69132168..722a2087ff 100644 --- a/tests/bench/identifier_completion.lean +++ b/tests/bench/identifier_completion.lean @@ -3,12 +3,10 @@ import Lean.AddDecl open Lean -set_option debug.skipKernelTC true - def buildSyntheticEnv : Lean.CoreM Unit := do for i in [0:100000] do let name := s!"Long.And.Hopefully.Unique.Name.foo{i}".toName - addDecl <| Declaration.opaqueDecl { + let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 <| .opaqueDecl { name := name levelParams := [] type := .const `Nat [] @@ -16,6 +14,7 @@ def buildSyntheticEnv : Lean.CoreM Unit := do isUnsafe := false all := [name] } + setEnv env' addDocStringCore name "A synthetic doc-string" #eval buildSyntheticEnv diff --git a/tests/bench/identifier_completion_didOpen.log b/tests/bench/identifier_completion_didOpen.log index eeab03db74..d10da13660 100644 --- a/tests/bench/identifier_completion_didOpen.log +++ b/tests/bench/identifier_completion_didOpen.log @@ -1,3 +1,3 @@ -Content-Length: 996 +Content-Length: 1041 -{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/mhuisi/Lean/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":952,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\nset_option debug.skipKernelTC true\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n for i in [0:100000] do\n let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n addDecl <| Declaration.opaqueDecl {\n name := name\n levelParams := []\n type := .const `Nat []\n value := .const `Nat.zero []\n isUnsafe := false\n all := [name]\n }\n addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}} \ No newline at end of file +{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":129,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n for i in [0:100000] do\n let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 <| .opaqueDecl {\n name := name\n levelParams := []\n type := .const `Nat []\n value := .const `Nat.zero []\n isUnsafe := false\n all := [name]\n }\n setEnv env'\n addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}} \ No newline at end of file diff --git a/tests/bench/identifier_completion_runner.lean b/tests/bench/identifier_completion_runner.lean index 14ce1aed37..0d3f9d647b 100644 --- a/tests/bench/identifier_completion_runner.lean +++ b/tests/bench/identifier_completion_runner.lean @@ -2,7 +2,7 @@ import Lean.Data.Lsp open IO Lean Lsp def mkCompletionRequest (id : Nat) : JsonRpc.Request Json := - let param := Json.parse r#"{"textDocument":{"uri":"file:///home/mhuisi/Lean/lean4/tests/bench/identifier_completion.lean"},"position":{"line":25,"character":40},"context":{"triggerKind":1}}"# + let param := Json.parse r#"{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean"},"position":{"line":24,"character":40},"context":{"triggerKind":1}}"# let param := param.toOption.get! { id, method := "textDocument/completion", param } diff --git a/tests/lean/run/printStructure.lean b/tests/lean/run/printStructure.lean index 325bbe2d40..352f35df81 100644 --- a/tests/lean/run/printStructure.lean +++ b/tests/lean/run/printStructure.lean @@ -59,9 +59,9 @@ constructor: info: class TypeName.{u} (α : Type u) : Type number of parameters: 1 fields: - private TypeName.data✝ : (TypeNameData✝ α).type + private TypeName.data✝ : (TypeNameData α).type constructor: - private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData✝ α).type) : TypeName α + private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData α).type) : TypeName α -/ #guard_msgs in #print TypeName