`kontrol simplify-node --lemmas` broken

[juliankuners]

kontrol simplify-node simplifies a given node in a proof and returns the output. It also has a flag --lemmas <lemmas.k file>:<MODULE_NAME> with which a lemmas file can be passed that is kompiled and used as well.

However, according to my observation this --lemmas flag is currently broken. It seems to me that the lemmas file is kompiled and sent to the haskell-backend, but not referenced in simplification requests and therefore unused. As a consequence, this feature cannot be used to test simplification lemmas.

Additionally, kontrol simplify-node --lemmas <lemmas.k file>:<MODULE_NAME> crashes when a simplification rule uses preserves-definedness.

This can be reproduced with this kontrol repository: https://github.com/juliankuners/test-simplify-node

[ehildenb]

I think the format is --lemmas lemmas.k:MODULE_NAME, does it work if you do that?

[juliankuners]

@ehildenb thanks for the note! I did try this with --lemmas lemmas.k:MODULE_NAME and it does not work unfortunately. I updated the issue text respectively.

[ehildenb]

Can you post more information about how you see that the lemmas file is not being considered? There are some tests that exercise this, so I'd be a bit surprised (but not too surprised). Could it be that your lemma actually just doesn't apply when you think it does?

[juliankuners]

Can you post more information about how you see that the lemmas file is not being considered? There are some tests that exercise this, so I'd be a bit surprised (but not too surprised). Could it be that your lemma actually just doesn't apply when you think it does?

I double checked and changed the lemma in https://github.com/juliankuners/test-simplify-node slightly to more easily see whether it fired or not. It does fire when included from the start when running kontrol build and kontrol prove. However, it does not apply if it's not part of the kontrol build lemmas.k and instead is supplied to kontrol simplify-node.