kframework/kweb

path to K definition set incorrectly

Opened this issue · 1 comments

If I click on a language definition under the examples folder, kompile it, and then try to run a program under the tutorial folder, then the path to the K definition is not set in the kompile button. This problem appeared in yesterday's K meeting, where Andrei tried to run some imp programs using his new java rewrite engine, which requires a slightly modified definition of imp, found under the exmaples folder.

Unfortunately this bug is due to a fundamental design restriction in kweb. Currently, the tool is not aware of the full path of each file client-side, and is only aware of the relative path from the collection. Because tutorial and samples are two different collections, selecting across them doesn't work. This is by design, because the samples and tutorials collection may not be stored in the same location. For example, if a user modifies the tutorials collection but not the sample collection, the tutorials collection will be in their workspace and therefore owned by them while the samples collection will remain as a reference to a folder in default's workspace. This is to save disk space and allow for logged in users to receive updates to collections they have not modified automatically.

If this is a must-have feature, we can put both samples and examples in a separate top-level collection, perhaps called default or k_default. Then you will be able to use command-line relative paths across them as they will share a top level directory.

I'm going to leave this bug open but put a wontfix on it for now, feel free to comment on any other way of handling this issue.