Adding a check that libraries verify to nightly testing

[davidcok]

This workflow can be a template (and changed to be reusuable) to test that a current build behaves acceptably on a given source code tree.

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

[robin-aws]

I had actually been thinking we would have our CI just check the latest result of the nightly check on libraries, similar to how we check our own nightly build, rather than actually testing it directly. Doing it directly just adds more synchronous CI load to every PR.

Regardless, also note that we should not make this a required check, because otherwise someone can add code to libraries that happens to not work with the latest unreleased Dafny and break our CI.

Mea culpa for not being clearer in offline conversations.

[davidcok]

A check of the latest nightly for libraries checks that the current library master branch is OK against recent releases of dafny.

You are correct that what I implemented checks current library master against current dafny.

So perhaps we need a check of current dafny against releases of the library (which would mean we need to start making releases).

What happened with 4.1.0 is that 4.1.0 dafny was released but it did not successfully verify the library -- and we did not realize it until I thought to add 4.1.0 to the list of dafny versions the library nightly checks. So I still think we need some nightly check of dafny vs library, even if it is not required and even if it is only nightly (and not every PR).

[robin-aws]

So perhaps we need a check of current dafny against releases of the library (which would mean we need to start making releases).

I don't think that makes a material difference, either way we still have the possibility of libraries getting a new commit/release that works with the latest released Dafny, but not Dafny master.

What happened with 4.1.0 is that 4.1.0 dafny was released but it did not successfully verify the library -- and we did not realize it until I thought to add 4.1.0 to the list of dafny versions the library nightly checks. So I still think we need some nightly check of dafny vs library, even if it is not required and even if it is only nightly (and not every PR).

Agreed (in this case we did know that the JSON code wouldn't verify under 4.1 and elected to fix that afterwards, but your point stands). I'm just saying that libraries itself is already doing this exact check, and I'd rather have dafny's CI just look for its result rather than duplicate the effort.