robin-aws
commented
5 months ago I think this workflow is absolutely valuable, and the automatic handling of .doo files should also be applied to the library.dtr concept we're discussing adding in https://github.com/dafny-lang/dafny/pull/5140.
My only thought is that I'm not completely sure that we should just overload --library to allow this kind of indirect value. The next logical step in this kind of workflow is declaring remote dependencies somehow as well, so that instead of building the .doo/.dtr artifacts locally, we're downloading them from (most likely) NuGet. For that we'll want to specify a package identifier and version somehow instead, and I worry that automatically figuring out whether a --library string is meant to be a path or a package identifier will be messy. .NET avoids this ambiguity by having separate <ProjectReference> and <PackageReference> options in .csproj files.
To enable smoothly working with multiple projects inside a single repository, Dafny should allow using a Dafny project file as an argument to
--library. This does the following: if the given Dafny project's output folder does not contain a doo file whose checksum matches the project's sources, then first a doo file is built. After that, this doo file is passed to--library. Attempting to use an existing doo file allows not doing verification twice for repositories where multiple local projects have the same local project as a dependency.