-
Notifications
You must be signed in to change notification settings - Fork 19
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Enable always using the latest nightly Dafny release #196
Enable always using the latest nightly Dafny release #196
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm looking forward to use that extension more often !
Thank you very much for making nightly version available.
Just a question, do you know if it will re-trigger installation at every startup? Or do I have to reinstall the extension every day?
version = LanguageServerConstants.LatestVersion; | ||
break; | ||
case LanguageServerConstants.LatestNightly: { | ||
const result: any = await (await fetch('https://api.github.com/repos/dafny-lang/dafny/releases/tags/nightly')).json(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Out of curiosity, will this be cleaner in the future if we start fetching the dlls from nuget instead?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would like the LSP server to be one of the commands in the Dafny CLI, so you would need to install the nightly build of the CLI dotnet tool. Maybe dotnet tool search --prerelease dafny
can provide us with a list of versions, and then dotnet tool install --tool-path=<something_containing_version> --version=<version>
can do the installation.
Co-authored-by: Robin Salkeld <[email protected]>
Co-authored-by: Mikaël Mayer <[email protected]>
It will retrigger |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great caching. Two more suggestions and I'm done I think.
src/language/dafnyInstallation.ts
Outdated
} | ||
window.showWarningMessage('Failed to install latest nightly version of Dafny'); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since we are not going to expect this message very often, could you make it more meaningful like this?
window.showWarningMessage('Failed to install latest nightly version of Dafny'); | |
window.showWarningMessage(`Failed to install latest nightly version of Dafny (got ${result.name})`); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
But it's always undefined in this case right? Do you mean to put result
in there? That seems like it would be spilling quite some internals to the user.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The path condition for this to happen is:
result.name === undefined || !name.startsWith('Dafny ')
so if result.name is undefined, we'll see (got )
and if the name does not start with Dafny
, we will see something like (got dafny lowercase)
.
So not the whole result, only the name (which we could use to help troubleshooting).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Tiny requested changes
src/language/dafnyInstallation.ts
Outdated
return getConfiguredTagAndVersionCache; | ||
} | ||
|
||
async function getConfiguredTagAndVersionUncached(): Promise<[string, string]> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
async function getConfiguredTagAndVersionUncached(): Promise<[string, string]> { | |
async function getConfiguredGitTagAndVersionUncached(): Promise<[string, string]> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How about putting that information in the method name, then it doesn't go out of date so easily?
Do you want to rename getConfiguredTagAndVersionUncached
to getConfiguredGitTagAndVersionUncached
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, yes, the fact that the tag is a git tag was important to me. Funny enough, when I was looking at the signature, I was trying to understand what the return type was without looking at the function's name, so I guessed it based on the function's content.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great job. Let's have it as part of our next release!
Changes
Add an option "latest nightly" at the end of the "Preferred version" list, that will cause the IDE to download and use the latest nightly Dafny release
Testing
Manually configured the IDE to use the latest nightly and used that, and the same for 3.7.