fix: new code generator must generate code for opaque declarations that are not `@[extern]`

src/Lean/Compiler/LCNF/Main.lean

diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index 5eef458..7b3e0b2 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -29,7 +29,7 @@
 def shouldGenerateCode (declName : Name) : CoreM Bool := do
   if (← isCompIrrelevant |>.run') then return false
   let some info ← getDeclInfo? declName | return false
-  unless info.hasValue do return false
+  unless info.hasValue (allowOpaque := true) do return false
   let env ← getEnv
   if isExtern env declName then return false
   if hasMacroInlineAttribute env declName then return false

src/Lean/Compiler/LCNF/ToDecl.lean

diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean
index df5fb21..7338dcc 100644
--- a/src/Lean/Compiler/LCNF/ToDecl.lean
+++ b/src/Lean/Compiler/LCNF/ToDecl.lean
@@ -96,7 +96,7 @@
 def toDecl (declName : Name) : CompilerM Decl := do
   let declName := if let some name := isUnsafeRecName? declName then name else declName
   let some info ← getDeclInfo? declName | throwError "declaration `{declName}` not found"
-  let some value := info.value? | throwError "declaration `{declName}` does not have a value"
+  let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
   let (type, value) ← Meta.MetaM.run' do
     let type  ← toLCNFType info.type
     let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body)
@@ -107,7 +107,7 @@
     /- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/
     let value ← macroInline value
     /-
-    Remark: we have disabled the following transformation, we will perform it at phase 2, after code specialization.
+    Remark: we have disabled the following transformatbion, we will perform it at phase 2, after code specialization.
     It prevents many optimizations (e.g., "cases-of-ctor").
     -/
     -- let value ← applyCasesOnImplementedBy value

src/Lean/Declaration.lean

diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 6c8833b..3ce068d 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -436,24 +436,30 @@
 def type (d : ConstantInfo) : Expr :=
   d.toConstantVal.type
 
-def value? : ConstantInfo → Option Expr
-  | .defnInfo {value := r, ..} => some r
-  | .thmInfo  {value := r, ..} => some r
-  | _                          => none
+def value? (info : ConstantInfo) (allowOpaque := false) : Option Expr :=
+  match info with
+  | .defnInfo {value, ..}   => some value
+  | .thmInfo  {value, ..}   => some value
+  | .opaqueInfo {value, ..} => if allowOpaque then some value else none
+  | _                       => none
 
-def hasValue : ConstantInfo → Bool
-  | .defnInfo _ => true
-  | .thmInfo  _ => true
-  | _           => false
+def hasValue (info : ConstantInfo) (allowOpaque := false) : Bool :=
+  match info with
+  | .defnInfo _   => true
+  | .thmInfo  _   => true
+  | .opaqueInfo _ => allowOpaque
+  | _             => false
 
-def value! : ConstantInfo → Expr
-  | .defnInfo {value := r, ..} => r
-  | .thmInfo  {value := r, ..} => r
-  | _                          => panic! "declaration with value expected"
+def value! (info : ConstantInfo) (allowOpaque := false) : Expr :=
+  match info with
+  | .defnInfo {value, ..}   => value
+  | .thmInfo  {value, ..}   => value
+  | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
+  | _                       => panic! "declaration with value expected"
 
 def hints : ConstantInfo → ReducibilityHints
-  | .defnInfo {hints := r, ..} => r
-  | _                          => ReducibilityHints.opaque
+  | .defnInfo {hints, ..} => hints
+  | _                     => .opaque
 
 def isCtor : ConstantInfo → Bool
   | .ctorInfo _ => true

tests/lean/run/opaqueNewCodeGen.lean

diff --git a/tests/lean/run/opaqueNewCodeGen.lean b/tests/lean/run/opaqueNewCodeGen.lean
new file mode 100644
index 0000000..85afa94
--- /dev/null
+++ b/tests/lean/run/opaqueNewCodeGen.lean
@@ -0,0 +1,20 @@
+import Lean
+
+set_option compiler.enableNew true
+
+/--
+info: [Compiler.result] size: 1
+    def f x : Nat :=
+      let _x.1 := Nat.add x x;
+      return _x.1
+-/
+#guard_msgs in
+set_option trace.Compiler.result true in
+opaque f : Nat → Nat :=
+  fun x => Nat.add x x
+
+/-- -/
+#guard_msgs in
+set_option trace.Compiler.result true in
+@[extern "lean_nat_gcd"]
+opaque g : Nat → Nat → Nat