Most of the changes are centered around exporting more information in the form of CodeWithInfos
so I can linkify it in doc-gen + hiding that this is the fact in the ToJson instnsances.
Additional Notes
There is one change that I did specific to doc-gen. The one in LeanInk/Analysis/Analysis.lean which does not initialize the search path anymore since doc-gen already does this for LeanInk.
Now as far as I can tell this only breaks non Lake projects because the search path initialization for Lake projects does actually happen in a different part of LeanInk. So maybe we can just keep it this way? Otherwise we might have to add something like a flag in the Analysis monad that indicates this.
Description
Finally merging the doc-gen LeanInk fork upstream
Notable Changes
Most of the changes are centered around exporting more information in the form of CodeWithInfos so I can linkify it in doc-gen + hiding that this is the fact in the
ToJsoninstnsances.Additional Notes
There is one change that I did specific to doc-gen. The one in LeanInk/Analysis/Analysis.lean which does not initialize the search path anymore since doc-gen already does this for LeanInk. Now as far as I can tell this only breaks non Lake projects because the search path initialization for Lake projects does actually happen in a different part of LeanInk. So maybe we can just keep it this way? Otherwise we might have to add something like a flag in the Analysis monad that indicates this.