Open erniecohen opened 2 months ago
I assume this is a temporary breakage, but this means a regression test should probably be added.
I assume this is a temporary breakage, but this means a regression test should probably be added.
Definitely. These reports are useful. We'll try to resolve them ASAP.
Dafny version
nightly 4/25/24
Code to produce this issue
Command to run and resulting output
What happened?
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues. System.NullReferenceException: Object reference not set to an instance of an object. at Microsoft.Dafny.ModuleResolver.AddToInheritedMembers(TopLevelDeclWithMembers cl, TopLevelDeclWithMembers baseOrParentTypeDecl, Dictionaryb0()
at Microsoft.Dafny.LanguageServer.Language.CacheExtensions.ProfileAndPruneCache[T,Key,Value](PruneIfNotUsedSinceLastPruneCacheb__0>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.ResolveAsync()
2 inheritedMembers, List
1 membersWithErrors) at Microsoft.Dafny.ModuleResolver.RegisterInheritedMembers(TopLevelDeclWithMembers cl, DPreType basePreType) at Microsoft.Dafny.PreTypeResolver.ResolvePreTypeSignature(Declaration d, PreTypeInferenceModuleState preTypeInferenceModuleState, ModuleResolver resolver) at Microsoft.Dafny.PreTypeResolver.ResolveDeclarations(List1 declarations, ModuleResolver resolver, Boolean firstPhaseOnly) at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List
1 declarations, Graph1 datatypeDependencies, Graph
1 codatatypeDependencies, String moduleDescription, Boolean isAnExport) at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName) at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>n0(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>cDisplayClass5_0.2 cache, Func
1 useCache, TelemetryPublisherBase telemetryPublisher, String programName, String activity) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.Resolve(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.TextDocumentLoader.<>cDisplayClass5_0.<What type of operating system are you experiencing the problem on?
Mac