feat: add initial commit in new projects (#406)

leanprover · Mar 14, 2024 · d7770bb · d7770bb
1 parent 62ff13b
commit d7770bb
Showing 1 changed file with 36 additions and 1 deletion.
diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts
@@ -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 {
 
@@ -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)
     }
 
@@ -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)
     }
 
@@ -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',