Setting `-D Elab.async=false` breaks `backward.privateInPublic`

[yhx-12243]

Prerequisites

(cf. #8746, but it is different and more fatal)

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

As title said: Elab.async and backward.privateInPublic are incompatible.

Steps to Reproduce

Code:

-- main.lean
module

set_option backward.privateInPublic true

public class U : Type where
  a : Nat
  h : a = a

private theorem A : 0 = 0 := rfl

public instance : U := ⟨0, A⟩

Compile it use lean main.lean -D Elab.async=false.

Expected behavior:

main.lean:12:27: warning: Private declaration `A` accessed publicly; this is allowed only because the `backward.privateInPublic` option is enabled.

Disable `backward.privateInPublic.warn` to silence this warning.

Actual behavior:

main.lean:12:27: error(lean.unknownIdentifier): Unknown identifier `A`

Note: A private declaration `A` (from the current module) exists but would need to be public to access here.

Versions

4.30.0-rc2, macOS (reproducible in live):

https://live.lean-lang.org/#codez=LYewJgrgNgpgUHAzjALgfRABxQSxAOwAIAjAQwGMBrAd1ICcwA6TOnAN1JRgEl8AFCMSg5yhFHQjxk6LLgKEAolFLFGpRAE98ogGakoyBJkHDR5ZYkSEAqoQBchACobMMQtQAWMOvEKFS9oQAcpxwfh6BAQC8%2FkasHFxiXiA%2BwIQAgoEADIQxOXYxdDpQRiYihDj4iCik2m4OtgWEgBfkWQA0GYCX5HBAA

Additional Information

Based on the description

lean4/src/Lean/CoreM.lean

Lines 35 to 46 in aa6fa1c

	register_builtin_option Elab.async : Bool := {
	defValue := false
	descr := "perform elaboration using multiple threads where possible\
	\n\
	\nThis option defaults to `false` but (when not explicitly set) is overridden to `true` in \
	the Lean language server and cmdline. \
	Metaprogramming users driving elaboration directly via e.g. \
	`Lean.Elab.Command.elabCommandTopLevel` can opt into asynchronous elaboration by setting \
	this option but then are responsible for processing messages and other data not only in the \
	resulting command state but also from async tasks in `Lean.Command.Context.snap?` and \
	`Lean.Command.State.snapshotTasks`."
	}

of this option, it shouldn't affect any correctness.