runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 19 forks source link

Allow `kore-proof-trace` to display `label` and `location` info for improve debugging if a kore definition file is given #1098

Open Robertorosmaninho opened 6 days ago

Robertorosmaninho commented 6 days ago

Fix: https://github.com/Pi-Squared-Inc/pi2/issues/1562

The Math Proof Team from Pi2 required that rule hints contain more high-level information, such as the label attribute, if present, and the k file location of a rule, instead of only printing the ordinal and arity, to help them debug their code.

With that in mind, we propose that kore-proof-trace could take an extra/optional argument of a kore definition file. When this file is passed in the CLI, the tool will parse and preprocess it so we can extract these high-level info from the definition and print it in the hints human-readable output! If the definition isn't passed to the tool, it keeps this old behavior.

The new output looks like this: