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

Re-enables auto-downloading of Lean via elan, and add Select Interpreter #35

Merged
merged 49 commits into from
Oct 26, 2021
Merged
Show file tree
Hide file tree
Changes from 27 commits
Commits
Show all changes
49 commits
Select commit Hold shift + click to select a range
8fc56e2
Write abbreviation rewriter errors to a new "Lean: Client" OutputChan…
lovettchris Sep 8, 2021
7c0d7fe
fix eslint error.
lovettchris Sep 8, 2021
abacb47
feat: add 'Lean 4: Select Interpreter' so user can enter a path that …
lovettchris Sep 24, 2021
ccd86dd
fix: npm lint error.
lovettchris Sep 24, 2021
ef5947f
merge master
lovettchris Oct 6, 2021
3cfecf9
Re-enable auto-install via elan.
lovettchris Oct 7, 2021
353bb86
fix versions
lovettchris Oct 7, 2021
db9620b
revert last change
lovettchris Oct 7, 2021
9330db5
fix: linux bootstrap
lovettchris Oct 7, 2021
bf5cad2
fix: windows elan install to specify powershell terminal in case user…
lovettchris Oct 7, 2021
5afe6ba
Add @testing-library/dom as an explicit dependency.
gebner Oct 7, 2021
c677314
fix: Error [ERR_STREAM_WRITE_AFTER_END]: write after end by moving to…
lovettchris Oct 7, 2021
9f91404
Merge branch 'clovett/logging_errors' of github.com:lovettchris/vscod…
lovettchris Oct 7, 2021
e0c0b69
Merge branch 'master' into clovett/logging_errors
lovettchris Oct 7, 2021
f724b32
chore : move lean installer code to separate class.
lovettchris Oct 8, 2021
685be11
fix: Argument 'path' should be typed
lovettchris Oct 8, 2021
188239d
fix: We do want to version control .vscode/,
lovettchris Oct 8, 2021
d2bfaf8
fix: remove lerna dependency
lovettchris Oct 8, 2021
bd025c3
fix: lean3 compatibility (extension should not activate on lean3 proj…
lovettchris Oct 8, 2021
74046fc
doc: make comment more clear.
lovettchris Oct 8, 2021
d9ee835
Fix URL to elan-init.ps1
lovettchris Oct 11, 2021
856c98a
re-enable capturing of output from lean --version in extension.ts bec…
lovettchris Oct 11, 2021
10f7aef
fix: improve error message
lovettchris Oct 11, 2021
bfec5bf
fix: logic should not be dependent on literal string 'program not found'
lovettchris Oct 12, 2021
30a68c6
Update vscode-lean4/src/utils/leanInstaller.ts
lovettchris Oct 12, 2021
fce1b7d
fix: addDefaultElanPath so PATH environment is not needed.
lovettchris Oct 13, 2021
e9bda71
Merge branch 'clovett/logging_errors' of github.com:lovettchris/vscod…
lovettchris Oct 13, 2021
d1e5c61
fix: Hide the LanguageClient object inside LeanClient to reduce bleed…
lovettchris Oct 13, 2021
c44fad5
fix: stop auto-editing .toml file and use Macs awesome idea using lea…
lovettchris Oct 14, 2021
518ab66
fix: build error.
lovettchris Oct 14, 2021
a1b432a
Merge branch 'master' into clovett/logging_errors
lovettchris Oct 18, 2021
7099a07
add debugging options
lovettchris Oct 18, 2021
ad702c0
fix: revert console.log debugging.
lovettchris Oct 18, 2021
dc6acba
Merge branch 'master' into clovett/logging_errors
lovettchris Oct 20, 2021
ff63f0c
fix: revert change while debugging
lovettchris Oct 20, 2021
cdf7600
fix: handle undefined InitializeResult when lean server fails to start.
lovettchris Oct 20, 2021
04f3c4c
fix: update to npm version 8.1.0, add some comments
lovettchris Oct 21, 2021
89c3070
add extension kind
lovettchris Oct 21, 2021
c256b57
revert: changes to package-lock files.
lovettchris Oct 21, 2021
d0994b4
fix: revert to "vscode-languageclient": "^7.0.0",
lovettchris Oct 21, 2021
0b806a5
Fix infoview initialization problems.
lovettchris Oct 21, 2021
7a8a77a
fix: compile error.
lovettchris Oct 21, 2021
f716149
remove extensionKind from infoview node module since it is not a vsco…
lovettchris Oct 21, 2021
a075640
also monitor and read "lean-toolchain" files and do not set --default…
lovettchris Oct 22, 2021
fb97974
fix: bootstrap should not install multiple toolchains.
lovettchris Oct 22, 2021
0d5502e
fix: install the toolchain requested in leanpkg or lean-toolchain
lovettchris Oct 22, 2021
db7b704
fix: removed unused member variable.
lovettchris Oct 22, 2021
e1017da
Update lean4-infoview/src/infoview/main.tsx
lovettchris Oct 25, 2021
326f560
CR: simplify code that parses out lean version info
lovettchris Oct 25, 2021
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
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
## Build directories
out/
dist/
.vs/

## Output
node_modules/
Expand Down
9 changes: 6 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,14 @@ The repository contains NPM packages implementing editor integration for the Lea
- Run `npm install` in this folder. This installs the Lerna package manager.
- Run `npx lerna bootstrap`. This sets up the project's dependencies.
- Run `npx lerna run build`. This compiles the extension (which is necessary for go-to-definition in vscode).

### Debugging
- Open VS Code on this folder.
- 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 Extension` from the drop down.
- Run the launch config.
- Press F5 to launch the extension in the vscode debugger, (we've checked in the correct launch.json configuration.)

**Note:** if breakpoints are not working, try changing one line of code in `function activate` in `extension.ts`, even
adding a newline seems to work, then press F5.

## Changelog
### 0.0.29 (Jun 4, 2021)
Expand Down
Loading