WSL ubuntu error

Stream: new members

[Jason KY.]

Hi!
I'm trying to install mathlib on Ubuntu running in a WSL (in order to use format lean) but this happens,

curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash
Installing python dependencies (at user level)
/home/jasonky/.virtualenvs/format_lean/bin/pip3
ERROR: Can not perform a '--user' install. User site-packages are not visible in this virtualenv.

Thanks in advance for any help!

[Andrew Ashworth]

This is a bit non-standard. You will need to install mathlib the standard way via leanpkg, and then compile it. The problem is with your use of a virtual environment, and a conflict with pip.

[Jason KY.]

I see... Sadly format lean requires the virtual environment to work :( But I guess I can always compile the LEAN code individually and then compile (and it works!)

[Andrew Ashworth]

I don't think it would be a big deal if you have some shell scripting experience to fix remote-install-update-mathlib? I can't help you there, though, since I personally do not use the community mathlib update scripts.

[Jason KY.]

Ahh.. I'll see if I can make something happen! Thanks for the help!

[Patrick Massot]

@Jason KY. Why do you say format_lean needs a virtual env? The documentation may recommend it, but there is nothing preventing you to install it in your global user space or even system-wide.

[Patrick Massot]

It's tricky to support all kinds of setup. We really need to write more levels of instructions. We need both simpler instructions for people who want Lean+precompiled mathlib without all the tooling and more detailed instructions. However the ultimate documentation for those mathlib tools are the bash scripts and python source code. That remote-install-update-mathlib actually does very little, especially if you want only update-mathlib, which is by far the most useful tool here. In the end, you want to be able to run the python program https://github.com/leanprover-community/mathlib-tools/blob/master/scripts/update-mathlib.py. So it needs to be found by your system, and its python dependencies need to be found. Every trick to make that happen in any given setup is allowed.

The external dependencies are listed here as they appear on PyPi and can be fetched by the python package installer pip. I think the only internal dependency is https://github.com/leanprover-community/mathlib-tools/blob/master/scripts/auth_github.py.

[Jason KY.]

I see! I assumed that format_lean needed the virtual environment since that's what it said on the installation guide. I'll try reinstalling it globally and perhaps that will work better!

[Kevin Buzzard]

You're using a virtual Ubuntu on a windows machine, right? Is there anything stopping you just installing it on Windows?

[Jason KY.]

I don't know how to install it on windows since there's no documentation about it (and I'm not techy enough to know how to) :/

[Kevin Buzzard]

Why not just install python 3.7 on Windows following some google instructions and then download a command line terminal and type in the commands in the installation instructions? I don't know much about Windows but I don't really see why this wouldn't work. Just make sure the python exe is in the path for the terminal.

[Jason KY.]

I tried this and it almost worked! But it broke once I tried to compile the lean files saying TypeError: argument of type 'WindowsPath' is not iterable. I don't believe this to be a Python path issue, should it? My Python works fine in the terminal otherwise.

[Bryan Gin-ge Chen]

Did the error give you a file and line number? You may be able to fix that by changing that line in the Python so that it uses the .name field of converts the WindowsPath object to a string.

[Jason KY.]

Traceback (most recent call last):
  File "C:/Users/Jason/AppData/Local/Programs/Python/Python37-32/Scripts/format_project", line 156, in <module>
    Fire(render_lean_project)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\fire\core.py", line 138, in Fire
    component_trace = _Fire(component, args, parsed_flag_args, context, name)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\fire\core.py", line 471, in _Fire
    target=component.__name__)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\fire\core.py", line 675, in _CallAndUpdateTrace
    component = fn(*varargs, **kwargs)
  File "C:/Users/Jason/AppData/Local/Programs/Python/Python37-32/Scripts/format_project", line 119, in render_lean_project
    TradBegin, TradEnd])
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\format_lean\line_reader.py", line 24, in __init__
    self.server = Server(lean_exec_path, lean_path)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\format_lean\server.py", line 15, in __init__
    env={'LEAN_PATH': lean_path})
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\subprocess.py", line 775, in __init__
    restore_signals, start_new_session)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\subprocess.py", line 1119, in _execute_child
    args = list2cmdline(args)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\subprocess.py", line 530, in list2cmdline
    needquote = (" " in arg) or ("\t" in arg) or not arg
TypeError: argument of type 'WindowsPath' is not iterable

This is the entire message. I'm not sure if I should mess around with these codes if I don't know what I'm doing :P

[Bryan Gin-ge Chen]

Could you try running format_project --debug? I'm curious what kind of object lean_exec_path is. I suspect that lean_exec_path needs to be converted to a string somewhere along the way.

[Jason KY.]

This is what format_project --debug gives me:

$ format_project --debug
Lean executable path: C:\Users\Jason\.elan\toolchains\3.4.2\bin\lean
LEAN_PATH: C:\Users\Jason\.elan\toolchains\3.4.2\bin\..\lib\lean\library:C:\Users\Jason\AppData\Local\Packages\CanonicalGroupLimited.Ubuntu16.04onWindows_79rhkp1fndgsc\LocalState\rootfs\home\jasonky\M4000x_LEAN_formalisation\src:_target\deps\mathlib\src
Template folder: C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\format_lean\templates
Tactic state filters:  []
Traceback (most recent call last):
  File "C:/Users/Jason/AppData/Local/Programs/Python/Python37-32/Scripts/format_project", line 156, in <module>
    Fire(render_lean_project)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\fire\core.py", line 138, in Fire
    component_trace = _Fire(component, args, parsed_flag_args, context, name)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\fire\core.py", line 471, in _Fire
    target=component.__name__)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\fire\core.py", line 675, in _CallAndUpdateTrace
    component = fn(*varargs, **kwargs)
  File "C:/Users/Jason/AppData/Local/Programs/Python/Python37-32/Scripts/format_project", line 119, in render_lean_project
    TradBegin, TradEnd])
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\format_lean\line_reader.py", line 24, in __init__
    self.server = Server(lean_exec_path, lean_path)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\format_lean\server.py", line 15, in __init__
    env={'LEAN_PATH': lean_path})
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\subprocess.py", line 775, in __init__
    restore_signals, start_new_session)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\subprocess.py", line 1119, in _execute_child
    args = list2cmdline(args)
  File "C:\users\jason\appdata\local\programs\python\python37-32\lib\subprocess.py", line 530, in list2cmdline
    needquote = (" " in arg) or ("\t" in arg) or not arg
TypeError: argument of type 'WindowsPath' is not iterable

[Bryan Gin-ge Chen]

Ah, OK, I guess this doesn't help much since print coerces objects to a string. The following might work (I can't test easily at the moment). Change this line to this:

    lecture_reader = FileReader(str(lean_exec_path), lean_path,

and then reinstall format_lean.

[Jason KY.]

Emm... Now it gives no error but it's not compiling either :(

[Bryan Gin-ge Chen]

What happens, exactly? Does the command successfully run with no output but nothing is added in the "outdir" that you specified? What does the file that you used for "inpath" look like?

[Jason KY.]

I have only = ['src/M40001/M40001.lean']within my format.tomlso I would expect it to compile the file indicated into the folder html. But when I run the command it creates some other files named lecture in html. The terminal itself does not return anything.

[Jason KY.]

My inpath file should be fine I think. I have compiled it once before in my WSL and it worked like a charm!

[Bryan Gin-ge Chen]

A file called lecture.css (and lecture.css.map) is fine. That's a style file used in the generated HTML. If you see other lecture files I'm not sure where they're coming from.

Does it work if you change format.toml to only = ['M40001/M40001.lean']? Make sure that format.lean is in the directory that contains src/ too. It looks like the paths in only need to be relative to the src/ subdirectory.

Sorry, I don't have direct experience with format_lean so I'm guessing based on browsing the source at this point.

[Jason KY.]

I can't seem to find the format.lean file. Where can I get it?

[Patrick Massot]

He meant format_lean, not format.lean I guess

[Patrick Massot]

Could you post an archive of the project you are trying to format?

[Jason KY.]

https://github.com/JasonKYi/M4000x_LEAN_formalisation.git
The files I want to compile are in src/M40001

[Patrick Massot]

It works with no problem here.

[Patrick Massot]

although the last entry in your format.toml is strange.

[Patrick Massot]

Reading back Bryan's message, he meant format.toml, not format.lean.

[Jason KY.]

Oh yeah, I see the typo. Unfortunately, it still doesn't compile with the typo fixed :(

Reading back Bryan's message, he meant format.toml, not format.lean.

That makes a lot more sense! Had me worried there for a bit cause I couldn't find format_lean either

[Patrick Massot]

Let me try to describe what I did

[Patrick Massot]

I checked out your repository, went there, ran leanpkg configure, then update-mathlib then format_project and it created html files. I did nothing else.

[Patrick Massot]

Could you describe again the situation on your side?

[Jason KY.]

Let me try to copy your steps

[Jason KY.]

I've done what the first two steps but when I enter format_project it simply creates 5 files in the indicated directory without compiling any of the indicated files.

[Patrick Massot]

Which 5 files?

[Jason KY.]

colourful jquery.min lean lecture lecture.css.map

[Patrick Massot]

Where do you see those files? Are you using a graphical file explorer hiding file extensions?

[Patrick Massot]

Or are you using a civilized shell?

[Patrick Massot]

You should see a M40001 folder inside your html folder.

[Jason KY.]

ah sorry, my windows automatically hid the file extensions. With the extensions they are colourful.css jquery.min.js lean.js lecture.css lecture.css.map

[Jason KY.]

There is no M40001 folder in the html folder

[Patrick Massot]

It would still help to fix the little issues from your repository. Remove the last entry in your only list, and correct the code in src/M40001/M40001.lean: you cannot end a proof with a comment. Each comment get attached to the following sequence of tactic lines.

[Patrick Massot]

I'm worried about those file extension because it looks like you use graphical stuff instead of a command line where you can actually see things happening.

[Patrick Massot]

What command line do you use to run format_project?

[Jason KY.]

I'm using git bash

[Patrick Massot]

What do you see when running format_project --debug (after fixing your format.toml)?

[Patrick Massot]

Then why don't you use git bash to list files in folders?!

[Jason KY.]

haha, I find just using the file explorer on windows easier :sweat:

[Patrick Massot]

You just proved this assumption was wrong...

[Jason KY.]

This is what I see

format_project --debug

Lean executable path: C:\Users\Jason\.elan\toolchains\3.4.2\bin\lean
LEAN_PATH: C:\Users\Jason\.elan\toolchains\3.4.2\bin\..\lib\lean\library:C:\Users\Jason\OneDrive\Documents\UG Documents\Lean\project\my_project\src:_target\deps\mathlib\src
Template folder: C:\users\jason\appdata\local\programs\python\python37-32\lib\site-packages\format_lean\templates
Tactic state filters:  []

[Patrick Massot]

And this is run from the folder C:\Users\Jason\OneDrive\Documents\UG Documents\Lean\project\my_project\, right?

[Jason KY.]

yes

[Patrick Massot]

this is crazy

[Patrick Massot]

Could you launch the python shell from there, and type:

from pathlib import Path
list(Path('src').glob('**/*.lean'))

[Jason KY.]

How do I open a python shell? Sorry, a bit new to this...

[Patrick Massot]

type python

[Jason KY.]

I get this

$ python
from pathlib import Path
list(Path('src').glob('**/*.lean'))

  File "<stdin>", line 3

    ^
SyntaxError: invalid syntax

[Patrick Massot]

Did you first type python and hit enter?

[Jason KY.]

yeah

[Jason KY.]

should I not do that?

[Patrick Massot]

And it doesn't write anything like:

Python 3.7.2 (default, Feb  2 2019, 10:55:41)
[GCC 7.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>>

[Patrick Massot]

maybe try python3 instead of python?

[Jason KY.]

writing python or python3 just gives me a black space to write on

Jason@DESKTOP-I8Q00VV MINGW64 ~/OneDrive/Documents/UG Documents/Lean/project/my_project (master)
$ python3 --version
Python 3.7.3

Jason@DESKTOP-I8Q00VV MINGW64 ~/OneDrive/Documents/UG Documents/Lean/project/my_project (master)
$ python3

[Bryan Gin-ge Chen]

You may need to follow the steps here to get a working shell: https://stackoverflow.com/questions/32597209/python-not-working-in-the-command-line-of-git-bash

[Bryan Gin-ge Chen]

The simplest thing to do is just to try typing python -i and hitting enter before pasting in the commands that Patrick gave.

[Jason KY.]

aha now it's working

$ python
Python 3.7.3 (v3.7.3:ef4ec6ed12, Mar 25 2019, 21:26:53) [MSC v.1916 32 bit (Inte
l)] on win32
Type "help", "copyright", "credits" or "license" for more information.

[Patrick Massot]

I cannot help with an operating system which is so actively fighting against its users, I'm sorry.

[Patrick Massot]

Who knows how much useful information it is hiding at every time.

[Jason KY.]

Emm, I get this error

>>> from pathlib import Path
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>

[Patrick Massot]

and nothing else?

[Patrick Massot]

This doesn't make any sense.

[Jason KY.]

it also says KeyboardInterrupt after that

[Jason KY.]

>>> from pathlib import Path
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
KeyboardInterrupt

but nothing after this

[Patrick Massot]

I need to go anyway. The quickest way to achieve your goals is probably to install Linux.

[Patrick Massot]

I'm sorry.

[Jason KY.]

Don't worry! Thanks for your help!

[Jason KY.]

I think for now I'll just send my files to @Kevin Buzzard to compile. I'll get a Linux machine anyway after chirstmas :)