Unable to run claims with kevm prove

[lucasmt]

I have a lemmas.k file with a LEMMAS module and a LEMMAS-SPEC module with a claim claim-1. I'm trying to run this claim with the commands

kevm kompile-spec lemmas.k --target haskell --main-module LEMMAS --syntax-module LEMMAS -o kompiled
kevm prove lemmas.k --claim LEMMAS-SPEC.claim-1 --definition kompiled

but I get the error ValueError: Claim labels not found: ['LEMMAS.LEMMAS-SPEC.claim-1']. In other words, it automatically prefixes the claim label with the main module LEMMAS, which is incorrect because the claim is in the LEMMAS-SPEC module. It's not even possible for the claim to be in the main module because in this case kevm kompile-spec fails with the error message Claims are not allowed in the definition.

kevm prove used to have a --spec-module option, but it no longer seems to accept it, so I don't know how else to specify the spec module.

[PetarMax]

I would classify this as high priority, since we do need it for ongiong engagements and standard testing.

[PetarMax]

In pyk version 0.1.696 we have an update_args static method for KDefinitionOptions here, which has --spec-module. We also have update_args for all subclasses of Options.

In pyk version 0.1.697, KDefinitionOptions disappears entirely.

In pyk version 0.1.712, KDefinitionOptions makes a comeback, but without the update_args static method (here). No subclass of Options has update_args anymore.