Skip to content
Merged
Show file tree
Hide file tree
Changes from 17 commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion .github/workflows/main.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,20 @@ jobs:
fail-fast: false
matrix:
os: [macos-latest, ubuntu-latest, windows-latest]
dafny: [3.0.0, 3.7.3, 3.8.1, nightly-2022-09-23-2bc0042]
dafny: [3.0.0, 3.7.3, 3.8.1, nightly-2023-02-13-14bc57f, nightly-latest]
# Windows 2.3.0 requires mono
include:
- os: macos-latest
dafny: 2.3.0
- os: ubuntu-latest
dafny: 2.3.0
steps:
# The first call to `dotnet tool` on a fresh runner sometimes takes multiple minutes,
# perhaps because it is lazily downloading and installing assets.
# It helps to hit that here so we don't hit it in a mocha test with a tight timeout.
- name: Warm up dotnet tool
run: dotnet tool search --help

- name: Checkout
uses: actions/checkout@v2

Expand Down
2 changes: 1 addition & 1 deletion __tests__/verify-dafny.sh
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ fi
echo "Expected Dafny Version: $expectedVersionString"
dafny_version="$(dafny $version)"
echo "Found $dafny_version"
if ! echo "$dafny_version" | grep -q "Dafny $expectedVersionString"; then
if ! echo "$dafny_version" | grep -qi "Dafny $expectedVersionString"; then
echo "Unexpected version" 1>&2
exit 1
fi
69 changes: 63 additions & 6 deletions dist/index.js
Original file line number Diff line number Diff line change
Expand Up @@ -6695,7 +6695,7 @@ const os = __nccwpck_require__(2037);
try {
const version = core.getInput("dafny-version", { required: true });
const distribution = getDistribution(os.platform(), version);
const url = dafnyURL(version, distribution);
const url = await dafnyURL(version, distribution);

core.info(`Dafny Url: ${url}`);
core.info(`Dafny Distribution: ${distribution}`);
Expand All @@ -6710,29 +6710,86 @@ const os = __nccwpck_require__(2037);
// Install related tools.
// 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.*")
await installDotnetTool("dafny-reportgenerator", "1.*");
} catch (error) {
core.setFailed(error.message);
}
})();

async function installDotnetTool(toolName, version) {
await exec.exec("dotnet", ["tool", "install", "-g", toolName, "--version", version])
await exec.exec("dotnet", [
"tool",
"install",
"-g",
toolName,
"--version",
version,
]);
}

// Export functions for testing
exports.dafnyURL = dafnyURL;
exports.getDistribution = getDistribution;

function dafnyURL(version, distribution) {
async function dafnyURL(version, distribution) {
const versionPath = version.startsWith("nightly") ? "nightly" : `v${version}`;
if (version == "nightly-latest") {
version = await latestNightlyVersion();
}
const root = "https://github.com/dafny-lang/dafny/releases/download";
return `${root}/${versionPath}/dafny-${version == "2.3.0" ? "2.3.0.10506" : version}-x64-${distribution}.zip`;
return `${root}/${versionPath}/dafny-${
version == "2.3.0" ? "2.3.0.10506" : version
}-x64-${distribution}.zip`;
}

async function latestNightlyVersion() {
// 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.
// Alternatively if we move to installing Dafny using `dotnet tool install`
// we could use the `--prerelease` flag, although that assumes
// that all nightly builds use a fresh version number,
// and can't be used together with `--version` to express something like
// "install the latest 3.X version including prereleases".
const { exitCode, stdout, stderr } = await exec.getExecOutput(
"dotnet",
["tool", "search", "Dafny", "--detail", "--prerelease"],
{ silent: true }
);
if (exitCode != 0) {
throw new Error(
`dotnet tool command failed (exitCode ${exitCode}):\n${stderr}"`
);
}
const entries = stdout
.split("----------------")
.map((entry) => entry.split(/\r?\n/).filter((e) => e !== ""));
const dafnyEntry = entries.filter((entry) => entry[0] === "dafny")[0];
const versionsIndex = dafnyEntry.findIndex((v) => v.startsWith("Versions:"));
const versions = dafnyEntry
.slice(versionsIndex + 1)
.map((versionLine) => versionLine.trimStart().split(" ")[0]);

const nightlies = versions.filter((l) => l.includes("nightly"));
const dates = nightlies.map((n, index) => {
const split = n.split("-");
return { index, date: split[2] + split[3] + split[4] };
});
dates.sort((a, b) => (a.date < b.date ? 1 : -1));
const toolVersion = nightlies[dates[0].index];

// 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;
}

function getDistribution(platform, version) {
return platform === "darwin" // Osx
? version == "2.3.0" ? "osx-10.14.1" : "osx-10.14.2"
? version == "2.3.0"
? "osx-10.14.1"
: "osx-10.14.2"
: platform === "win32" // windows
? "win"
: "ubuntu-16.04"; // Everything else is linux...
Expand Down
69 changes: 63 additions & 6 deletions index.js
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ const os = require("os");
try {
const version = core.getInput("dafny-version", { required: true });
const distribution = getDistribution(os.platform(), version);
const url = dafnyURL(version, distribution);
const url = await dafnyURL(version, distribution);

core.info(`Dafny Url: ${url}`);
core.info(`Dafny Distribution: ${distribution}`);
Expand All @@ -22,29 +22,86 @@ const os = require("os");
// Install related tools.
// 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.*")
await installDotnetTool("dafny-reportgenerator", "1.*");
} catch (error) {
core.setFailed(error.message);
}
})();

async function installDotnetTool(toolName, version) {
await exec.exec("dotnet", ["tool", "install", "-g", toolName, "--version", version])
await exec.exec("dotnet", [
"tool",
"install",
"-g",
toolName,
"--version",
version,
]);
}

// Export functions for testing
exports.dafnyURL = dafnyURL;
exports.getDistribution = getDistribution;

function dafnyURL(version, distribution) {
async function dafnyURL(version, distribution) {
const versionPath = version.startsWith("nightly") ? "nightly" : `v${version}`;
if (version == "nightly-latest") {
version = await latestNightlyVersion();
}
const root = "https://github.com/dafny-lang/dafny/releases/download";
return `${root}/${versionPath}/dafny-${version == "2.3.0" ? "2.3.0.10506" : version}-x64-${distribution}.zip`;
return `${root}/${versionPath}/dafny-${
version == "2.3.0" ? "2.3.0.10506" : version
}-x64-${distribution}.zip`;
}

async function latestNightlyVersion() {
// 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.
// Alternatively if we move to installing Dafny using `dotnet tool install`
// we could use the `--prerelease` flag, although that assumes
// that all nightly builds use a fresh version number,
// and can't be used together with `--version` to express something like
// "install the latest 3.X version including prereleases".
const { exitCode, stdout, stderr } = await exec.getExecOutput(
"dotnet",
["tool", "search", "Dafny", "--detail", "--prerelease"],

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This pulls both dafny and the report, I would suggest --take 1
There is some way to query,
but I don't understand how to get the specific package ID.
https://learn.microsoft.com/en-us/nuget/api/search-query-service-resource#search-for-packages

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yup, I wouldn't want to just --take 1 though, it feels brittle to depend on the order of results.

As per my comment I'd also prefer to use the NuGet API, will timebox attempting that.

{ silent: true }
);
if (exitCode != 0) {
throw new Error(
`dotnet tool command failed (exitCode ${exitCode}):\n${stderr}"`
);
}
const entries = stdout
.split("----------------")
.map((entry) => entry.split(/\r?\n/).filter((e) => e !== ""));

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having only taken the first or removed the report generator

Suggested change
const entries = stdout
.split("----------------")
.map((entry) => entry.split(/\r?\n/).filter((e) => e !== ""));
const entries = stdout
.split('\n')
.filter(s => s.includes('-nightly-)
.map(s => s.split('Downloads:')[0].trim())

const dafnyEntry = entries.filter((entry) => entry[0] === "dafny")[0];
const versionsIndex = dafnyEntry.findIndex((v) => v.startsWith("Versions:"));
const versions = dafnyEntry
.slice(versionsIndex + 1)
.map((versionLine) => versionLine.trimStart().split(" ")[0]);

const nightlies = versions.filter((l) => l.includes("nightly"));
const dates = nightlies.map((n, index) => {
const split = n.split("-");

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You mean to compare a date,
so I would do that.

Suggested change
const split = n.split("-");
const date = new Date(n.split('-').slice(2, 5).join('-'))

return { index, date: split[2] + split[3] + split[4] };

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would just take the value n rather than the index...
Then you can just take the value right off the sorted dates

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Had that thought too when making this work initially :)

});
dates.sort((a, b) => (a.date < b.date ? 1 : -1));

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree I don't think you care about equal

const toolVersion = nightlies[dates[0].index];

// 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;

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would be best refactored into a function that takes the string.
Then we can have a test with a hard coded string...

}

function getDistribution(platform, version) {
return platform === "darwin" // Osx
? version == "2.3.0" ? "osx-10.14.1" : "osx-10.14.2"
? version == "2.3.0"
? "osx-10.14.1"
: "osx-10.14.2"
: platform === "win32" // windows
? "win"
: "ubuntu-16.04"; // Everything else is linux...
Expand Down
19 changes: 13 additions & 6 deletions test/setup-dafny-action.js
Original file line number Diff line number Diff line change
Expand Up @@ -2,22 +2,29 @@ const { dafnyURL, getDistribution } = require("../index");
const { expect } = require("chai");

describe("dafnyURL", () => {
it("basic usage", () => {
const test = dafnyURL("3.8.1", "win");
it("basic usage", async () => {
const test = await dafnyURL("3.8.1", "win");
expect(test).to.equal(
"https://github.com/dafny-lang/dafny/releases/download/v3.8.1/dafny-3.8.1-x64-win.zip"
);
});

it("nightly usage", () => {
const test = dafnyURL("nightly-2022-09-23-2bc0042", "ubuntu-16.04");
it("nightly usage", async () => {
const test = await dafnyURL("nightly-2022-09-23-2bc0042", "ubuntu-16.04");
expect(test).to.equal(
"https://github.com/dafny-lang/dafny/releases/download/nightly/dafny-nightly-2022-09-23-2bc0042-x64-ubuntu-16.04.zip"
);
});

it("version 2.3.0", () => {
const test = dafnyURL("2.3.0", "win");
it("latest nightly usage", async () => {
const test = await dafnyURL("nightly-latest", "ubuntu-16.04");
expect(test).to.match(
/^https:\/\/github.com\/dafny-lang\/dafny\/releases\/download\/nightly\/dafny-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");
// 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
Expand Down