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

Use pipx for installation of mathlibtools #77

Merged
merged 4 commits into from
Jul 10, 2020

Conversation

TwoFX
Copy link
Member

@TwoFX TwoFX commented Jun 30, 2020

This is my attempt at the most likely abandoned #74, trying to address the fact that using sudo pip3 install seems to be discouraged (cf. this comment). The easiest way of installing end-user software from PyPI that follows "best practices" that I am aware of is pipx, which in particular has a command ensurepath that does all the PATH fiddling (which is not necessary when using sudo, but is necessary when using --user) automatically. This PR changes the instructions to follow this route.

@dimpase
Copy link

dimpase commented Jun 30, 2020

I'd have mentioned what pipx does, e.g.

(along with a support tool [pipx](https://pipxproject.github.io/pipx/))

@TwoFX
Copy link
Member Author

TwoFX commented Jul 1, 2020

I'd have mentioned what pipx does, e.g.

(along with a support tool [pipx](https://pipxproject.github.io/pipx/))

Good point. I've added this and also took the liberty to slightly homogenize the different guides.

```bash
python3 -m pip install --user pipx
python3 -m pipx ensurepath
pipx install mathlibtools
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sadly, this doesn't work. I just followed the instructions on a fresh Windows 10 machine, and upon getting to this step pipx install mathlibtools just says bash: pipx: command not found.

I closed and restarted "git bash", and get the same message. I rebooted the windows machine (I have not yet tried unplugging the router...) and get the same message.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for testing this. I'm looking into it.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

pipx is known to work on Windows, so the question is about what goes wrong in your environment. Something semi-trivial with PATH, I suppose. Hard to tell without a Windows box (or at least a VM) in front of me.

Copy link
Member Author

@TwoFX TwoFX Jul 8, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The first problem is that pipx ensurepath modifies the Windows PATH variable, but we want to modify the git bash PATH, which is different.

After manually setting the path, there was also some venv problem, which can probably be fixed, but I didn't try very hard.

@TwoFX
Copy link
Member Author

TwoFX commented Jul 8, 2020

Despite pipx documentation claiming that it works on Windows, I was unable to confirm that this is indeed the case, so I decided to roll back the changes. Global pip install doesn't require administrator privileges on Windows anyway, the difference between global and user install is merely whether the package is installed to AppData/Local (global) or AppData/Roaming (User), so personally I think manually having the user figure out the correct path (which includes both the user name and the Python version number) is not worth it. I have also rolled back the changes to macos.md; while i believe that it should work similar to Linux (replacing apt with brew), I have no way to verify this.

@PatrickMassot
Copy link
Member

@TwoFX am I correct in thinking that instructions in this PR now match what is done by the automatic scripts, hence work? Could you have a look at the git conflict?

@TwoFX
Copy link
Member Author

TwoFX commented Jul 10, 2020

@TwoFX am I correct in thinking that instructions in this PR now match what is done by the automatic scripts, hence work?

Yes the instructions match.

Could you have a look at the git conflict?

I merged; is the conflict resolved?

@PatrickMassot PatrickMassot merged commit 65a94aa into leanprover-community:newsite Jul 10, 2020
@PatrickMassot
Copy link
Member

Actually, the conflicts were due to the complicated git history. The end result was not conflicting, so I squashed. Thanks again for looking into all this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants