Enable specifying a remote Dafny dependency

[keyboardDrummer]

Currently when my Dafny application depends on a Dafny library, I have to manually add that library as a submodule to my Dafny project. Instead, I would like to point to a remote URL and have the Dafny CLI take care of downloading the library to my local machine. If this requires the library to be published in a Dafny specific way, that's OK.

Implementation options

1. allow specifying a Git URL, commit and repository path, as an argument to --library, after which the Dafny CLI will ensure that the referred to repository commit is downloaded to the local machine.
2. something else, possibly building on top of an existing package repository such as NuGet, GitHub packages, AWS CodeArtefact, ...

[cpitclaudel]

I prefer multiple small tools over one big tool, and I worry about scope creep. Should Dafny.exe really be in the business of cloning git repositories?

(Regarding using --library, I would prefer it to be an action that's run separately from build / verify / etc. Maybe this is more easy to do once we have a project file. But I realize that "dotnet build" fetches dependencies agressively.)

[keyboardDrummer]

I prefer multiple small tools over one big tool, and I worry about scope creep

To optimise for the user, I think the Dafny CLI should include everything that you expect any Dafny developer will need, and I would argue that includes being able to use third-party libraries.

Should Dafny.exe really be in the business of cloning git repositories?

Maybe not, that's just an option, but to support third-party libraries it should be able to fetch those from remote locations.

[DavePearce]

To optimise for the user, I think the Dafny CLI should include everything that you expect any Dafny developer will need, and I would argue that includes being able to use third-party libraries.

I agree with this, btw. Ideally, you would have some mechanism for specifying versions in a config file (like a Rust Cargo.toml file):

[dependencies]
clap="3.1"
delta_inc="0.3.1"
log="0.4"
log4rs="1"

Initially, these could be urls to a repository with either a tag (or a commit?). Eventually you could consider adding a package repository (which can be implemented easily enough as e.g. a github repository).