Add ConfigManager #1160

shonfeder · 2021-12-08T00:10:26Z

This adds the configuration management component, based around PureConfig,
decided for in #1156:

Changes:

Add dependency on PureConfig
Specify ApalacheConfigs trait (extending OutputManagerConfig) to serve
as the collection of loadable application configurations.
Add new ConfigManager(cli: CliArgs) class as a sibling of OutputManager
Look for a local config file .apalache.cfg, starting from the cwd, and climbing up through parent dirs.
Factor out all configuration from OutputManager, removing the
syncFromCli method.

Routine:

Tests added for any new code
Ran make fmt-fix (or had formatting run automatically on all files edited)
Documentation added for any new functionality
Entry added to UNRELEASED.md for any new functionality

To the point where current integration tests are passing.

We just check overrides for one config value, since we aren't checking that the PureConfig library can load configs, only that our desired precedence levels and overrides work as expected via the PureConfig library. I've tested the default global config locally, as I'm not sure of a good way to put that in the integration tests.

- To use the authorship schema proposed in the new ADR template. - To reflect introduction of the ConfigManager

konnov

Looks great! See several comments.

konnov · 2021-12-15T09:00:25Z

docs/src/adr/009adr-outputs.md

+Apalache should also look for a local configuration file `.apalache.cfg`, within
+current working directory or its parents. If it finds such file, any configured
+parameters therein will override the parameters from the global config file.


I wonder, whether we want to merge the TLC config in our configuration settings too. Certainly, we have way more options than the TLC config.

I'd not be opposed, but I'm also not very clear on the use or nature of TLC configuration. Could you maybe elaborate on #1177 or a new issue?

In either case, I think that'd be work for a followup.

konnov · 2021-12-15T09:02:54Z

docs/src/apalache/config.md

+Local configuration files support JSON and the JSON superset
+[HOCON](/~https://github.com/lightbend/config/blob/master/HOCON.md).


JSON has a weird limit on the length of integer literals. Does it apply to HOCON too?

I don't see a limit on integer sizes in the JSON spec: https://www.json.org/json-en.html

Is this an implementation detail of certain deserialization libs, or is there a different spec where you've seen this?

I'm not sure whether the implementation of HOCON has such a limit. The docs seem to indicate a limit of 64 bit integers: /~https://github.com/lightbend/config/blob/main/HOCON.md

I don't see how this could be a problem for any of the current configurations we support tho.

konnov · 2021-12-15T09:03:50Z

docs/src/apalache/config.md

+```yaml
+# Directory in which to write all log files and records of each run
+out-dir: "${PWD}/_apalache-out"
+
+# Whether or not to write additional files, that report on intermediate
+# processing steps
+write-intermediate: false


This example looks like yaml, not json, which contradicts the preceding sentence.

Which sentence does it contradict? This is valid HOCON.

docs/src/apalache/running.md

docs/src/adr/009adr-outputs.md

docs/src/apalache/running.md

Kukovec

LGTM. I'm just happy General finally defines a file field.

Kukovec · 2021-12-15T09:36:58Z

docs/src/adr/009adr-outputs.md

@@ -67,9 +68,18 @@ following:

 ## 4. Global Configuration File

-Apalache should define a global configuration file `apalache-global-config`, e.g. in the `<HOME>/.tlaplus` directory, in which users can define the default values of all parameters, including all flags listed in section 1, as well as `out-dir`. The format of the configuration file is an implementation detail and will not be specified here.
+Apalache should define a global configuration file `apalache.cfg`, e.g. in the `<HOME>/.tlaplus` directory, in which users can define the default values of all parameters, including all flags listed in section 1, as well as `out-dir`. The format of the configuration file is an implementation detail and will not be specified here.


I recall Igor complaining about the name apalache.cfg last time I suggested it
#1025 (comment)

That link doesn't actually take me to a particular comment (I think just because of how github hides resolved comments). @konnov are you still opposed to this config file name? It seems in keeping with the conventions I'm familiar with from other tools and the patterns suggested by the PureConfig docs.

docs/src/adr/009adr-outputs.md

docs/src/apalache/config.md

docs/src/apalache/running.md

Kukovec · 2021-12-15T09:51:52Z

tla-io/src/main/scala/at/forsyte/apalache/io/ConfigManager.scala

+  val TLA_PLUS_DIR = ".tlaplus"
+  val APALACHE_CFG = "apalache.cfg"
+  val DOT_APALACHE_CFG = "." + APALACHE_CFG


Wouldn't these be better suited for a companion object?

I don't know :)

What's the advantage of putting it it in the companion object?

I do think these should private tho. I'll at least change that.

I can't find anything in the Scala style guide that says where fields like this should be declared. Could you point me towards something that explains why putting such things in companion object might be preferable?

My own feeling is that -- in this case -- moving these into the companion object it would negatively impact readability: these values are only accessed in the class methods, and don't show up anywhere in the one method in the companion object. Moving them would then require readers to jump back and forth between the class and the companion object to see what means what.

I think we generally have the convention across the codebase that any public static X-type value goes in a companion object, so it can be accessed without creating a fresh instance.
This page quotes the "Scala Cookbook": https://alvinalexander.com/scala/how-to-static-members-in-scala-companion-objects-fields-methods/

It's not gospel, but it is convention elsewhere in the project.

Does the fact that these are (now) private and not meant to be accessed outside of the class at all impact your feelings on this? (I.e., they are never supposed to be accessed at all, whether by creating instance or not).

I still don't see there anything that explains a benefit in this case, and the downside on readability (and abstraction) seem pretty evident to me. I don't want to buck our conventions, but I'd rather there be a good reason if I'm going to negatively impact readability.

A bit more concretely, that recipe is for the case where

You want to create a Scala class that has both instance methods and static methods, but unlike Java, Scala does not have a static keyword.

afaict, that's not what we're actually after here.

docs/src/adr/009adr-outputs.md

docs/src/apalache/running.md

docs/src/adr/009adr-outputs.md

shonfeder · 2021-12-15T15:02:01Z

docs/src/apalache/config.md

+Local configuration files support JSON and the JSON superset
+[HOCON](/~https://github.com/lightbend/config/blob/master/HOCON.md).


I don't see a limit on integer sizes in the JSON spec: https://www.json.org/json-en.html

Is this an implementation detail of certain deserialization libs, or is there a different spec where you've seen this?

I'm not sure whether the implementation of HOCON has such a limit. The docs seem to indicate a limit of 64 bit integers: /~https://github.com/lightbend/config/blob/main/HOCON.md

I don't see how this could be a problem for any of the current configurations we support tho.

shonfeder · 2021-12-15T15:02:23Z

docs/src/apalache/config.md

+```yaml
+# Directory in which to write all log files and records of each run
+out-dir: "${PWD}/_apalache-out"
+
+# Whether or not to write additional files, that report on intermediate
+# processing steps
+write-intermediate: false


Which sentence does it contradict? This is valid HOCON.

docs/src/apalache/config.md

docs/src/apalache/running.md

shonfeder · 2021-12-15T15:15:51Z

tla-io/src/main/scala/at/forsyte/apalache/io/ConfigManager.scala

+  val TLA_PLUS_DIR = ".tlaplus"
+  val APALACHE_CFG = "apalache.cfg"
+  val DOT_APALACHE_CFG = "." + APALACHE_CFG


I don't know :)

What's the advantage of putting it it in the companion object?

I do think these should private tho. I'll at least change that.

I can't find anything in the Scala style guide that says where fields like this should be declared. Could you point me towards something that explains why putting such things in companion object might be preferable?

My own feeling is that -- in this case -- moving these into the companion object it would negatively impact readability: these values are only accessed in the class methods, and don't show up anywhere in the one method in the companion object. Moving them would then require readers to jump back and forth between the class and the companion object to see what means what.

tla-io/src/main/scala/at/forsyte/apalache/io/ConfigManager.scala

Co-authored-by: Kukovec <jure.kukovec@gmail.com> Co-authored-by: Igor Konnov <igor@informal.systems>

shonfeder marked this pull request as draft December 8, 2021 00:11

shonfeder mentioned this pull request Dec 14, 2021

Replace untyped option maps with statically typed configuration objects #1174

Closed

5 tasks

Shon Feder added 10 commits December 14, 2021 20:57

Add dependency on PureConfig

ccebaca

Add new ConfigManager class

7776d85

Wire application configuration through ConfgManager

a430b98

To the point where current integration tests are passing.

Fix formatting

2796376

Use default ApalacheConfig for unconfigured state

71f4ebd

Fix spelling of local config file name

19023ac

Remove outdated todo

e3fb447

Update output ADR

d910bc0

- To use the authorship schema proposed in the new ADR template. - To reflect introduction of the ConfigManager

Update documentation

3cf3d30

shonfeder force-pushed the shon/1069/add-config-mgr branch from 470e217 to 3cf3d30 Compare December 15, 2021 01:57

Update release notes

6d680db

shonfeder requested review from Kukovec and konnov December 15, 2021 02:05

shonfeder marked this pull request as ready for review December 15, 2021 02:06

shonfeder changed the title ~~WIP: Add ConfigManager~~ Add ConfigManager Dec 15, 2021

Remove unrelated change

e3298c6

konnov approved these changes Dec 15, 2021

View reviewed changes

Kukovec approved these changes Dec 15, 2021

View reviewed changes

shonfeder mentioned this pull request Dec 15, 2021

Integrate all CLI options into the configuration management system #1177

Closed

shonfeder commented Dec 15, 2021

View reviewed changes

tla-io/src/main/scala/at/forsyte/apalache/io/ConfigManager.scala Outdated Show resolved Hide resolved

Apply suggestions from code review

9702562

Co-authored-by: Kukovec <jure.kukovec@gmail.com> Co-authored-by: Igor Konnov <igor@informal.systems>

shonfeder requested a review from Kukovec December 15, 2021 15:23

Merge branch 'unstable' into shon/1069/add-config-mgr

0f3f771

shonfeder enabled auto-merge December 15, 2021 18:28

shonfeder merged commit 49138e1 into unstable Dec 15, 2021

apalache-bot mentioned this pull request Dec 20, 2021

[release] 0.18.2 #1185

Closed

apalache-bot mentioned this pull request Dec 20, 2021

[release] 0.19.0 #1186

Merged

shonfeder mentioned this pull request Jan 12, 2022

Fix expansion of ~ in configured paths #1208

Merged

3 tasks

shonfeder deleted the shon/1069/add-config-mgr branch February 4, 2022 14:53

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add ConfigManager #1160

Add ConfigManager #1160

shonfeder commented Dec 8, 2021 •

edited

Loading

konnov left a comment

konnov Dec 15, 2021

shonfeder Dec 15, 2021

konnov Dec 15, 2021

shonfeder Dec 15, 2021

konnov Dec 15, 2021

shonfeder Dec 15, 2021

Kukovec left a comment

Kukovec Dec 15, 2021

shonfeder Dec 15, 2021

Kukovec Dec 15, 2021

shonfeder Dec 15, 2021

Kukovec Dec 15, 2021

Kukovec Dec 15, 2021

shonfeder Dec 15, 2021

shonfeder Dec 15, 2021

shonfeder Dec 15, 2021

shonfeder Dec 15, 2021

shonfeder Dec 15, 2021

		Local configuration files support JSON and the JSON superset
		[HOCON](/~https://github.com/lightbend/config/blob/master/HOCON.md).

Add ConfigManager #1160

Add ConfigManager #1160

Conversation

shonfeder commented Dec 8, 2021 • edited Loading

Changes:

Routine:

konnov left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Kukovec left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder commented Dec 8, 2021 •

edited

Loading