[Caml-list] More precise line number directives?

[Caml-list] More precise line number directives?

[Clément Pit-Claudel]

Hi all,

I came across the following section of the documentation a few days ago:

> Line number directives
>
> Preprocessors that generate OCaml source code can insert line number
> directives in their output so that error messages produced by the
> compiler contain line numbers and file names referring to the source
> file before preprocessing, instead of after preprocessing. A line
> number directive is composed of a # (sharp sign), followed by a
> positive integer (the source line number), optionally followed by a
> character string (the source file name). Line number directives are
> treated as blanks during lexical analysis.

Has there been efforts or proposals in the past to support more precise annotations?  Something like source maps, for example (https://github.com/ryanseddon/source-map/wiki/Source-maps:-languages,-tools-and-other-info; specs at https://docs.google.com/document/d/1U1RGAehQwRypUTovF1KRlpiOFze0b-_2gc6fAH0KY0k/).

Some background: multiple languages, including Coq and F*, use OCaml as an intermediate language.  Debugging extracted code (with ocamldebug or gdb) or looking at backtraces is unpleasant, because the generated OCaml code isn't always pretty.  It would be very nice to get backtraces pointing to the original code (and even nicer to be able to step through the original sources!).

Has a similar proposal been discussed before?  Would it be hard to implement?

Thanks!
Clément.