Do we still want this feature? It creates an extra level of complexity in the kompile data structures. If this is not needed, or could be replaced with something more general, we should consider deprecating it.
Dwight: imports syntax directive, was created because there was a situation where you wanted to be able to import another configuration fragment for configuration composition, but not import the initializers for those cells. I'm not sure it's really used in any of our semantics currently, so I'm not hugely opposed to deprecating it somehow.
This is currently being used in lambda++:
https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/lambda.k#L38
https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_5/lambda.k#L14
and domains.md, DEFAULT-STRATEGY:
https://github.com/kframework/k/blob/master/k-distribution/include/kframework/builtin/domains.md
I also searched evm-semantics, c-semantics, k-exercises, wasm-semantics, firefly,
michelson-semantics, elrond-semantics, iele-semantics and pending-documentation and couldn't find any reference for this feature.
Do we still want this feature? It creates an extra level of complexity in the kompile data structures. If this is not needed, or could be replaced with something more general, we should consider deprecating it.
Dwight:
imports syntaxdirective, was created because there was a situation where you wanted to be able to import another configuration fragment for configuration composition, but not import the initializers for those cells. I'm not sure it's really used in any of our semantics currently, so I'm not hugely opposed to deprecating it somehow.This is currently being used in
lambda++:https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/lambda.k#L38
https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_5/lambda.k#L14
and domains.md, DEFAULT-STRATEGY:
https://github.com/kframework/k/blob/master/k-distribution/include/kframework/builtin/domains.md
I also searched evm-semantics, c-semantics, k-exercises, wasm-semantics, firefly,
michelson-semantics, elrond-semantics, iele-semantics and pending-documentation and couldn't find any reference for this feature.