search

dapphub / klab

K framework proof explorer & smart contract specification format
GNU Affero General Public License v3.0
123 stars 36 forks source link

klab debug's rule view uses hardcoded paths #404

Open livnev opened 4 years ago

livnev commented 4 years ago

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 commented 4 years ago

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

livnev commented 4 years ago

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

mhhf commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

I like the issue number on this issue