Merge pull request #30 from Vtec234/lsp-infoview

LSP-based infoview

.github/workflows/on-push.yml

@@ -8,12 +8,15 @@ jobs:
     name: Build
     steps:
       - uses: actions/checkout@v2
+      - uses: actions/setup-node@v2
+        with:
+          node-version: '16'
       - run: npm install
-      - run: npm run compile
-      - run: npm run package
+      - run: npx lerna bootstrap
+      - run: npm run build
+      - run: npx lerna run --scope=lean4 package
       - uses: actions/upload-artifact@v2
         with:
           name: vscode-lean4
-          path: 'lean4-*.vsix'
+          path: 'vscode-lean4/lean4-*.vsix'
       - run: npm run lint
-      - run: npm list --production --parseable --depth=99999 --loglevel=error

.gitignore

@@ -1,5 +1,9 @@
-out
-node_modules
+## Build directories
+out/
+dist/
+
+## Output
+node_modules/
+**/media/webview.*
+*.tsbuildinfo
 *.vsix
-media/index.js*
-infoview/dist

.vscode/launch.json

@@ -7,22 +7,11 @@
             "type": "extensionHost",
             "request": "launch",
             "runtimeExecutable": "${execPath}",
-            "args": ["--extensionDevelopmentPath=${workspaceRoot}" ],
+            "args": ["--extensionDevelopmentPath=${workspaceRoot}/vscode-lean4" ],
             "stopOnEntry": false,
             "sourceMaps": true,
-            "outFiles": [ "${workspaceRoot}/out/src/**/*.js" ],
+            "outFiles": [ "${workspaceRoot}/vscode-lean4/out/**/*.js" ],
             "preLaunchTask": "watch"
-        },
-        {
-            "name": "Launch Tests",
-            "type": "extensionHost",
-            "request": "launch",
-            "runtimeExecutable": "${execPath}",
-            "args": ["--extensionDevelopmentPath=${workspaceRoot}", "--extensionTestsPath=${workspaceRoot}/out/test" ],
-            "stopOnEntry": false,
-            "sourceMaps": true,
-            "outFiles": [ "${workspaceRoot}/out/test/**/*.js" ],
-            "preLaunchTask": "${defaultBuildTask}"
         }
     ]
 }

.vscode/settings.json

@@ -1,11 +1,16 @@
 // Place your settings in this file to overwrite default and user settings.
 {
     "files.exclude": {
-        "out": true, // set this to true to hide the "out" folder with the compiled JS files
-        "node_modules": true // set this to true to hide the "out" folder with the compiled JS files
+        "*/out": true, // set this to true to hide the "out" folder with the compiled JS files
+        "*/dist": true, // set this to true to hide the "dist" folder with the compiled JS files
+        "*/node_modules": true // set this to true to hide the "out" folder with the compiled JS files
     },
     "search.exclude": {
-        "out": true // set this to false to include "out" folder in search results
+        "*/out": true // set this to false to include "out" folder in search results
     },
-    "typescript.tsdk": "./node_modules/typescript/lib" // we want to use the TS server from our node_modules folder to control its version
+    "typescript.tsdk": "./node_modules/typescript/lib", // we want to use the TS server from our node_modules folder to control its version
+    "eslint.workingDirectories": [
+        "./lean4-infoview",
+        "./vscode-lean4",
+    ]
 }

.vscode/tasks.json

@@ -39,9 +39,9 @@
 			"group": "build"
 		},
 		{
-			"label": "compile",
+			"label": "build",
 			"type": "npm",
-			"script": "compile",
+			"script": "build",
 			"problemMatcher": {
 				"owner": "typescript",
 				"source": "ts",

README.md

@@ -33,12 +33,16 @@ As of now, the extension supports the following features:
 - Command to restart the full Lean 4 server, accessible via Ctrl+Shift+P
 - Compatibility with the [Lean 3 VSCode extension](https://github.com/leanprover/vscode-lean)
 
-## Building the client
-- Run `npm install` in this folder. This installs all necessary npm modules.
+## For developers
+The repository contains NPM packages implementing editor integration for the Lean 4 programming language. The VSCode extension proper is in [`vscode-lean4`](vscode-lean4/), while [`lean4-infoview`](lean4-infoview/) implements the information display. We build the packages in tandem using Lerna.
+
+### Building
+- Run `npm install` in this folder. This installs the Lerna package manager.
+- Run `npx lerna bootstrap`. This sets up the project's dependencies.
 - Open VS Code on this folder.
-- Press Ctrl+Shift+B to compile the client.
+- Press Ctrl+Shift+B to compile the extension. This step is needed for a working development setup.
 - Switch to the Debug viewlet (Ctrl+Shift+D).
-- Select `Launch Client` from the drop down.
+- Select `Launch Extension` from the drop down.
 - Run the launch config.
 
 ## Changelog
@@ -90,4 +94,4 @@ As of now, the extension supports the following features:
   - The following commands:
     - `lean4.restartServer`
     - `lean4.input.convert` (Tab)
-    - `lean4.refreshFileDependencies` (Ctrl+Shift+X)
+    - `lean4.refreshFileDependencies` (Ctrl+Shift+X)