Arthur Ryman

Stream: new members

[Arthur Ryman]

Hi. I have a backbround in math, software engineering, and formal specification (Z). I just tried to install Lean and math lib on MacOS the fast way as described on https://leanprover-community.github.io/install/macos.html. The install script reported an error, but I was able to run Visual Studio Code. Where should install issues be reported? Zulip or GitHub? Thanks.

[Johan Commelin]

Welcome! Please paste the error here.

[Arthur Ryman]

Installing extensions...
Installing extension 'jroesch.lean'...
(node:60348) [DEP0005] DeprecationWarning: Buffer() is deprecated due to security and usability issues. Please use the Buffer.alloc(), Buffer.allocUnsafe(), or Buffer.from() methods instead.
(Use Electron --trace-deprecation ... to show where the warning was created)
Extension 'jroesch.lean' v0.16.39 was successfully installed.
(node:60348) UnhandledPromiseRejectionWarning: Canceled: Canceled
at D (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:5:1157)
at O.cancel (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:9:62880)
at O.dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:9:63012)
at N.dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:9:63274)
at d (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:3655)
at N.clear (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:4133)
at N.dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:4112)
at dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:4672)
at dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cliProcessMain.js:11:7330)
at d (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:3655)
at /Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:3843
at /Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:3942
at Object.dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:762)
at d (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:3788)
at /Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cliProcessMain.js:14:41520
at Map.forEach (<anonymous>)
at Ne.dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cliProcessMain.js:14:41496)
at d (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:3655)
at N.clear (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:4133)
at N.dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:4112)
at S.dispose (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:6:4672)
at Object.M [as main] (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cliProcessMain.js:17:38649)
at runMicrotasks (<anonymous>)
at processTicksAndRejections (internal/process/task_queues.js:93:5)
at async N (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/code/node/cli.js:12:13842)
(node:60348) UnhandledPromiseRejectionWarning: Unhandled promise rejection. This error originated either by throwing inside of an async function without a catch block, or by rejecting a promise which was not handled with .catch(). To terminate the node process on unhandled promise rejection, use the CLI flag --unhandled-rejections=strict (see https://nodejs.org/api/cli.html#cli_unhandled_rejections_mode). (rejection id: 1)
(node:60348) [DEP0018] DeprecationWarning: Unhandled promise rejections are deprecated. In the future, promise rejections that are not handled will terminate the Node.js process with a non-zero exit code.

[Arthur Ryman]

@Johan Commelin Thanks!

[Arthur Ryman]

Here's my brew config:
HOMEBREW_VERSION: 3.2.6
ORIGIN: https://github.com/Homebrew/brew
HEAD: 265c8c36a4c0a74f478cba16417940b3b588736c
Last commit: 5 days ago
Core tap ORIGIN: https://github.com/Homebrew/homebrew-core
Core tap HEAD: 0d73d02e52030eb27231ce36ef0fc461f9fa62e8
Core tap last commit: 53 minutes ago
Core tap branch: master
HOMEBREW_PREFIX: /usr/local
HOMEBREW_CASK_OPTS: []
HOMEBREW_DISPLAY: /private/tmp/com.apple.launchd.B1u1E7nlur/org.macosforge.xquartz:0
HOMEBREW_MAKE_JOBS: 8
Homebrew Ruby: 2.6.3 => /usr/local/Homebrew/Library/Homebrew/vendor/portable-ruby/2.6.3_2/bin/ruby
CPU: octa-core 64-bit haswell
Clang: 12.0.0 build 1200
Git: 2.24.3 => /Applications/Xcode.app/Contents/Developer/usr/bin/git
Curl: 7.64.1 => /usr/bin/curl
macOS: 10.15.7-x86_64
CLT: 12.4.0.0.1.1610135815
Xcode: 12.4
XQuartz: 2.7.11 => /opt/X11

[Johan Commelin]

Hmm, at first sight this looks like some error in VScode while it was installing the Lean extension.

[Johan Commelin]

Does Lean work? Did you test it yet?

[Arthur Ryman]

I tested it. Created test.lean and ran #eval 2+2 successfully. So it looks like the Lean extension is installed OK and working.

[Arthur Ryman]

I'll continue testing it. Is this issue worth reporting on GitHub?

[Johan Commelin]

Ok. I'm not an installation expert. But I think this is a VScode issue. I don't think it comes from our install script.

[Johan Commelin]

Have you used VScode before? Do similar errors occur if you install other plugins?

[Arthur Ryman]

Yes, looks like maybe the lean extension was built with a downlevel version of node and the current version of VSCode is bundling a later version with stricter behaviour.

[Johan Commelin]

Aha. @Gabriel Ebner could that be the case?

[Arthur Ryman]

No, I'm not a VSCode user - I use IntelliJ professionally. So I'll stumble around VScode for a while. If I see unexpected behaviour I'll report it here.

[Johan Commelin]

Ok, thanks! And good luck and lots of fun with using lean (-;

[Gabriel Ebner]

That seems like a harmless deprecation warning. It doesn't break the extension for you, right? Please feel free to submit a bug at https://github.com/leanprover/vscode-lean

[Arthur Ryman]

@Johan Commelin Thanks. I appreciate your help.

[Arthur Ryman]

@Gabriel Ebner Agreed. I assume that when the extension was built the developer would have resolved any warnings. So it looks like a version mismatch. So far it's harmless as far as I can tell, but I'm just getting started. I will file a bug report.

[Arthur Ryman]

@Gabriel Ebner Here's the github issue: https://github.com/leanprover/vscode-lean/issues/279