Zulip Chat Archive

Hello! I was able to install elan and lean using VSCode on one of my devices a few months ago, but now I need to install them on a Windows device. There are reasons for me not to use VSCode, thus I opted for a manual installation as in https://leanprover-community.github.io/install/windows.html. On powershell -ExecutionPolicy Bypass -f elan-init.ps1 there are several errors like 'Missing file specification after redirection operator' and 'Unexpected token '}' in the expression or statement'. Is my device at fault?

Julian Berman (Mar 26 2025 at 15:04):

Anything is possible, but I would recommend trying the git bash route which is likely better trodden, and seeing if that works.

V S (Mar 26 2025 at 15:08):

Julian Berman said:

Anything is possible, but I would recommend trying the git bash route which is likely better trodden, and seeing if that works.

This leads to several errors:

sh: line 1: syntax error near unexpected token `newline'
sh: line 1: `<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'

(there are no < or > in the command though and | is used in the manual) Thank you still!

Ruben Van de Velde (Mar 26 2025 at 15:29):

Uh, that's html, not a shell script. You're getting the wrong data somewhere

V S (Mar 26 2025 at 15:31):

Ruben Van de Velde said:

Uh, that's html, not a shell script. You're getting the wrong data somewhere

I'm using curl https://elan.lean-lang.org/elan-init.sh -sSf --ssl-no-revoke| sh since it will not work unless I add the ssl part.

V S (Mar 26 2025 at 15:33):

Not sure if the ssl part is at fault, but it seems unlikely that this would swap html and shell script

Mauricio Collares (Mar 26 2025 at 16:04):

When you ignore SSL certificates, captive portals or antiviruses can inject their own pages in place of what you're requesting. What is the output of the curl command if you remove the pipe to sh?

Last updated: May 02 2025 at 03:31 UTC

leanprover-community / mathlib