Refactor

Source/DafnyCore/DooFile.cs

@@ -168,22 +168,18 @@ public class ManifestData {
  return null;
  }
 
- return CheckAndGetLibraryOptions(reporter, file, options, origin, Manifest.Options,
- ImmutableDictionary<Option, OptionCompatibility.OptionCheck>.Empty);
+ return CheckAndGetLibraryOptions(reporter, file, options, origin, Manifest.Options);
  }
 
  public static DafnyOptions? CheckAndGetLibraryOptions(ErrorReporter reporter,
  Uri libraryFile,
  DafnyOptions options, IToken origin,
- IDictionary<string, object> libraryOptions,
- ImmutableDictionary<Option, OptionCompatibility.OptionCheck> additionalOptions) {
+ IDictionary<string, object> libraryOptions) {
  var result = new DafnyOptions(options);
  var success = true;
- var totalOptions = additionalOptions.Merge(OptionChecks,
- (_, _) => throw new InvalidOperationException());
 
  var relevantOptions = options.Options.OptionArguments.Keys.ToHashSet();
- foreach (var (option, check) in totalOptions) {
+ foreach (var (option, check) in OptionChecks) {
  // It's important to only look at the options the current command uses,
  // because other options won't be initialized to the correct default value.
  // See CommandRegistry.Create().

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -579,7 +579,7 @@ public enum DefaultFunctionOpacityOptions {
  DooFile.RegisterNoChecksNeeded(LogLevelOption, false);
  DooFile.RegisterNoChecksNeeded(ManualTriggerOption, true);
  DooFile.RegisterNoChecksNeeded(ShowHints, false);
- DooFile.RegisterNoChecksNeeded(Libraries, false);
+ DooFile.RegisterNoChecksNeeded(Libraries, true);
  DooFile.RegisterNoChecksNeeded(Output, false);
  DooFile.RegisterNoChecksNeeded(PluginOption, false);
  DooFile.RegisterNoChecksNeeded(Prelude, false);

Source/DafnyDriver/DafnyNewCli.cs

@@ -273,10 +273,7 @@ public static class DafnyNewCli {
 
  var dependencyProject = await DafnyProject.Open(fileSystem, options, uri, uriOrigin);
  var dependencyOptions =
- DooFile.CheckAndGetLibraryOptions(reporter, uri, options, uriOrigin, dependencyProject.Options,
- ImmutableDictionary<Option, OptionCompatibility.OptionCheck>.Empty.SetItem(
- CommonOptionBag.Libraries, OptionCompatibility.NoOpOptionCheck)
- );
+ DooFile.CheckAndGetLibraryOptions(reporter, uri, options, uriOrigin, dependencyProject.Options);
  if (dependencyOptions == null) {
  yield break;
  }