Pickling-unpickling an environment makes definitions noncomputable?

Hello!

I was playing with the pickling / unpickling feature of the REPL and I got the following result:
If I run def x := 1 then def y := x + 1, I get the following output:

{"cmd": "def x := 1"}

{"env": 0}

{"cmd": "def y := x + 1", "env": 0}

{"env": 1}

However, if I instead pickle and unpickle env 0, I get this:

{"cmd": "def x := 1"}

{"env": 0}

{"pickleTo": "def_test.olean", "env": 0}

{"env": 0}

{"unpickleEnvFrom": "def_test.olean"}

{"env": 1}

{"cmd": "def y := x + 1", "env": 1}

{"messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 4},
   "endPos": {"line": 1, "column": 5},
   "data":
   "failed to compile definition, consider marking it as 'noncomputable' because it depends on 'x', and it does not have executable code"}],
 "env": 2}

Which seems to indicate that x is now noncomputable. We can define y as noncomputable as well to make the command valid:

{"cmd": "noncomputable def y := x + 1", "env": 1}

{"env": 3}

I tested on the revisions v4.14.0 and v4.7.0.
Based on my understanding of Lean, this behavior seems unexpected. However, if I'm overlooking something, please let me know ^^

Thanks!

No source file or test is named. Reproduce the reported sequence in the REPL: define x, pickle env 0, unpickle it, then define y using x; compare it with the unpickled environment's behavior. Trace the pickling and environment-restoration entry points, and consider the issue done when the restored definition remains computable or the behavior is documented as intended.