search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
359 stars 53 forks source link

Positions count 1 tab as 8 spaces #984

Open jad-hamza opened 3 years ago

jad-hamza commented 3 years ago

cc: @deiruch

This makes IDEs who count 1 tab = 1 column misreport positions of warnings and errors.

We could adjust positions down by fetching the source code line and counting tabs during code extraction when converting Scala positions to Inox positions. The feature could be put under an option (enabled by default or not), because not all IDEs count 1 tab = 1 column.

Edit: If positions are scaled down to count 1 tab = 1 column, we should replace 1 tab with 1 space when reporting lines and error positions in the console output: https://github.com/epfl-lara/inox/blob/1b17cb4d38dfddf16286e3346929b7a05267c380/src/main/scala/inox/Reporter.scala#L207

sfiruch commented 3 years ago

Out of curiosity: Which IDEs expect 1 tab = 8 spaces? With a cursory review, I found that my tested editors all expect 1 tab = 1 column (EditPlus, Visual Studio, IntelliJ)

jad-hamza commented 3 years ago

I tried in VSCode and emacs to enter a tab (of length 8), and the column numbers in the bottom of the screen are shown as 9 (VSCode) and 8 (emacs)

sfiruch commented 3 years ago

Yes, that happens in VS (non-code) as well. However, the IDEs I tested use characters, not columns, when interpreting the error message. I.e., when I click on the error "file.scala:10:10", the cursor might end up at character 10, column 18 (which is shown in the status bar).