Description
In ProbeLean/Types.lean:
Atom.ToJson intentionally omits the name field (it becomes the key in the AtomsOutput dict)Atom.FromJson requires a name field from the JSON value
This means individual Atom instances cannot round-trip through their own FromJson/ToJson. Only AtomsOutput can round-trip (it has its own manual parsing that extracts name from the dict key).
Impact
Confusing API: Atom.FromJson will fail when applied to JSON produced by Atom.ToJson. The two parallel parsing implementations (Atom.FromJson vs AtomsOutput.FromJson) must be kept in sync manually, which has already led to bugs (e.g., rustSource being dropped in AtomsOutput.FromJson).
Suggested Fix
Either:
- Remove
Atom.FromJson (since it's never used directly)
- Or refactor
AtomsOutput.FromJson to set name on the JSON value and delegate to Atom.FromJson
Description
In
ProbeLean/Types.lean:Atom.ToJsonintentionally omits thenamefield (it becomes the key in theAtomsOutputdict)Atom.FromJsonrequires anamefield from the JSON valueThis means individual
Atominstances cannot round-trip through their ownFromJson/ToJson. OnlyAtomsOutputcan round-trip (it has its own manual parsing that extractsnamefrom the dict key).Impact
Confusing API:
Atom.FromJsonwill fail when applied to JSON produced byAtom.ToJson. The two parallel parsing implementations (Atom.FromJsonvsAtomsOutput.FromJson) must be kept in sync manually, which has already led to bugs (e.g.,rustSourcebeing dropped inAtomsOutput.FromJson).Suggested Fix
Either:
Atom.FromJson(since it's never used directly)AtomsOutput.FromJsonto setnameon the JSON value and delegate toAtom.FromJson