Skip to content

Commit 9384651

Browse files
mhuisimhuisi
authored
feat: better error message for windows antivirus cache errors (#624)
This PR adjusts the error message that is reported on Windows when Lake commands fail while fetching build cache artifacts to suggest that the issue might have been caused by a third-party antivirus, linking to the setup guide with steps to fix the issue.
1 parent 9b32ef6 commit 9384651

File tree

5 files changed

+161
-93
lines changed

5 files changed

+161
-93
lines changed

‎vscode-lean4/package.json‎

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -525,6 +525,12 @@
525525
"title": "Moogle: Search",
526526
"description": "Show MoogleView"
527527
},
528+
{
529+
"command": "lean4.troubleshooting.showTroubleshootingGuide",
530+
"category": "Lean 4: Troubleshooting",
531+
"title": "Show Troubleshooting Guide",
532+
"description": "Show 'Troubleshooting' page in setup guide"
533+
},
528534
{
529535
"command": "lean4.troubleshooting.showOutput",
530536
"category": "Lean 4",
@@ -962,6 +968,9 @@
962968
{
963969
"command": "lean4.moogle.search"
964970
},
971+
{
972+
"command": "lean4.troubleshooting.showTroubleshootingGuide"
973+
},
965974
{
966975
"command": "lean4.troubleshooting.showOutput"
967976
},
@@ -1079,15 +1088,20 @@
10791088
"group": "4_search@2"
10801089
},
10811090
{
1082-
"command": "lean4.troubleshooting.showOutput",
1091+
"command": "lean4.troubleshooting.showTroubleshootingGuide",
10831092
"when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
10841093
"group": "5_troubleshooting@1"
10851094
},
10861095
{
1087-
"command": "lean4.troubleshooting.showSetupInformation",
1096+
"command": "lean4.troubleshooting.showOutput",
10881097
"when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
10891098
"group": "5_troubleshooting@2"
10901099
},
1100+
{
1101+
"command": "lean4.troubleshooting.showSetupInformation",
1102+
"when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
1103+
"group": "5_troubleshooting@3"
1104+
},
10911105
{
10921106
"submenu": "lean4.titlebar.versions",
10931107
"when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
@@ -1533,7 +1547,6 @@
15331547
"workspace"
15341548
],
15351549
"activationEvents": [
1536-
"onLanguage:lean",
15371550
"onLanguage:markdown",
15381551
"onStartupFinished"
15391552
],

‎vscode-lean4/src/extension.ts‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,13 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled
8484
commands.registerCommand('lean4.docs.showSetupGuide', () =>
8585
commands.executeCommand('workbench.action.openWalkthrough', 'leanprover.lean4#lean4.welcome', false),
8686
),
87+
commands.registerCommand('lean4.troubleshooting.showTroubleshootingGuide', () =>
88+
commands.executeCommand(
89+
'workbench.action.openWalkthrough',
90+
{ category: 'leanprover.lean4#lean4.welcome', step: 'lean4.welcome.help' },
91+
false,
92+
),
93+
),
8794
commands.registerCommand('lean4.docs.showDocResources', () =>
8895
commands.executeCommand('simpleBrowser.show', 'https://lean-lang.org/documentation/'),
8996
),

‎vscode-lean4/src/projectinit.ts‎

Lines changed: 21 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ import {
1010
} from './utils/batch'
1111
import { elanStableChannel } from './utils/elan'
1212
import { ExtUri, extUriToCwdUri, FileUri } from './utils/exturi'
13-
import { FetchMathlibCacheResult, lake } from './utils/lake'
13+
import { displayLakeRunnerError, FetchMathlibCacheResult, lake, LakeRunnerResult } from './utils/lake'
1414
import { LeanInstaller } from './utils/leanInstaller'
1515
import { displayNotification, displayNotificationWithInput } from './utils/notifs'
1616
import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo'
@@ -91,18 +91,18 @@ export class ProjectInitializationProvider implements Disposable {
9191
return
9292
}
9393

94-
const buildResult: ExecutionResult = await lake({
94+
const buildResult: LakeRunnerResult = await lake({
9595
channel: this.channel,
9696
cwdUri: projectFolder,
9797
context: createStandaloneProjectContext,
9898
toolchain,
9999
toolchainUpdateMode: 'UpdateAutomatically',
100100
}).build()
101-
if (buildResult.exitCode === ExecutionExitCode.Cancelled) {
101+
if (buildResult.kind === 'Cancelled') {
102102
return
103103
}
104-
if (buildResult.exitCode !== ExecutionExitCode.Success) {
105-
displayResultError(buildResult, 'Cannot build Lean project.')
104+
if (buildResult.kind !== 'Success') {
105+
displayLakeRunnerError(buildResult, 'Cannot build Lean project.')
106106
return
107107
}
108108

@@ -144,23 +144,23 @@ export class ProjectInitializationProvider implements Disposable {
144144
)
145145
return
146146
}
147-
if (cacheGetResult.result.exitCode !== ExecutionExitCode.Success) {
148-
displayResultError(cacheGetResult.result, 'Cannot fetch Mathlib build artifact cache.')
147+
if (cacheGetResult.kind !== 'Success') {
148+
displayLakeRunnerError(cacheGetResult, 'Cannot fetch Mathlib build artifact cache.')
149149
return
150150
}
151151

152-
const buildResult: ExecutionResult = await lake({
152+
const buildResult: LakeRunnerResult = await lake({
153153
channel: this.channel,
154154
cwdUri: projectFolder,
155155
context: createMathlibProjectContext,
156156
toolchain: mathlibToolchain,
157157
toolchainUpdateMode: 'UpdateAutomatically',
158158
}).build()
159-
if (buildResult.exitCode === ExecutionExitCode.Cancelled) {
159+
if (buildResult.kind === 'Cancelled') {
160160
return
161161
}
162-
if (buildResult.exitCode !== ExecutionExitCode.Success) {
163-
displayResultError(buildResult, 'Cannot build Lean project.')
162+
if (buildResult.kind !== 'Success') {
163+
displayLakeRunnerError(buildResult, 'Cannot build Lean project.')
164164
return
165165
}
166166

@@ -199,30 +199,33 @@ export class ProjectInitializationProvider implements Disposable {
199199
}
200200

201201
const projectName: string = projectFolder.baseName()
202-
const result: ExecutionResult = await lake({
202+
const result: LakeRunnerResult = await lake({
203203
channel: this.channel,
204204
cwdUri: projectFolder,
205205
context,
206206
toolchain,
207207
toolchainUpdateMode: 'UpdateAutomatically',
208208
}).initProject(projectName, kind)
209-
if (result.exitCode !== ExecutionExitCode.Success) {
210-
displayResultError(result, 'Cannot initialize project.')
209+
if (result.kind === 'Cancelled') {
210+
return 'DidNotComplete'
211+
}
212+
if (result.kind !== 'Success') {
213+
displayLakeRunnerError(result, 'Cannot initialize project.')
211214
return 'DidNotComplete'
212215
}
213216

214-
const updateResult: ExecutionResult = await lake({
217+
const updateResult: LakeRunnerResult = await lake({
215218
channel: this.channel,
216219
cwdUri: projectFolder,
217220
context,
218221
toolchain,
219222
toolchainUpdateMode: 'UpdateAutomatically',
220223
}).updateDependencies()
221-
if (updateResult.exitCode === ExecutionExitCode.Cancelled) {
224+
if (updateResult.kind === 'Cancelled') {
222225
return 'DidNotComplete'
223226
}
224-
if (updateResult.exitCode !== ExecutionExitCode.Success) {
225-
displayResultError(updateResult, 'Cannot update dependencies.')
227+
if (updateResult.kind !== 'Success') {
228+
displayLakeRunnerError(updateResult, 'Cannot update dependencies.')
226229
return 'DidNotComplete'
227230
}
228231

‎vscode-lean4/src/projectoperations.ts‎

Lines changed: 33 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,16 @@ import * as fs from 'fs'
22
import { join } from 'path'
33
import { commands, Disposable, OutputChannel, QuickPickItem, window } from 'vscode'
44
import { LeanClient } from './leanclient'
5-
import { batchExecute, displayResultError, ExecutionExitCode, ExecutionResult } from './utils/batch'
5+
import { batchExecute, ExecutionExitCode, ExecutionResult } from './utils/batch'
66
import { LeanClientProvider } from './utils/clientProvider'
7-
import { FetchMathlibCacheResult, lake, LakeRunner } from './utils/lake'
7+
import {
8+
CacheGetAvailabilityResult,
9+
displayLakeRunnerError,
10+
FetchMathlibCacheResult,
11+
lake,
12+
LakeRunner,
13+
LakeRunnerResult,
14+
} from './utils/lake'
815
import { lean } from './utils/leanEditorProvider'
916
import { DirectGitDependency, Manifest, ManifestReadError, parseManifestInFolder } from './utils/manifest'
1017
import { displayNotification, displayNotificationWithInput, displayNotificationWithOptionalInput } from './utils/notifs'
@@ -38,12 +45,12 @@ export class ProjectOperationProvider implements Disposable {
3845
return
3946
}
4047

41-
const result: ExecutionResult = await lakeRunner.build()
42-
if (result.exitCode === ExecutionExitCode.Cancelled) {
48+
const result: LakeRunnerResult = await lakeRunner.build()
49+
if (result.kind === 'Cancelled') {
4350
return
4451
}
45-
if (result.exitCode !== ExecutionExitCode.Success) {
46-
displayResultError(result, 'Cannot build project.')
52+
if (result.kind !== 'Success') {
53+
displayLakeRunnerError(result, 'Cannot build project.')
4754
return
4855
}
4956

@@ -64,23 +71,27 @@ export class ProjectOperationProvider implements Disposable {
6471
}
6572

6673
await this.runOperation('Clean Project', async lakeRunner => {
67-
const cleanResult: ExecutionResult = await lakeRunner.clean()
68-
if (cleanResult.exitCode === ExecutionExitCode.Cancelled) {
74+
const cleanResult: LakeRunnerResult = await lakeRunner.clean()
75+
if (cleanResult.kind === 'Cancelled') {
6976
return
7077
}
71-
if (cleanResult.exitCode !== ExecutionExitCode.Success) {
72-
displayResultError(cleanResult, 'Cannot delete build artifacts.')
78+
if (cleanResult.kind !== 'Success') {
79+
displayLakeRunnerError(cleanResult, 'Cannot delete build artifacts.')
7380
return
7481
}
7582

76-
const checkResult: 'Available' | 'Unavailable' | 'Cancelled' = await lakeRunner.isMathlibCacheGetAvailable()
77-
if (checkResult === 'Cancelled') {
83+
const checkResult: CacheGetAvailabilityResult = await lakeRunner.isMathlibCacheGetAvailable()
84+
if (checkResult.kind === 'Cancelled') {
7885
return
7986
}
80-
if (checkResult === 'Unavailable') {
87+
if (checkResult.kind === 'CacheUnavailable') {
8188
displayNotification('Information', 'Project cleaned successfully.')
8289
return
8390
}
91+
if (checkResult.kind !== 'CacheAvailable') {
92+
displayLakeRunnerError(checkResult, 'Cannot check availability of Mathlib cache.')
93+
return
94+
}
8495

8596
const fetchMessage = "Project cleaned successfully. Do you wish to fetch Mathlib's build artifact cache?"
8697
const fetchInput = 'Fetch Cache'
@@ -112,11 +123,8 @@ export class ProjectOperationProvider implements Disposable {
112123
displayNotification('Error', 'This command cannot be used in non-Mathlib projects.')
113124
return
114125
}
115-
if (fetchResult.result.exitCode === ExecutionExitCode.Cancelled) {
116-
return
117-
}
118-
if (fetchResult.result.exitCode !== ExecutionExitCode.Success) {
119-
displayResultError(fetchResult.result, 'Cannot fetch Mathlib build artifact cache.')
126+
if (fetchResult.kind !== 'Success') {
127+
displayLakeRunnerError(fetchResult, 'Cannot fetch Mathlib build artifact cache.')
120128
return
121129
}
122130

@@ -182,12 +190,9 @@ export class ProjectOperationProvider implements Disposable {
182190
displayNotification('Error', 'This command cannot be used in non-Mathlib projects.')
183191
return
184192
}
185-
if (fetchResult.result.exitCode === ExecutionExitCode.Cancelled) {
186-
return
187-
}
188-
if (fetchResult.result.exitCode !== ExecutionExitCode.Success) {
189-
displayResultError(
190-
fetchResult.result,
193+
if (fetchResult.kind !== 'Success') {
194+
displayLakeRunnerError(
195+
fetchResult,
191196
`Cannot fetch Mathlib build artifact cache for '${relativeDocUri.fsPath}'.`,
192197
)
193198
return
@@ -260,12 +265,12 @@ export class ProjectOperationProvider implements Disposable {
260265
}
261266

262267
await this.runOperation('Update Dependency', async lakeRunner => {
263-
const result: ExecutionResult = await lakeRunner.updateDependency(dependencyChoice.name)
264-
if (result.exitCode === ExecutionExitCode.Cancelled) {
268+
const result: LakeRunnerResult = await lakeRunner.updateDependency(dependencyChoice.name)
269+
if (result.kind === 'Cancelled') {
265270
return
266271
}
267-
if (result.exitCode !== ExecutionExitCode.Success) {
268-
void displayResultError(result, 'Cannot update dependency.')
272+
if (result.kind !== 'Success') {
273+
displayLakeRunnerError(result, 'Cannot update dependency.')
269274
return
270275
}
271276

0 commit comments

Comments
 (0)
⚡