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.

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

feat: add initial commit in new projects #406

Merged
merged 1 commit into from
Mar 14, 2024
Merged
Changes from all commits
Commits
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
37 changes: 36 additions & 1 deletion vscode-lean4/src/projectinit.ts
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ import path = require('path');
import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo';
import { elanSelfUpdate } from './utils/elan';
import { lake } from './utils/lake';
import { ExecutionExitCode, ExecutionResult, batchExecuteWithProgress, displayError } from './utils/batch';
import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress, displayError } from './utils/batch';

export class ProjectInitializationProvider implements Disposable {

Expand Down Expand Up @@ -34,6 +34,11 @@ export class ProjectInitializationProvider implements Disposable {
return
}

const initialCommitResult: 'Success' | 'GitAddFailed' | 'GitCommitFailed' = await this.createInitialCommit(projectFolder)
if (initialCommitResult !== 'Success') {
return
}

await ProjectInitializationProvider.openNewFolder(projectFolder)
}

Expand All @@ -53,6 +58,20 @@ export class ProjectInitializationProvider implements Disposable {
return
}

const buildResult: ExecutionResult = await lake(this.channel, projectFolder, mathlibToolchain).build()
if (buildResult.exitCode === ExecutionExitCode.Cancelled) {
return
}
if (buildResult.exitCode !== ExecutionExitCode.Success) {
await displayError(buildResult, 'Cannot build Lean project.')
return
}

const initialCommitResult: 'Success' | 'GitAddFailed' | 'GitCommitFailed' = await this.createInitialCommit(projectFolder)
if (initialCommitResult !== 'Success') {
return
}

await ProjectInitializationProvider.openNewFolder(projectFolder)
}

Expand Down Expand Up @@ -92,6 +111,22 @@ export class ProjectInitializationProvider implements Disposable {
return projectFolder
}

private async createInitialCommit(projectFolder: Uri): Promise<'Success' | 'GitAddFailed' | 'GitCommitFailed'> {
const gitAddResult = await batchExecute('git', ['add', '--all'], projectFolder.fsPath, { combined: this.channel } )
if (gitAddResult.exitCode !== ExecutionExitCode.Success) {
await displayError(gitAddResult, 'Cannot add files to staging area of Git repository for project.')
return 'GitAddFailed'
}

const gitCommitResult = await batchExecute('git', ['commit', '--author', 'Lean 4 VS Code Extension <>', '-m', 'Initial commit'], projectFolder.fsPath, { combined: this.channel } )
if (gitCommitResult.exitCode !== ExecutionExitCode.Success) {
await displayError(gitAddResult, 'Cannot commit files to Git repository for project.')
return 'GitCommitFailed'
}

return 'Success'
}

private async openProject() {
const projectFolders: Uri[] | undefined = await window.showOpenDialog({
title: 'Open Lean 4 project folder containing a \'lean-toolchain\' file',
Expand Down
Loading