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.

Sign up for GitHub

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

Jump to bottom

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

Merged
merged 49 commits into from
Oct 26, 2021
Merged

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

merged 49 commits into from
Oct 26, 2021

Commits on Sep 8, 2021

  1. Write abbreviation rewriter errors to a new "Lean: Client" OutputChan… 

    …nel so we can better debug the issue of \ sometimes not wroking.
    @lovettchris
    lovettchris committed Sep 8, 2021
    Configuration menu
    Copy the full SHA
    8fc56e2 View commit details
    Browse the repository at this point in the history

  2. fix eslint error.

    @lovettchris
    lovettchris committed Sep 8, 2021
    Configuration menu
    Copy the full SHA
    7c0d7fe View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2021

  1. feat: add 'Lean 4: Select Interpreter' so user can enter a path that … 

    …is workspace specific.

fix: auto open of infoview should only happen once per vscode session.
fix: auto open of infoview should not happen on markdown files.
    @lovettchris
    lovettchris committed Sep 24, 2021
    Configuration menu
    Copy the full SHA
    abacb47 View commit details
    Browse the repository at this point in the history

  2. fix: npm lint error.

    @lovettchris
    lovettchris committed Sep 24, 2021
    Configuration menu
    Copy the full SHA
    ccd86dd View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2021

  1. merge master

    @lovettchris
    lovettchris committed Oct 6, 2021
    Configuration menu
    Copy the full SHA
    ef5947f View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2021

  1. Re-enable auto-install via elan.

    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    3cfecf9 View commit details
    Browse the repository at this point in the history

  2. fix versions

    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    353bb86 View commit details
    Browse the repository at this point in the history

  3. revert last change

    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    db9620b View commit details
    Browse the repository at this point in the history

  4. fix: linux bootstrap

    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    9330db5 View commit details
    Browse the repository at this point in the history

  5. fix: windows elan install to specify powershell terminal in case user… 

    … has set a different default.
    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    bf5cad2 View commit details
    Browse the repository at this point in the history

  6. Add @testing-library/dom as an explicit dependency.

    @gebner
    gebner committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    5afe6ba View commit details
    Browse the repository at this point in the history

  7. fix: Error [ERR_STREAM_WRITE_AFTER_END]: write after end by moving to… 

    … vscode-languageclient version 8.0.0 as per recommendation from microsoft/vscode-languageserver-node#825 this also means we've moved to vscode-languageserver-protocol 3.17.  Everything seems to work, but probably needs more testing...
    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    c677314 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'clovett/logging_errors' of github.com:lovettchris/vscod… 

    …e-lean4 into clovett/logging_errors
    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    9f91404 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' into clovett/logging_errors

    @lovettchris
    lovettchris committed Oct 7, 2021
    Configuration menu
    Copy the full SHA
    e0c0b69 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2021

  1. chore : move lean installer code to separate class.

    @lovettchris
    lovettchris committed Oct 8, 2021
    Configuration menu
    Copy the full SHA
    f724b32 View commit details
    Browse the repository at this point in the history

  2. fix: Argument 'path' should be typed

    @lovettchris
    lovettchris committed Oct 8, 2021
    Configuration menu
    Copy the full SHA
    685be11 View commit details
    Browse the repository at this point in the history

  3. fix: We do want to version control .vscode/,

    @lovettchris
    lovettchris committed Oct 8, 2021
    Configuration menu
    Copy the full SHA
    188239d View commit details
    Browse the repository at this point in the history

  4. fix: remove lerna dependency

    @lovettchris
    lovettchris committed Oct 8, 2021
    Configuration menu
    Copy the full SHA
    d2bfaf8 View commit details
    Browse the repository at this point in the history

  5. fix: lean3 compatibility (extension should not activate on lean3 proj… 

    …ects).
    @lovettchris
    lovettchris committed Oct 8, 2021
    Configuration menu
    Copy the full SHA
    bd025c3 View commit details
    Browse the repository at this point in the history

  6. doc: make comment more clear.

    @lovettchris
    lovettchris committed Oct 8, 2021
    Configuration menu
    Copy the full SHA
    74046fc View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2021

  1. Fix URL to elan-init.ps1

    @lovettchris
    lovettchris committed Oct 11, 2021
    Configuration menu
    Copy the full SHA
    d9ee835 View commit details
    Browse the repository at this point in the history

  2. re-enable capturing of output from lean --version in extension.ts bec… 

    …ause that may result in a long running "downloading lean" session so this output helps explain to the user why the big delay.
    @lovettchris
    lovettchris committed Oct 11, 2021
    Configuration menu
    Copy the full SHA
    856c98a View commit details
    Browse the repository at this point in the history

  3. fix: improve error message

    @lovettchris
    lovettchris committed Oct 11, 2021
    Configuration menu
    Copy the full SHA
    10f7aef View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2021

  1. fix: logic should not be dependent on literal string 'program not found' 

    fix: read lean version from the leanpkg.toml file so that installation from elan is set to install the right version from the get go (this avoids duplicate installation of 2 versions during bootstraping).
fix: bring in the LeanPkg service from the old code, updated to new vscode api's with some functionality disabled for now.
    @lovettchris
    lovettchris committed Oct 12, 2021
    Configuration menu
    Copy the full SHA
    bfec5bf View commit details
    Browse the repository at this point in the history

  2. Update vscode-lean4/src/utils/leanInstaller.ts 

    Co-authored-by: Wojciech Nawrocki <[email protected]>
    @lovettchris @Vtec234
    lovettchris and Vtec234 authored Oct 12, 2021
    Configuration menu
    Copy the full SHA
    30a68c6 View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2021

  1. fix: addDefaultElanPath so PATH environment is not needed. 

    fix: move selectToolchain UI out of LeanClient and into LeanInstaller.
fix: add Select Toolchain command that lets user pick from elan toolchain list
fix: when user switches toolchain automatically update the leanpkg.toml file.
    @lovettchris
    lovettchris committed Oct 13, 2021
    Configuration menu
    Copy the full SHA
    fce1b7d View commit details
    Browse the repository at this point in the history

  2. Merge branch 'clovett/logging_errors' of github.com:lovettchris/vscod… 

    …e-lean4 into clovett/logging_errors
    @lovettchris
    lovettchris committed Oct 13, 2021
    Configuration menu
    Copy the full SHA
    e9bda71 View commit details
    Browse the repository at this point in the history

  3. fix: Hide the LanguageClient object inside LeanClient to reduce bleed… 

    … on client.running state.
    @lovettchris
    lovettchris committed Oct 13, 2021
    Configuration menu
    Copy the full SHA
    d1e5c61 View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2021

  1. fix: stop auto-editing .toml file and use Macs awesome idea using lea… 

    …n +version.
    @lovettchris
    lovettchris committed Oct 14, 2021
    Configuration menu
    Copy the full SHA
    c44fad5 View commit details
    Browse the repository at this point in the history

  2. fix: build error.

    @lovettchris
    lovettchris committed Oct 14, 2021
    Configuration menu
    Copy the full SHA
    518ab66 View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2021

  1. Merge branch 'master' into clovett/logging_errors

    @lovettchris
    lovettchris committed Oct 18, 2021
    Configuration menu
    Copy the full SHA
    a1b432a View commit details
    Browse the repository at this point in the history

  2. add debugging options

    @lovettchris
    lovettchris committed Oct 18, 2021
    Configuration menu
    Copy the full SHA
    7099a07 View commit details
    Browse the repository at this point in the history

  3. fix: revert console.log debugging.

    @lovettchris
    lovettchris committed Oct 18, 2021
    Configuration menu
    Copy the full SHA
    ad702c0 View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2021

  1. Merge branch 'master' into clovett/logging_errors

    @lovettchris
    lovettchris committed Oct 20, 2021
    Configuration menu
    Copy the full SHA
    dc6acba View commit details
    Browse the repository at this point in the history

  2. fix: revert change while debugging

    @lovettchris
    lovettchris committed Oct 20, 2021
    Configuration menu
    Copy the full SHA
    ff63f0c View commit details
    Browse the repository at this point in the history

  3. fix: handle undefined InitializeResult when lean server fails to start.

    @lovettchris
    lovettchris committed Oct 20, 2021
    Configuration menu
    Copy the full SHA
    cdf7600 View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2021

  1. fix: update to npm version 8.1.0, add some comments

    @lovettchris
    lovettchris committed Oct 21, 2021
    Configuration menu
    Copy the full SHA
    04f3c4c View commit details
    Browse the repository at this point in the history

  2. add extension kind

    @lovettchris
    lovettchris committed Oct 21, 2021
    Configuration menu
    Copy the full SHA
    89c3070 View commit details
    Browse the repository at this point in the history

  3. revert: changes to package-lock files.

    @lovettchris
    lovettchris committed Oct 21, 2021
    Configuration menu
    Copy the full SHA
    c256b57 View commit details
    Browse the repository at this point in the history

  4. fix: revert to "vscode-languageclient": "^7.0.0",

    @lovettchris
    lovettchris committed Oct 21, 2021
    Configuration menu
    Copy the full SHA
    d0994b4 View commit details
    Browse the repository at this point in the history

  5. Fix infoview initialization problems.

    @lovettchris
    lovettchris committed Oct 21, 2021
    Configuration menu
    Copy the full SHA
    0b806a5 View commit details
    Browse the repository at this point in the history

  6. fix: compile error.

    @lovettchris
    lovettchris committed Oct 21, 2021
    Configuration menu
    Copy the full SHA
    7a8a77a View commit details
    Browse the repository at this point in the history

  7. remove extensionKind from infoview node module since it is not a vsco… 

    …de extension.
    @lovettchris
    lovettchris committed Oct 21, 2021
    Configuration menu
    Copy the full SHA
    f716149 View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2021

  1. also monitor and read "lean-toolchain" files and do not set --default… 

    …-toolchain to something specific.
    @lovettchris
    lovettchris committed Oct 22, 2021
    Configuration menu
    Copy the full SHA
    a075640 View commit details
    Browse the repository at this point in the history

  2. fix: bootstrap should not install multiple toolchains.

    @lovettchris
    lovettchris committed Oct 22, 2021
    Configuration menu
    Copy the full SHA
    fb97974 View commit details
    Browse the repository at this point in the history

  3. fix: install the toolchain requested in leanpkg or lean-toolchain

    @lovettchris
    lovettchris committed Oct 22, 2021
    Configuration menu
    Copy the full SHA
    0d5502e View commit details
    Browse the repository at this point in the history

  4. fix: removed unused member variable.

    @lovettchris
    lovettchris committed Oct 22, 2021
    Configuration menu
    Copy the full SHA
    db7b704 View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2021

  1. Update lean4-infoview/src/infoview/main.tsx 

    Co-authored-by: Gabriel Ebner <[email protected]>
    @lovettchris @gebner
    lovettchris and gebner authored Oct 25, 2021
    Configuration menu
    Copy the full SHA
    e1017da View commit details
    Browse the repository at this point in the history

  2. CR: simplify code that parses out lean version info

    @lovettchris
    lovettchris committed Oct 25, 2021
    Configuration menu
    Copy the full SHA
    326f560 View commit details
    Browse the repository at this point in the history