Add the option --features
#1648
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
konnov
requested review from
shonfeder,
thpani,
bugarela,
Kukovec and
rodrigo7491
and removed request for
shonfeder
thpani
reviewed
Apr 20, 2022
UNRELEASED.md
Outdated
Comment on lines
19
to
23
| * Fix references to `--tune-here` (actually `--tuning-options`), see #1579 | ||
| * Fix references to `--tune-here` (actually `--tuning-options`), see #1579 |
There was a problem hiding this comment.
We should either not commit these, or have a convention on file ending newlines.
mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/General.scala
Outdated
Show resolved
Hide resolved
Comment on lines
39
to
40
| | - rows: enable row typing as explained in ADR-014 | ||
| |""".stripMargin) |
There was a problem hiding this comment.
Won't this print an extra newline?
Suggested change
| | - rows: enable row typing as explained in ADR-014 | |
| |""".stripMargin) | |
| | - rows: enable row typing as explained in ADR-014""".stripMargin) |
Codecov Report
@@ Coverage Diff @@
## unstable #1648 +/- ##
============================================
- Coverage 75.00% 74.90% -0.10%
============================================
Files 356 357 +1
Lines 11597 11611 +14
Branches 552 553 +1
============================================
- Hits 8698 8697 -1
- Misses 2899 2914 +15
Continue to review full report at Codecov.
|
thpani
approved these changes
Apr 21, 2022
I'm not sure why the mdx wildcard matching wasn't working as expected, but I think this test is as clear. The `ERROR` output was actually spurious, afaict, because CLI parsing errors are handled before we ever get to Apalache's internal tool executable error handling.
Moving the name and description into the `Feature` trait lets us ensure the inline documentation is up to date. Moving the conversion into the case class lets us reuse this logic in the configuration manager.
There's no need to call `ConfigManager` outside of `outputAndLogConfig` since its result is only used in the body of the latter.
Under the assumption that: - We shouldn't start measuring model checking time while setting up the output and processing configs. - We want to be able to reflect configuration failures in the exit code. - We don't need comments that repeat the name of functions.
Prior to this change errors resulting from invalid Apalache configuration files were resulting in uncaught exceptions. Now we return an `Either` from the configuration loading, and use that to determine whether we should continue running the command or report a configuration error.
The full error looks something like ``` 22:00:34.534 [main] ERROR at.forsyte.apalache.tla.Tool$ - Configuration error: at 'features.0': - (/home/sf/Sync/informal-systems/apalache/apalache-core/test/tla/./.apalache.cfg: 1) Cannot convert 'invalid-feature' to at.forsyte.apalache.tla.lir.Feature: . EXITCODE: ERROR (255) ``` We truncate it in the integration test to avoid platform-specific information breaking the integration tests.
Hopefully will account for stderr output from docker container
…neral.scala Co-authored-by: Thomas Pani <thomas@informal.systems>
@shonfeder quick workflow question: I think we don't necessarily need to block on this? |
added 2 commits
April 26, 2022 08:56
…stions Integrate features flag into ConfigManager
shonfeder
approved these changes
Apr 26, 2022
18 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Closes #1647. As discussed in #401, this PR introduces the option
--featuresthat lets us pass experimental features to the tool. The only supported feature inrows, which is parsed asRowsFeature. When we want to add new features, we have to extend the traitFeaturewith a case class and update the parser inGeneral.For the moment, I am not adding any documentation to the user manual. I will extend the manual section on types, when we start the transition period to Type System 1.2.
make fmt-fix(or had formatting run automatically on all files edited)