Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Enable always using the latest nightly Dafny release #196

Merged
merged 12 commits into from
Jul 12, 2022
Merged

Enable always using the latest nightly Dafny release #196

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
e91ad82
Allow downloading nightly
keyboardDrummer Jul 7, 2022
0a0efba
Update src/language/dafnyInstallation.ts
keyboardDrummer Jul 8, 2022
8b20c36
Update src/extension.ts
keyboardDrummer Jul 8, 2022
a2e0698
Refactoring and show warning if nightly fails to install
keyboardDrummer Jul 8, 2022
04ec886
Make getConfiguredTagAndVersionCache thread-safe
keyboardDrummer Jul 8, 2022
72eda90
Add forgotten await
keyboardDrummer Jul 11, 2022
bbe1dee
Add troubleshooting information
keyboardDrummer Jul 12, 2022
8ca1935
Merge remote-tracking branch 'origin/master' into enableUsingNightly
keyboardDrummer Jul 12, 2022
56c34b5
Fix build error
keyboardDrummer Jul 12, 2022
4093e10
Add outDir to tscconfig.json
keyboardDrummer Jul 12, 2022
910bbce
Fix test run by doing a dynamic import of node-fetch
keyboardDrummer Jul 12, 2022
83d6743
Rename function
keyboardDrummer Jul 12, 2022
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
1 change: 0 additions & 1 deletion src/extension.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
import { Disposable, ExtensionContext, OutputChannel, window, commands } from 'vscode';
import { ExtensionConstants, LanguageServerConstants } from './constants';
import { DafnyCommands } from './commands';

import { DafnyLanguageClient } from './language/dafnyLanguageClient';
import checkAndInformAboutInstallation from './startupCheck';
import { DafnyInstaller, getLanguageServerRuntimePath, isConfiguredToInstallLatestDafny } from './language/dafnyInstallation';
Expand Down
17 changes: 14 additions & 3 deletions src/language/dafnyInstallation.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,13 @@ async function getConfiguredVersion(): Promise<string> {

let getConfiguredTagAndVersionCache: [string, string];
async function getConfiguredTagAndVersion(): Promise<[string, string]> {
return getConfiguredTagAndVersionCache ?? (getConfiguredTagAndVersionCache = await getConfiguredTagAndVersionUncached());
if(getConfiguredTagAndVersionCache === undefined) {
const result = await getConfiguredTagAndVersionUncached();
if(getConfiguredTagAndVersionCache === undefined) {
getConfiguredTagAndVersionCache = result;
}
}
return getConfiguredTagAndVersionCache;
}

async function getConfiguredTagAndVersionUncached(): Promise<[string, string]> {
Copy link
Member

@MikaelMayer MikaelMayer Jul 12, 2022 •
edited
Loading

Choose a reason for hiding this comment

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

Suggested change
async function getConfiguredTagAndVersionUncached(): Promise<[string, string]> {
async function getConfiguredGitTagAndVersionUncached(): Promise<[string, string]> {

Copy link
Member Author

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 ?

Copy link
Member

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.

Expand All @@ -44,9 +50,14 @@ async function getConfiguredTagAndVersionUncached(): Promise<[string, string]> {
case LanguageServerConstants.LatestNightly: {
const result: any = await (await fetch('https://api.github.com/repos/dafny-lang/dafny/releases/tags/nightly')).json();
Copy link
Member

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?

Copy link
Member Author

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.

if(result.name !== undefined) {
const version = result.name.substring(6);
return [ 'nightly', version ];
const name: string = result.name;
const versionPrefix = 'Dafny ';
if(name.startsWith(versionPrefix)) {
const version = name.substring(versionPrefix.length);
return [ 'nightly', version ];
}
}
window.showWarningMessage('Failed to install latest nightly version of Dafny');
Copy link
Member

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?

Suggested change
window.showWarningMessage('Failed to install latest nightly version of Dafny');
window.showWarningMessage(`Failed to install latest nightly version of Dafny (got ${result.name})`);

Copy link
Member Author

@keyboardDrummer keyboardDrummer Jul 11, 2022 •
edited
Loading

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.

Copy link
Member

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

version = LanguageServerConstants.LatestVersion;
}
}
Expand Down