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

Refactor how options are registered #5675

Merged
merged 8 commits into from
Aug 12, 2024

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Aug 8, 2024

Description

Refactor how options are registered. Replaces the various ways of registering options by these four types:

  • Cli:
    • Can be chosen independent of libraries used.
    • Never stored
    • Can be accessed through most available DafnyOptions objects
    • Examples: --cores, --verification-time-limit, --warn-as-errors
  • Global:
    • Value chosen for root project imposes constraints on this option for all consumed projects. The constraint is configured through a separate function.
    • Stored in .doo
    • Can be accessed through most available DafnyOptions objects
    • Examples: --unicode-char, --enforce-determinism
  • Module:
    • Can be configured either through the CLI, or with an attribute at the module level
    • Stored in the doo if configured through CLI
    • Should be accessed through the instance field ModuleDecl.Options
    • Examples: --function-syntax, --manual-triggers, --warn-redundant-assumptions
  • Translation:
    • Can be different per module in program.
    • Stored in .dtr
    • Currently accessed through program.Compilation.AlreadyTranslatedRecord.OptionsByModule
    • Examples: --outer-module, --go-module-name

Follow-up

  • Load read translation records into ModuleDecl.Options and replace usages of CompilationData.AlreadyTranslatedRecord with ModuleDecl.Options,
  • Decide what to do with:
OptionRegistry.RegisterOption(OptimizeErasableDatatypeWrapper, OptionScope.Cli); // TODO needs translation record registration
OptionRegistry.RegisterOption(AddCompileSuffix, OptionScope.Cli);  // TODO needs translation record registration

How has this been tested?

It's a refactoring so no additional tests are needed.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) August 8, 2024 10:50
Comment on lines 56 to 78
// public static void RegisterLibraryCheck(Option option, OptionCompatibility.OptionCheck check) {
// if (NoChecksNeeded.Contains(option)) {
// throw new ArgumentException($"Option already registered as not needing a library check: {option.Name}");
// }
// OptionChecks.Add(option, check);
// }
//
// public static void RegisterLibraryChecks(IDictionary<Option, OptionCompatibility.OptionCheck> checks) {
// foreach (var (option, check) in checks) {
// RegisterLibraryCheck(option, check);
// }
// }
//
// public static void RegisterNoChecksNeeded(Option option, bool semantic) {
// if (semantic) {
// RegisterLibraryCheck(option, OptionCompatibility.NoOpOptionCheck);
// } else {
// if (OptionChecks.ContainsKey(option)) {
// throw new ArgumentException($"Option already registered as needing a library check: {option.Name}");
// }
// NoChecksNeeded.Add(option);
// }
// }
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: unused

Suggested change
// public static void RegisterLibraryCheck(Option option, OptionCompatibility.OptionCheck check) {
// if (NoChecksNeeded.Contains(option)) {
// throw new ArgumentException($"Option already registered as not needing a library check: {option.Name}");
// }
// OptionChecks.Add(option, check);
// }
//
// public static void RegisterLibraryChecks(IDictionary<Option, OptionCompatibility.OptionCheck> checks) {
// foreach (var (option, check) in checks) {
// RegisterLibraryCheck(option, check);
// }
// }
//
// public static void RegisterNoChecksNeeded(Option option, bool semantic) {
// if (semantic) {
// RegisterLibraryCheck(option, OptionCompatibility.NoOpOptionCheck);
// } else {
// if (OptionChecks.ContainsKey(option)) {
// throw new ArgumentException($"Option already registered as needing a library check: {option.Name}");
// }
// NoChecksNeeded.Add(option);
// }
// }

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Woops! Sorry

@@ -216,7 +215,8 @@ public class ManifestData {
result.Options.OptionArguments[option] = libraryValue;
result.ApplyBinding(option);
var prefix = $"cannot load {options.GetPrintPath(libraryFile.LocalPath)}";
success = success && check(reporter, origin, prefix, option, localValue, libraryValue);
var checkpasses = OptionRegistry.GlobalCheck(option)?.Invoke(reporter, origin, prefix, option, localValue, libraryValue) ?? true;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The CI warns that libraryValue is possibly null, is that intended?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed

@keyboardDrummer keyboardDrummer removed the request for review from robin-aws August 10, 2024 08:20
Copy link
Contributor

@alex-chew alex-chew left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@keyboardDrummer keyboardDrummer merged commit f5e5106 into dafny-lang:master Aug 12, 2024
20 of 21 checks passed
@keyboardDrummer keyboardDrummer deleted the optionRefactoring branch August 12, 2024 10:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants