Preserve comments

Open jespercockx opened this issue 3 years ago • 4 comments

As in the title, requested by @gallais

Oct 06 '22 14:10 jespercockx

Note that we can currently "fake" documentation in the generated output by including comments within a {-# FOREIGN #-} block.

Oct 06 '22 14:10 omelkonian

Linking agda/agda#5541, because if there is support for it upstream any backend would be able to preserve comments attached to definitions.

Feb 28 '23 09:02 flupe

This doesn't seem feasible with the current state of Agda and there is a reasonable workaround, so I'm closing this.

Oct 23 '23 11:10 jespercockx

After some discussion with @HeinrichApfelmus about the importance of being able to generate comments, I'm re-opening this.

In particular, the existence of this tool shows that there is a real need: https://github.com/cardano-foundation/cardano-wallet-agda/tree/main/lib/agda2hs-fixer If necessary, we could consider re-parsing the actual Agda source in agda2hs just so we can properly extract the comments.

Nov 15 '24 13:11 jespercockx