Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clarify kontrol build behavior #42

Closed
palinatolmach opened this issue Apr 5, 2024 · 1 comment
Closed

Clarify kontrol build behavior #42

palinatolmach opened this issue Apr 5, 2024 · 1 comment
Labels
documentation Improvements or additions to documentation

Comments

@palinatolmach
Copy link
Contributor

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.
@yale-vinson yale-vinson added the documentation Improvements or additions to documentation label Apr 18, 2024
@palinatolmach
Copy link
Contributor Author

Closed in favor of #54.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation
Projects
None yet
Development

No branches or pull requests

2 participants