feat: Set DAFNY_VERSION environment variable

README.md

@@ -19,5 +19,10 @@ If you need to use a specific version:
     dafny-version: "2.3.0"
 ```
 
+You can also use `nightly-latest` to install the most recent nightly pre-release.
+
+This action sets a DAFNY_VERSION environment variable for the benefit of subsequent steps
+containing the actual resolved Dafny version: particularly useful for `nightly-latest`!
+
 This action transparently works on macOS by detecting the running OS. You can
 just set `runs-on` to a macOS virtual environment like `macos-latest`.

__tests__/verify-dafny.sh

@@ -30,3 +30,12 @@ if ! echo "$dafny_version" | grep -qi "Dafny $expectedVersionString"; then
   echo "Unexpected version" 1>&2
   exit 1
 fi
+
+# check the DAFNY_VERSION environment variable as well
+# (which is more useful when installing nightly versions)
+
+if [[ $expectedVersionString != "" && $DAFNY_VERSION != $expectedVersionString ]]
+then
+  echo "DAFNY_VERSION not set correctly: $DAFNY_VERSION"
+	exit 1
+fi

dist/index.js

@@ -6695,8 +6695,12 @@ const os = __nccwpck_require__(2037);
   try {
     const version = core.getInput("dafny-version", { required: true });
     const distribution = getDistribution(os.platform(), version);
-    const url = await dafnyURL(version, distribution);
+    const { url, fullVersion } = await dafnyURLAndFullVersion(
+      version,
+      distribution
+    );
 
+    core.info(`Dafny Version: ${fullVersion}`);
     core.info(`Dafny Url: ${url}`);
     core.info(`Dafny Distribution: ${distribution}`);
 
@@ -6711,6 +6715,8 @@ const os = __nccwpck_require__(2037);
     // Hopefully in the future we can install Dafny itself this way as well.
     // For now the zipped releases are simpler because they include Z3.
     await installDotnetTool("dafny-reportgenerator", "1.*");
+
+    core.exportVariable("DAFNY_VERSION", fullVersion);
   } catch (error) {
     core.setFailed(error.message);
   }
@@ -6728,23 +6734,34 @@ async function installDotnetTool(toolName, version) {
 }
 
 // Export functions for testing
-exports.dafnyURL = dafnyURL;
+exports.dafnyURLAndFullVersion = dafnyURLAndFullVersion;
 exports.getDistribution = getDistribution;
-exports.latestNightlyVersionFromDotnetToolSearch =
-  latestNightlyVersionFromDotnetToolSearch;
+exports.resolveNightlyVersionFromDotnetToolSearch =
+  resolveNightlyVersionFromDotnetToolSearch;
 
-async function dafnyURL(version, distribution) {
+async function dafnyURLAndFullVersion(version, distribution) {
   const versionPath = version.startsWith("nightly") ? "nightly" : `v${version}`;
-  if (version == "nightly-latest") {
-    version = await latestNightlyVersion();
+  var fullVersion;
+  if (version.startsWith("nightly")) {
+    fullVersion = await resolveNightlyVersion(version);
+    // Slice off the "3.11.0.50201-" from 3.11.0.50201-nightly-2023-02-13-14bc57f, for e.g.
+    version = fullVersion.slice(fullVersion.indexOf("-") + 1);
+  } else {
+    fullVersion = version;
   }
   const root = "https://github.com/dafny-lang/dafny/releases/download";
-  return `${root}/${versionPath}/dafny-${
+  const url = `${root}/${versionPath}/dafny-${
     version == "2.3.0" ? "2.3.0.10506" : version
   }-x64-${distribution}.zip`;
+  return { url, fullVersion };
 }
 
-async function latestNightlyVersion() {
+async function resolveNightlyVersion(nightlyVersion) {
+  const output = await dotnetToolSearch();
+  return resolveNightlyVersionFromDotnetToolSearch(output, nightlyVersion);
+}
+
+async function dotnetToolSearch() {
   const { exitCode, stdout, stderr } = await exec.getExecOutput(
     "dotnet",
     ["tool", "search", "Dafny", "--detail", "--prerelease"],
@@ -6755,10 +6772,10 @@ async function latestNightlyVersion() {
       `dotnet tool command failed (exitCode ${exitCode}):\n${stderr}"`
     );
   }
-  return latestNightlyVersionFromDotnetToolSearch(stdout);
+  return stdout;
 }
 
-function latestNightlyVersionFromDotnetToolSearch(output) {
+function resolveNightlyVersionFromDotnetToolSearch(output, nightlyVersion) {
   // Shamelessly copied and modified from dafny-lang/ide-vscode.
   // Parsing the dotnet tool output is obviously not great,
   // and we could consider using the NuGet API in the future.
@@ -6777,18 +6794,28 @@ function latestNightlyVersionFromDotnetToolSearch(output) {
     .map((versionLine) => versionLine.trimStart().split(" ")[0]);
 
   const nightlies = versions.filter((l) => l.includes("nightly"));
-  const dates = nightlies.map((nightly) => {
-    const date = new Date(nightly.split("-").slice(2, 5).join("-"));
-    return { nightly, date };
-  });
-  dates.sort((a, b) => (a.date < b.date ? 1 : -1));
-  const toolVersion = dates[0].nightly;
-
-  // Slice off the "3.11.0.50201-" from 3.11.0.50201-nightly-2023-02-13-14bc57f, for e.g.
-  const version = toolVersion.slice(toolVersion.indexOf("-") + 1);
+  var toolVersion;
+  if (nightlyVersion == "nightly-latest") {
+    const dates = nightlies.map((nightly) => {
+      const date = new Date(nightly.split("-").slice(2, 5).join("-"));
+      return { nightly, date };
+    });
+    dates.sort((a, b) => (a.date < b.date ? 1 : -1));
+    toolVersion = dates[0].nightly;
+  } else {
+    const matchingVersions = versions.filter((nightly) =>
+      nightly.includes(nightlyVersion)
+    );
+    if (matchingVersions.length != 1) {
+      throw new Error(
+        `Did not find exactly one version matching ${nightlyVersion}: ${matchingVersions}"`
+      );
+    }
+    toolVersion = matchingVersions[0];
+  }
 
-  core.info(`Using latest nightly version: ${version}`);
-  return version;
+  core.info(`Using nightly version: ${toolVersion}`);
+  return toolVersion;
 }
 
 function versionToNumeric(version) {

index.js

@@ -7,8 +7,12 @@ const os = require("os");
   try {
     const version = core.getInput("dafny-version", { required: true });
     const distribution = getDistribution(os.platform(), version);
-    const url = await dafnyURL(version, distribution);
+    const { url, fullVersion } = await dafnyURLAndFullVersion(
+      version,
+      distribution
+    );
 
+    core.info(`Dafny Version: ${fullVersion}`);
     core.info(`Dafny Url: ${url}`);
     core.info(`Dafny Distribution: ${distribution}`);
 
@@ -23,6 +27,8 @@ const os = require("os");
     // Hopefully in the future we can install Dafny itself this way as well.
     // For now the zipped releases are simpler because they include Z3.
     await installDotnetTool("dafny-reportgenerator", "1.*");
+
+    core.exportVariable("DAFNY_VERSION", fullVersion);
   } catch (error) {
     core.setFailed(error.message);
   }
@@ -40,23 +46,34 @@ async function installDotnetTool(toolName, version) {
 }
 
 // Export functions for testing
-exports.dafnyURL = dafnyURL;
+exports.dafnyURLAndFullVersion = dafnyURLAndFullVersion;
 exports.getDistribution = getDistribution;
-exports.latestNightlyVersionFromDotnetToolSearch =
-  latestNightlyVersionFromDotnetToolSearch;
+exports.resolveNightlyVersionFromDotnetToolSearch =
+  resolveNightlyVersionFromDotnetToolSearch;
 
-async function dafnyURL(version, distribution) {
+async function dafnyURLAndFullVersion(version, distribution) {
   const versionPath = version.startsWith("nightly") ? "nightly" : `v${version}`;
-  if (version == "nightly-latest") {
-    version = await latestNightlyVersion();
+  var fullVersion;
+  if (version.startsWith("nightly")) {
+    fullVersion = await resolveNightlyVersion(version);
+    // Slice off the "3.11.0.50201-" from 3.11.0.50201-nightly-2023-02-13-14bc57f, for e.g.
+    version = fullVersion.slice(fullVersion.indexOf("-") + 1);
+  } else {
+    fullVersion = version;
   }
   const root = "https://github.com/dafny-lang/dafny/releases/download";
-  return `${root}/${versionPath}/dafny-${
+  const url = `${root}/${versionPath}/dafny-${
     version == "2.3.0" ? "2.3.0.10506" : version
   }-x64-${distribution}.zip`;
+  return { url, fullVersion };
+}
+
+async function resolveNightlyVersion(nightlyVersion) {
+  const output = await dotnetToolSearch();
+  return resolveNightlyVersionFromDotnetToolSearch(output, nightlyVersion);
 }
 
-async function latestNightlyVersion() {
+async function dotnetToolSearch() {
   const { exitCode, stdout, stderr } = await exec.getExecOutput(
     "dotnet",
     ["tool", "search", "Dafny", "--detail", "--prerelease"],
@@ -67,10 +84,10 @@ async function latestNightlyVersion() {
       `dotnet tool command failed (exitCode ${exitCode}):\n${stderr}"`
     );
   }
-  return latestNightlyVersionFromDotnetToolSearch(stdout);
+  return stdout;
 }
 
-function latestNightlyVersionFromDotnetToolSearch(output) {
+function resolveNightlyVersionFromDotnetToolSearch(output, nightlyVersion) {
   // Shamelessly copied and modified from dafny-lang/ide-vscode.
   // Parsing the dotnet tool output is obviously not great,
   // and we could consider using the NuGet API in the future.
@@ -89,18 +106,28 @@ function latestNightlyVersionFromDotnetToolSearch(output) {
     .map((versionLine) => versionLine.trimStart().split(" ")[0]);
 
   const nightlies = versions.filter((l) => l.includes("nightly"));
-  const dates = nightlies.map((nightly) => {
-    const date = new Date(nightly.split("-").slice(2, 5).join("-"));
-    return { nightly, date };
-  });
-  dates.sort((a, b) => (a.date < b.date ? 1 : -1));
-  const toolVersion = dates[0].nightly;
-
-  // Slice off the "3.11.0.50201-" from 3.11.0.50201-nightly-2023-02-13-14bc57f, for e.g.
-  const version = toolVersion.slice(toolVersion.indexOf("-") + 1);
-
-  core.info(`Using latest nightly version: ${version}`);
-  return version;
+  var toolVersion;
+  if (nightlyVersion == "nightly-latest") {
+    const dates = nightlies.map((nightly) => {
+      const date = new Date(nightly.split("-").slice(2, 5).join("-"));
+      return { nightly, date };
+    });
+    dates.sort((a, b) => (a.date < b.date ? 1 : -1));
+    toolVersion = dates[0].nightly;
+  } else {
+    const matchingVersions = versions.filter((nightly) =>
+      nightly.includes(nightlyVersion)
+    );
+    if (matchingVersions.length != 1) {
+      throw new Error(
+        `Did not find exactly one version matching ${nightlyVersion}: ${matchingVersions}"`
+      );
+    }
+    toolVersion = matchingVersions[0];
+  }
+
+  core.info(`Using nightly version: ${toolVersion}`);
+  return toolVersion;
 }
 
 function versionToNumeric(version) {

test/setup-dafny-action.js

@@ -1,47 +1,58 @@
 const {
-  dafnyURL,
+  dafnyURLAndFullVersion,
   getDistribution,
-  latestNightlyVersionFromDotnetToolSearch,
+  resolveNightlyVersionFromDotnetToolSearch,
 } = require("../index");
 const { expect } = require("chai");
 
-describe("dafnyURL", () => {
+describe("dafnyURLAndFullVersion", () => {
   it("basic usage", async () => {
-    const test = await dafnyURL("3.8.1", "win");
-    expect(test).to.equal(
+    const { url, fullVersion } = await dafnyURLAndFullVersion("3.8.1", "win");
+    expect(url).to.equal(
       "https://github.com/dafny-lang/dafny/releases/download/v3.8.1/dafny-3.8.1-x64-win.zip"
     );
+    expect(fullVersion).to.equal("3.8.1");
   });
 
   it("nightly usage", async () => {
-    const test = await dafnyURL("nightly-2022-09-23-2bc0042", "ubuntu-16.04");
-    expect(test).to.equal(
+    const { url, fullVersion } = await dafnyURLAndFullVersion(
+      "nightly-2022-09-23-2bc0042",
+      "ubuntu-16.04"
+    );
+    expect(url).to.equal(
       "https://github.com/dafny-lang/dafny/releases/download/nightly/dafny-nightly-2022-09-23-2bc0042-x64-ubuntu-16.04.zip"
     );
-  });
+    expect(fullVersion).to.equal("3.8.1.40901-nightly-2022-09-23-2bc0042");
+  }).timeout(20_000); // Invoking and parsing the output of `dotnet tool search` can take well over 2 seconds
 
   it("latest nightly parsing logic", async () => {
-    const test = latestNightlyVersionFromDotnetToolSearch(
-      sampleDotnetToolSearchOutput
+    const test = resolveNightlyVersionFromDotnetToolSearch(
+      sampleDotnetToolSearchOutput,
+      "nightly-latest"
     );
-    expect(test).to.equal("nightly-2023-02-15-567a5ba");
+    expect(test).to.equal("3.11.0.50201-nightly-2023-02-15-567a5ba");
   });
 
   it("latest nightly usage", async () => {
-    const test = await dafnyURL("nightly-latest", "ubuntu-16.04");
-    expect(test).to.match(
+    const { url, fullVersion } = await dafnyURLAndFullVersion(
+      "nightly-latest",
+      "ubuntu-16.04"
+    );
+    expect(url).to.match(
       /^https:\/\/github.com\/dafny-lang\/dafny\/releases\/download\/nightly\/dafny-nightly-/
     );
+    expect(fullVersion).to.contain("nightly");
   }).timeout(20_000); // Invoking and parsing the output of `dotnet tool search` can take well over 2 seconds
 
   it("version 2.3.0", async () => {
-    const test = await dafnyURL("2.3.0", "win");
+    const { url, fullVersion } = await dafnyURLAndFullVersion("2.3.0", "win");
     // https://github.com/dafny-lang/dafny/releases/download/v2.3.0/dafny-2.3.0.10506-x64-osx-10.14.1.zip
     // https://github.com/dafny-lang/dafny/releases/download/v2.3.0/dafny-2.3.0.10506-x64-ubuntu-16.04.zip
     // https://github.com/dafny-lang/dafny/releases/download/v2.3.0/dafny-2.3.0.10506-x64-win.zip
-    expect(test).to.equal(
+    expect(url).to.equal(
       "https://github.com/dafny-lang/dafny/releases/download/v2.3.0/dafny-2.3.0.10506-x64-win.zip"
     );
+    expect(fullVersion).to.equal("2.3.0");
   });
 });