Skip to content

Support “nightly-latest” version#13

Merged
robin-aws merged 18 commits into
dafny-lang:mainfrom
robin-aws:support-latest-nightly
Feb 16, 2023
Merged

Support “nightly-latest” version#13
robin-aws merged 18 commits into
dafny-lang:mainfrom
robin-aws:support-latest-nightly

Conversation

@robin-aws

@robin-aws robin-aws commented Feb 13, 2023

Copy link
Copy Markdown
Member

Resolves #12

@robin-aws robin-aws changed the title First crack at “latest-nightly” Support “nightly-latest” version Feb 13, 2023
@davidcok

Copy link
Copy Markdown

While you are at it, put in latest release as well

Comment thread dist/index.js Outdated
async function latestNightlyVersion() {
// Shamelessly copied and modified from dafny-lang/ide-vscode
// I'd prefer to use the GitHub API to list the assets under the "nightly" release,
// but @actions/github requires authentication.

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.

Oh I suppose I can use GITHUB_TOKEN, true. Not sure how to refactor the tests to still work though.

Comment thread index.js Outdated
@robin-aws

Copy link
Copy Markdown
Member Author

While you are at it, put in latest release as well

Actually, I'm going to leave that out for now. It goes against repeatable builds, and especially in Dafny's case automatically picking up the latest version just means being forced to immediately deal with verification variability.

@robin-aws

Copy link
Copy Markdown
Member Author

Temporarily closing to conserve dafny-lang CI resources

@robin-aws robin-aws closed this Feb 14, 2023
@robin-aws robin-aws reopened this Feb 14, 2023
@robin-aws robin-aws marked this pull request as ready for review February 14, 2023 20:49
Comment thread index.js Outdated
Comment on lines +76 to +97
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;

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...

Comment thread index.js
// "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.

Comment thread index.js Outdated
Comment on lines +76 to +78
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())

Comment thread index.js Outdated

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('-'))

Comment thread index.js
const split = n.split("-");
return { index, date: split[2] + split[3] + split[4] };
});
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

Comment thread index.js Outdated
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] };

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 :)

@seebees seebees left a comment

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.

LGTM, I would refactor the search logic, but keeping it the same as the IDE is a good idea too.

@robin-aws robin-aws merged commit ef97afb into dafny-lang:main Feb 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Support easy "latest nightly" version

3 participants