Skip to content

Commit 9b32ef6

Browse files
mhuisimhuisi
authored
feat: improve lake exe cache get error reporting (#621)
This PR ensures that the VS Code extension always reports the error that occurred when `lake exe cache get` fails in Mathlib or in a project downstream of Mathlib. Previously, this was only the case for project creation commands.
1 parent 78194a5 commit 9b32ef6

File tree

4 files changed

+127
-67
lines changed

4 files changed

+127
-67
lines changed

‎vscode-lean4/src/projectinit.ts‎

Lines changed: 15 additions & 9 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 { lake } from './utils/lake'
13+
import { FetchMathlibCacheResult, lake } from './utils/lake'
1414
import { LeanInstaller } from './utils/leanInstaller'
1515
import { displayNotification, displayNotificationWithInput } from './utils/notifs'
1616
import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo'
@@ -127,18 +127,25 @@ export class ProjectInitializationProvider implements Disposable {
127127
return
128128
}
129129

130-
const cacheGetResult: ExecutionResult = await lake({
130+
const cacheGetResult: FetchMathlibCacheResult = await lake({
131131
channel: this.channel,
132132
cwdUri: projectFolder,
133133
context: createMathlibProjectContext,
134134
toolchain: mathlibToolchain,
135135
toolchainUpdateMode: 'UpdateAutomatically',
136136
}).fetchMathlibCache()
137-
if (cacheGetResult.exitCode === ExecutionExitCode.Cancelled) {
137+
if (cacheGetResult.kind === 'Cancelled') {
138138
return
139139
}
140-
if (cacheGetResult.exitCode !== ExecutionExitCode.Success) {
141-
displayResultError(cacheGetResult, 'Cannot fetch Mathlib build artifact cache.')
140+
if (cacheGetResult.kind === 'CacheUnavailable') {
141+
displayNotification(
142+
'Error',
143+
'Cannot fetch Mathlib build artifact cache: `lake exe cache` is not available.',
144+
)
145+
return
146+
}
147+
if (cacheGetResult.result.exitCode !== ExecutionExitCode.Success) {
148+
displayResultError(cacheGetResult.result, 'Cannot fetch Mathlib build artifact cache.')
142149
return
143150
}
144151

@@ -395,14 +402,13 @@ Open this project instead?`
395402
return
396403
}
397404

398-
// Try it. If this is not a mathlib project, it will fail silently. Otherwise, it will grab the cache.
399-
const fetchResult: ExecutionResult = await lake({
405+
const fetchResult: 'Success' | 'Failure' = await lake({
400406
channel: this.channel,
401407
cwdUri: projectFolder,
402408
context: downloadProjectContext,
403409
toolchainUpdateMode: 'UpdateAutomatically',
404-
}).fetchMathlibCache(true)
405-
if (fetchResult.exitCode === ExecutionExitCode.Cancelled) {
410+
}).tryFetchMathlibCacheWithError()
411+
if (fetchResult !== 'Success') {
406412
return
407413
}
408414

‎vscode-lean4/src/projectoperations.ts‎

Lines changed: 36 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import { commands, Disposable, OutputChannel, QuickPickItem, window } from 'vsco
44
import { LeanClient } from './leanclient'
55
import { batchExecute, displayResultError, ExecutionExitCode, ExecutionResult } from './utils/batch'
66
import { LeanClientProvider } from './utils/clientProvider'
7-
import { cacheNotFoundError, lake, LakeRunner } from './utils/lake'
7+
import { FetchMathlibCacheResult, lake, LakeRunner } from './utils/lake'
88
import { lean } from './utils/leanEditorProvider'
99
import { DirectGitDependency, Manifest, ManifestReadError, parseManifestInFolder } from './utils/manifest'
1010
import { displayNotification, displayNotificationWithInput, displayNotificationWithOptionalInput } from './utils/notifs'
@@ -33,8 +33,8 @@ export class ProjectOperationProvider implements Disposable {
3333

3434
private async buildProject() {
3535
await this.runOperation('Build Project', async lakeRunner => {
36-
const fetchResult: 'Success' | 'CacheNotAvailable' | 'Cancelled' = await this.tryFetchingCache(lakeRunner)
37-
if (fetchResult === 'Cancelled') {
36+
const fetchResult: 'Success' | 'Failure' = await lakeRunner.tryFetchMathlibCacheWithError()
37+
if (fetchResult !== 'Success') {
3838
return
3939
}
4040

@@ -73,11 +73,11 @@ export class ProjectOperationProvider implements Disposable {
7373
return
7474
}
7575

76-
const checkResult: 'Yes' | 'No' | 'Cancelled' = await lakeRunner.isMathlibCacheGetAvailable()
76+
const checkResult: 'Available' | 'Unavailable' | 'Cancelled' = await lakeRunner.isMathlibCacheGetAvailable()
7777
if (checkResult === 'Cancelled') {
7878
return
7979
}
80-
if (checkResult === 'No') {
80+
if (checkResult === 'Unavailable') {
8181
displayNotification('Information', 'Project cleaned successfully.')
8282
return
8383
}
@@ -94,12 +94,8 @@ export class ProjectOperationProvider implements Disposable {
9494
return
9595
}
9696

97-
const fetchResult: ExecutionResult = await lakeRunner.fetchMathlibCache()
98-
if (fetchResult.exitCode === ExecutionExitCode.Cancelled) {
99-
return
100-
}
101-
if (fetchResult.exitCode !== ExecutionExitCode.Success) {
102-
void displayResultError(fetchResult, 'Cannot fetch Mathlib build artifact cache.')
97+
const fetchResult: 'Success' | 'Failure' = await lakeRunner.tryFetchMathlibCacheWithError()
98+
if (fetchResult !== 'Success') {
10399
return
104100
}
105101
displayNotification('Information', 'Mathlib build artifact cache fetched successfully.')
@@ -108,16 +104,19 @@ export class ProjectOperationProvider implements Disposable {
108104

109105
private async fetchMathlibCache() {
110106
await this.runOperation('Fetch Mathlib Build Cache', async lakeRunner => {
111-
const result: ExecutionResult = await lakeRunner.fetchMathlibCache()
112-
if (result.exitCode === ExecutionExitCode.Cancelled) {
107+
const fetchResult: FetchMathlibCacheResult = await lakeRunner.fetchMathlibCache()
108+
if (fetchResult.kind === 'Cancelled') {
113109
return
114110
}
115-
if (result.exitCode !== ExecutionExitCode.Success) {
116-
if (result.stderr.includes(cacheNotFoundError)) {
117-
displayNotification('Error', 'This command cannot be used in non-Mathlib projects.')
118-
return
119-
}
120-
displayResultError(result, 'Cannot fetch Mathlib build artifact cache.')
111+
if (fetchResult.kind === 'CacheUnavailable') {
112+
displayNotification('Error', 'This command cannot be used in non-Mathlib projects.')
113+
return
114+
}
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.')
121120
return
122121
}
123122

@@ -175,12 +174,22 @@ export class ProjectOperationProvider implements Disposable {
175174
return
176175
}
177176

178-
const result: ExecutionResult = await lakeRunner.fetchMathlibCacheForFile(relativeDocUri)
179-
if (result.exitCode === ExecutionExitCode.Cancelled) {
177+
const fetchResult: FetchMathlibCacheResult = await lakeRunner.fetchMathlibCacheForFile(relativeDocUri)
178+
if (fetchResult.kind === 'Cancelled') {
180179
return
181180
}
182-
if (result.exitCode !== ExecutionExitCode.Success) {
183-
displayResultError(result, `Cannot fetch Mathlib build artifact cache for '${relativeDocUri.fsPath}'.`)
181+
if (fetchResult.kind === 'CacheUnavailable') {
182+
displayNotification('Error', 'This command cannot be used in non-Mathlib projects.')
183+
return
184+
}
185+
if (fetchResult.result.exitCode === ExecutionExitCode.Cancelled) {
186+
return
187+
}
188+
if (fetchResult.result.exitCode !== ExecutionExitCode.Success) {
189+
displayResultError(
190+
fetchResult.result,
191+
`Cannot fetch Mathlib build artifact cache for '${relativeDocUri.fsPath}'.`,
192+
)
184193
return
185194
}
186195

@@ -260,7 +269,10 @@ export class ProjectOperationProvider implements Disposable {
260269
return
261270
}
262271

263-
await this.tryFetchingCache(lakeRunner)
272+
const fetchResult: 'Success' | 'Failure' = await lakeRunner.tryFetchMathlibCacheWithError()
273+
if (fetchResult !== 'Success') {
274+
return
275+
}
264276

265277
const localToolchainPath: string = join(activeFolderUri.fsPath, 'lean-toolchain')
266278
const dependencyToolchainPath: string = join(
@@ -378,18 +390,6 @@ export class ProjectOperationProvider implements Disposable {
378390
return [localToolchain, dependencyToolchain]
379391
}
380392

381-
private async tryFetchingCache(lakeRunner: LakeRunner): Promise<'Success' | 'CacheNotAvailable' | 'Cancelled'> {
382-
const fetchResult: ExecutionResult = await lakeRunner.fetchMathlibCache(true)
383-
switch (fetchResult.exitCode) {
384-
case ExecutionExitCode.Success:
385-
return 'Success'
386-
case ExecutionExitCode.Cancelled:
387-
return 'Cancelled'
388-
default:
389-
return 'CacheNotAvailable'
390-
}
391-
}
392-
393393
private async runOperation(context: string, command: (lakeRunner: LakeRunner) => Promise<void>) {
394394
if (this.isRunningOperation) {
395395
displayNotification(

‎vscode-lean4/src/utils/batch.ts‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -273,13 +273,17 @@ export function displayResultError(result: ExecutionResult, message: string) {
273273
if (result.exitCode === ExecutionExitCode.Success) {
274274
throw Error()
275275
}
276-
const errorMessage: string = formatErrorMessage(result, message)
276+
displayOutputError(result.combined, message)
277+
}
278+
279+
export function displayOutputError(output: string, message: string) {
280+
const errorMessage: string = formatErrorMessage(output, message)
277281
displayNotificationWithOutput('Error', errorMessage)
278282
}
279283

280-
function formatErrorMessage(error: ExecutionResult, message: string): string {
281-
if (error.combined === '') {
284+
function formatErrorMessage(output: string, message: string): string {
285+
if (output === '') {
282286
return `${message}`
283287
}
284-
return `${message} Command output: ${error.combined}`
288+
return `${message} Command output: ${output}`
285289
}

‎vscode-lean4/src/utils/lake.ts‎

Lines changed: 68 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,8 @@
11
import { OutputChannel } from 'vscode'
2-
import { ExecutionExitCode, ExecutionResult } from './batch'
2+
import { displayOutputError, ExecutionExitCode, ExecutionResult } from './batch'
33
import { FileUri } from './exturi'
44
import { leanRunner, ToolchainUpdateMode } from './leanCmdRunner'
55

6-
export const cacheNotFoundError = 'unknown executable `cache`'
7-
export const cacheNotFoundExitError = '=> Operation failed. Exit Code: 1.'
8-
96
export type LakeRunnerOptions = {
107
channel: OutputChannel
118
cwdUri: FileUri | undefined
@@ -14,6 +11,13 @@ export type LakeRunnerOptions = {
1411
toolchainUpdateMode: ToolchainUpdateMode
1512
}
1613

14+
export type TryFetchMathlibCacheResult = { kind: 'Success' } | { kind: 'Error'; output: string } | { kind: 'Cancelled' }
15+
16+
export type FetchMathlibCacheResult =
17+
// Invariant: `result.exitCode !== ExecutionExitCode.Cancelled`
18+
// since this exit code always gets mapped to `{ kind: 'Cancelled' }`.
19+
{ kind: 'CacheAvailable'; result: ExecutionResult } | { kind: 'CacheUnavailable' } | { kind: 'Cancelled' }
20+
1721
export class LakeRunner {
1822
constructor(readonly options: LakeRunnerOptions) {}
1923

@@ -38,34 +42,80 @@ export class LakeRunner {
3842
return this.runLakeCommandWithProgress('clean', [], 'Cleaning Lean project')
3943
}
4044

41-
async fetchMathlibCache(filterError: boolean = false): Promise<ExecutionResult> {
42-
const prompt = 'Checking Mathlib build artifact cache'
43-
return this.runLakeCommandWithProgress('exe', ['cache', 'get'], prompt, line => {
44-
if (filterError && line.includes(cacheNotFoundError)) {
45-
return undefined
46-
}
47-
return line
48-
})
45+
private async runFetchMathlibCacheCommand(args: string[], prompt: string): Promise<FetchMathlibCacheResult> {
46+
const availability = await this.isMathlibCacheGetAvailable()
47+
if (availability === 'Cancelled') {
48+
return { kind: 'Cancelled' }
49+
}
50+
if (availability === 'Unavailable') {
51+
return { kind: 'CacheUnavailable' }
52+
}
53+
const result = await this.runLakeCommandWithProgress('exe', ['cache', 'get'].concat(args), prompt)
54+
if (result.exitCode === ExecutionExitCode.Cancelled) {
55+
return { kind: 'Cancelled' }
56+
}
57+
return { kind: 'CacheAvailable', result }
4958
}
5059

51-
async fetchMathlibCacheForFile(projectRelativeFileUri: FileUri): Promise<ExecutionResult> {
52-
const prompt = `Fetching Mathlib build artifact cache for ${projectRelativeFileUri.baseName()}`
53-
return this.runLakeCommandWithProgress('exe', ['cache', 'get', projectRelativeFileUri.fsPath], prompt)
60+
private async tryRunFetchMathlibCacheCommand(args: string[], prompt: string): Promise<TryFetchMathlibCacheResult> {
61+
const fetchResult = await this.runFetchMathlibCacheCommand(args, prompt)
62+
if (fetchResult.kind === 'Cancelled') {
63+
return { kind: 'Cancelled' }
64+
}
65+
if (fetchResult.kind === 'CacheUnavailable') {
66+
return { kind: 'Success' }
67+
}
68+
if (fetchResult.result.exitCode === ExecutionExitCode.Cancelled) {
69+
return { kind: 'Cancelled' }
70+
}
71+
if (fetchResult.result.exitCode !== ExecutionExitCode.Success) {
72+
return { kind: 'Error', output: fetchResult.result.combined }
73+
}
74+
return { kind: 'Success' }
75+
}
76+
77+
async fetchMathlibCache(): Promise<FetchMathlibCacheResult> {
78+
return this.runFetchMathlibCacheCommand([], 'Fetching Mathlib build artifact cache')
79+
}
80+
81+
async tryFetchMathlibCache(): Promise<TryFetchMathlibCacheResult> {
82+
return this.tryRunFetchMathlibCacheCommand([], 'Fetching Mathlib build artifact cache')
83+
}
84+
85+
async tryFetchMathlibCacheWithError(): Promise<'Success' | 'Failure'> {
86+
const fetchResult = await this.tryFetchMathlibCache()
87+
if (fetchResult.kind === 'Cancelled') {
88+
return 'Failure'
89+
}
90+
if (fetchResult.kind !== 'Success') {
91+
displayOutputError(fetchResult.output, 'Cannot fetch Mathlib build artifact cache.')
92+
return 'Failure'
93+
}
94+
return 'Success'
95+
}
96+
97+
async fetchMathlibCacheForFile(projectRelativeFileUri: FileUri): Promise<FetchMathlibCacheResult> {
98+
return this.runFetchMathlibCacheCommand(
99+
[projectRelativeFileUri.fsPath],
100+
`Fetching Mathlib build artifact cache for ${projectRelativeFileUri.baseName()}`,
101+
)
54102
}
55103

56-
async isMathlibCacheGetAvailable(): Promise<'Yes' | 'No' | 'Cancelled'> {
104+
async isMathlibCacheGetAvailable(): Promise<'Available' | 'Unavailable' | 'Cancelled'> {
57105
const result: ExecutionResult = await this.runLakeCommandWithProgress(
58106
'exe',
59107
['cache'],
60108
'Checking whether this is a Mathlib project',
109+
// Filter the `lake exe cache` help string.
110+
_line => undefined,
61111
)
62112
if (result.exitCode === ExecutionExitCode.Cancelled) {
63113
return 'Cancelled'
64114
}
65115
if (result.exitCode === ExecutionExitCode.Success) {
66-
return 'Yes'
116+
return 'Available'
67117
}
68-
return 'No'
118+
return 'Unavailable'
69119
}
70120

71121
private async runLakeCommandWithProgress(

0 commit comments

Comments
 (0)
⚡