klab debug's rule view uses hardcoded paths

[livnev]

For example, if you investigate a proof trace with klab fetch and klab debug, the rule view will fail because it uses paths hardcoded on a different machine:

rule                                                                                                                                                                                                                                                                                         
/home/someuser/code/uniswap/k-uniswap-v2/burn/deps/klab/evm-semantics/.build/defn/java/evm.k 2038-2038                                                                                                                                                                                             
  | rule (/home/someuser/code/uniswap/k-uniswap-v2/burn/deps/klab/evm-semantics/.build/defn/java/evm.k:2038-2038) not found 

[mhhf]

the path is written hardcoded by k, klab only reads the path

[livnev]

Would it work to patch the paths by checking KLAB_EVMS_PATH? This would make the rule view useable in klab fetch workflows.

[mhhf]

yeah, it could work. but its a bit non trivial: we need to export KLAB_EVMS_PATH somehow to save it along with the proof's metadata in the zip file and then substitute it in the rule file. maybe 1-2h of work. how badly do you need this? is it blocking a proof for you or just nice to have?

[livnev]

yeah, it could work. but its a bit non trivial: we need to export KLAB_EVMS_PATH somehow to save it along with the proof's metadata in the zip file and then substitute it in the rule file. maybe 1-2h of work. how badly do you need this? is it blocking a proof for you or just nice to have?

Actually I was thinking maybe we don't need to save the original path, since it's probably possible to guess what the initial path looks like because it always has */evm-semantics/.build/defn etc. So we only need the KLAB_EVMS_PATH when klab debug is run.

This is not crucial for me at all, I only made the issue to make a note/suggest the idea. So I wouldn't worry about it for now.

[asymmetric]

I like the issue number on this issue