Skip to content

Clarify kontrol build behavior #42

@palinatolmach

Description

@palinatolmach

Identified during the Secureum workshop. We should clarify the following behavior of kontrol build in the documentation

  • if Solidity files changed, we detect it by comparing digests that we generate during each kompilation, and, if the digest changed, trigger rekompilation (so in that case kontrol build --rekompile and kontrol build are equivalent, and that is why you see a change in the verification result); that is done here: https://github.com/runtimeverification/kontrol/blob/7ee1b0473aa177f95440876c21154d2d944248e2/src/kontrol/kompile.py#L139
  • if Solidity files did not change, kompilation will be skipped
  • in this case, --rekompile is needed if you want to add something else to the kompilation, in particular, lemmas — in other words, if you want to retrigger kompilation even if there're no changes in the forge build output that would trigger rekompilation automatically.

Metadata

Metadata

Assignees

No one assigned

    Labels

    documentationImprovements or additions to documentation

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions