Doc 4 kontrol.toml #65
Conversation
Stevengre
commented
Nov 18, 2024
Stevengre
commented
- provide all options for kontrol.toml
palinatolmach
left a comment
palinatolmach
left a comment
There was a problem hiding this comment.
I left a few comments. Could you please also make sure that you can run kontrol commands in a project with this kontrol.toml file?
README.md
Outdated
| visible: true | ||
| --- | ||
|
|
||
| # Kontrol |
There was a problem hiding this comment.
I think it was removed in the previous PR:
| # Kontrol |
There was a problem hiding this comment.
And the next empty line too.
glossary/kontrol-toml.md
Outdated
| module-import = 'TestBase:KONTROL-LEMMAS' | ||
| auxiliary-lemmas = true | ||
|
|
||
| # ? definition_dir = None |
There was a problem hiding this comment.
What does this question mark indicate? I think it's ok to just leave these options commented, e.g.,
# definition_dir = None
or even
# definition_dir =
glossary/kontrol-toml.md
Outdated
| # ? spec_module = None | ||
|
|
||
| [build] | ||
| # Directories to lookup K definitions in. |
There was a problem hiding this comment.
I wouldn't put comments below or after the options. How about placing them next to the option instead? E.g.,
# include = [] # Directories to lookup K definitions in.
glossary/kontrol-toml.md
Outdated
| no-stack-checks = true | ||
|
|
||
| [prove] | ||
| -I INCLUDES Directories to lookup K definitions in. |
There was a problem hiding this comment.
Please update those values too.
Stevengre
force-pushed
the
jh/kontrol-toml
branch
from
6791f00 to
1697109
Compare
README.md
Outdated
| # Kontrol | ||
|
|
There was a problem hiding this comment.
| # Kontrol |
glossary/kontrol-toml.md
Outdated
| # spec_module = | ||
|
|
||
| [build] | ||
| backend = # K backend to target with compilation. |
There was a problem hiding this comment.
I don't think that's allowed in a non-comment line, please consider changing it (and other similar lines) to the following:
| backend = # K backend to target with compilation. | |
| # backend = # K backend to target with compilation. |
Please check if kontrol build, prove, etc. works with this kontrol.toml file.
There was a problem hiding this comment.
Sorry, I missed these options. I'll check it again.
Stevengre
left a comment
Stevengre
left a comment
There was a problem hiding this comment.
kontrol buildpassed.kontrol proveworked, butsetupfunction costs more time than expected and still not finished.kontrol showunchecked.
Running setup functions in parallel: test%CounterTest.setUp()
⠇ 0:04:23 test%CounterTest.setUp():0 Running proof PENDING: 35 nodes: 9 pending|5 passed|0 failing|0 vacuous|0 refuted|0 stuck
3 participants
