-
Notifications
You must be signed in to change notification settings - Fork 232
Error locations in generated OCaml code
Jonathan Protzenko edited this page Mar 25, 2016
·
2 revisions
The OCaml extraction backend of F★ generates so-called "location directives", so that backtraces and error messages locate errors in the original F★ files, rather than in the extracted OCaml files. Essentially, F★ generates once in a while a line of the form # X F
where X
is the original line number and F
is the original file name. This modifies the OCaml parser's internal state.
Currently (02/11/2016), these lines are generated before every top-level binding and every let-binding. This means that some locations may be off by a few lines.
Use --no_location_info
to disable this behavior (because, say, you're debugging F* itself).