Open
Description
I propose a default setting enhancement for lemma files and module imports for the kontrol build
command.
Current Requirement:
If a user wants to include project-specific lemmas, he must explicitly specify the lemmas file and module import on each build, like so:
kontrol build --require lemmas.k --module-import CronTwoTest:CRON-TWO-LEMMAS
Proposed Default Behavior:
The new behavior turns this configuration into a convention:
- We let
--require
default toproject-lemmas.k
. - We let
--module-import
default toPROJECT-LEMMAS
. - We auto-create
project-lemmas.k
with an emptyPROJECT-LEMMAS
module if not present. (Maybe we could even add a simple lemma here, so users have a template to start from). - We emit a warning/error if
PROJECT-LEMMAS
module is missing (e.g. because a user deleted it).
This simplifies the process, benefiting users by reducing repetitive command-line specifications.