--- layout: archive title: Zulip Chat Archive permalink: /stream/113488-general/topic/Trying.20to.20run.20update-mathlib.html ---
I'm trying to get update-mathlib
to work. I am on Windows, and I usually use the msys2 minGW 64-bit
command prompt. I tried installing update-mathlib
on both my msys2
terminal, and in a Git Bash
terminal.
In msys2
, when I try to run the script to get update-mathlib
I get an error. The first line in the output that looks like an error is (full output at the bottom of this message)
requests 2.21.0 has requirement urllib3<1.25,>=1.21.1, but you'll have urllib3 1.25.2 which is incompatible.
It seems like one of my packages is too new?
I now also tried using git bash
with choco
as package manager. Running the install-update-mathlib
script works without errors.
However, if I then run update-mathlib
I get the error that python3
is not found. (does choco
come automatically come with pip
but not with python
? Is that even possible?)
So I install python3
(choco install python3
), but now I get the following error.
Floris@MSI MINGW64 /d/projects/formalabstracts (master) $ update-mathlib Traceback (most recent call last): File "C:/Users/Floris/.mathlib/bin/update-mathlib", line 6, in <module> from github import Github ModuleNotFoundError: No module named 'github'
How do I continue? pip install github
doesn't work.
full output of the msys2 install-update-mathlib
script:
Floris@MSI MINGW64 /d/projects $ curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh Installing python dependencies (at user level) /usr/bin/pip3 Collecting setuptools Downloading https://files.pythonhosted.org/packages/ec/51/f45cea425fd5cb0b0380f5b0f048ebc1da5b417e48d304838c02d6288a1e/setuptools-41.0.1-py2.py3-none-any.whl (575kB) 100% |████████████████████████████████| 583kB 2.0MB/s Installing collected packages: setuptools Successfully installed setuptools-41.0.1 Requirement already up-to-date: toml in /home/Floris/.local/lib/python3.7/site-packages (0.10.0) Collecting PyGithub Downloading https://files.pythonhosted.org/packages/f7/48/ec5ef5239f3a4043ee7e07b454b5f3a024a5f22a4e585400ac6caa22c3c4/PyGithub-1.43.7.tar.gz (107kB) 100% |████████████████████████████████| 112kB 1.1MB/s Collecting urllib3 Downloading https://files.pythonhosted.org/packages/39/ec/d93dfc69617a028915df914339ef66936ea976ef24fa62940fd86ba0326e/urllib3-1.25.2-py2.py3-none-any.whl (150kB) 100% |████████████████████████████████| 153kB 1.5MB/s Collecting certifi Using cached https://files.pythonhosted.org/packages/60/75/f692a584e85b7eaba0e03827b3d51f45f571c2e793dd731e598828d380aa/certifi-2019.3.9-py2.py3-none-any.whl Collecting gitpython Using cached https://files.pythonhosted.org/packages/fe/e5/fafe827507644c32d6dc553a1c435cdf882e0c28918a5bab29f7fbebfb70/GitPython-2.1.11-py2.py3-none-any.whl Collecting deprecated (from PyGithub) Using cached https://files.pythonhosted.org/packages/9f/7a/003fa432f1e45625626549726c2fbb7a29baa764e9d1fdb2323a5d779f8a/Deprecated-1.2.5-py2.py3-none-any.whl Collecting pyjwt (from PyGithub) Using cached https://files.pythonhosted.org/packages/87/8b/6a9f14b5f781697e51259d81657e6048fd31a113229cf346880bb7545565/PyJWT-1.7.1-py2.py3-none-any.whl Collecting requests>=2.14.0 (from PyGithub) Using cached https://files.pythonhosted.org/packages/7d/e3/20f3d364d6c8e5d2353c72a67778eb189176f08e873c9900e10c0287b84b/requests-2.21.0-py2.py3-none-any.whl Collecting gitdb2>=2.0.0 (from gitpython) Using cached https://files.pythonhosted.org/packages/da/30/a407568aa8d8f25db817cf50121a958722f3fc5f87e3a6fba1f40c0633e3/gitdb2-2.0.5-py2.py3-none-any.whl Collecting wrapt<2,>=1 (from deprecated->PyGithub) Using cached https://files.pythonhosted.org/packages/67/b2/0f71ca90b0ade7fad27e3d20327c996c6252a2ffe88f50a95bba7434eda9/wrapt-1.11.1.tar.gz Collecting chardet<3.1.0,>=3.0.2 (from requests>=2.14.0->PyGithub) Using cached https://files.pythonhosted.org/packages/bc/a9/01ffebfb562e4274b6487b4bb1ddec7ca55ec7510b22e4c51f14098443b8/chardet-3.0.4-py2.py3-none-any.whl Collecting idna<2.9,>=2.5 (from requests>=2.14.0->PyGithub) Using cached https://files.pythonhosted.org/packages/14/2c/cd551d81dbe15200be1cf41cd03869a46fe7226e7450af7a6545bfc474c9/idna-2.8-py2.py3-none-any.whl Collecting smmap2>=2.0.0 (from gitdb2>=2.0.0->gitpython) Using cached https://files.pythonhosted.org/packages/55/d2/866d45e3a121ee15a1dc013824d58072fd5c7799c9c34d01378eb262ca8f/smmap2-2.0.5-py2.py3-none-any.whl requests 2.21.0 has requirement urllib3<1.25,>=1.21.1, but you'll have urllib3 1.25.2 which is incompatible. Installing collected packages: wrapt, deprecated, pyjwt, chardet, certifi, urllib3, idna, requests, PyGithub, smmap2, gitdb2, gitpython Running setup.py install for wrapt ... error Complete output from command /usr/bin/python3 -u -c "import setuptools, tokenize;__file__='/tmp/pip-install-ooh4zvm2/wrapt/setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record /tmp/pip-record-yk7wu2wz/install-record.txt --single-version-externally-managed --compile --user --prefix=: running install running build running build_py creating build creating build/lib.mingw64_nt-10.0-3.0.6(0.338 creating build/lib.mingw64_nt-10.0-3.0.6(0.338/5 creating build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7 creating build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt copying src/wrapt/decorators.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt copying src/wrapt/importer.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt copying src/wrapt/wrappers.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt copying src/wrapt/__init__.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt running build_ext Traceback (most recent call last): File "<string>", line 1, in <module> File "/tmp/pip-install-ooh4zvm2/wrapt/setup.py", line 101, in <module> run_setup(with_extensions=True) File "/tmp/pip-install-ooh4zvm2/wrapt/setup.py", line 71, in run_setup setup(**setup_kwargs_tmp) File "/usr/lib/python3.7/distutils/core.py", line 148, in setup dist.run_commands() File "/usr/lib/python3.7/distutils/dist.py", line 966, in run_commands self.run_command(cmd) File "/usr/lib/python3.7/distutils/dist.py", line 985, in run_command cmd_obj.run() File "/home/Floris/.local/lib/python3.7/site-packages/setuptools/command/install.py", line 61, in run return orig.install.run(self) File "/usr/lib/python3.7/distutils/command/install.py", line 545, in run self.run_command('build') File "/usr/lib/python3.7/distutils/cmd.py", line 313, in run_command self.distribution.run_command(command) File "/usr/lib/python3.7/distutils/dist.py", line 985, in run_command cmd_obj.run() File "/usr/lib/python3.7/distutils/command/build.py", line 135, in run self.run_command(cmd_name) File "/usr/lib/python3.7/distutils/cmd.py", line 313, in run_command self.distribution.run_command(command) File "/usr/lib/python3.7/distutils/dist.py", line 985, in run_command cmd_obj.run() File "/tmp/pip-install-ooh4zvm2/wrapt/setup.py", line 25, in run build_ext.run(self) File "/usr/lib/python3.7/distutils/command/build_ext.py", line 308, in run force=self.force) File "/usr/lib/python3.7/distutils/ccompiler.py", line 1034, in new_compiler return klass(None, dry_run, force) File "/usr/lib/python3.7/distutils/cygwinccompiler.py", line 280, in __init__ CygwinCCompiler.__init__ (self, verbose, dry_run, force) File "/usr/lib/python3.7/distutils/cygwinccompiler.py", line 124, in __init__ if self.ld_version >= "2.10.90": TypeError: '>=' not supported between instances of 'NoneType' and 'str' ---------------------------------------- Command "/usr/bin/python3 -u -c "import setuptools, tokenize;__file__='/tmp/pip-install-ooh4zvm2/wrapt/setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record /tmp/pip-record-yk7wu2wz/install-record.txt --single-version-externally-managed --compile --user --prefix=" failed with error code 1 in /tmp/pip-install-ooh4zvm2/wrapt/
@Patrick Massot
I don't know anything about Windows but I've seen the requests 2.21.0 has requirement urllib3<1.25,>=1.21.1,
warning. I fear this is totally out of our control, see https://github.com/kennethreitz/requests/issues/4673 and dozen of google his when asking about this message
Can I downgrade urllib3
?
This message is a warning only right?
I think it worked anyway
Also, I don't know if this is Windows-specific, but when I install python, with choco install python3
, I only get the python
command, not python3
:
Floris@MSI MINGW64 /d/projects $ python --version Python 3.7.3 Floris@MSI MINGW64 /d/projects $ which python /c/Python37/python Floris@MSI MINGW64 /d/projects $ which python3 which: no python3 in [...]
On a related note, and more naively, how do I tell if update-mathlib
worked? I run the command and it says it extracts the nightly, but which repo can I compare it to?
It might be only a warning. It was printed red in msys2
, so it looked important.
The issue is that I have no way to get a Windows computer anywhere here. I'm always amazed to see how people in the US seem to use Windows. In France I know no mathematician or computer scientist using Windows
My secretary will be on vacation next week, but I can't enter her office and use her Windows computer (I need to become a German professor, I'm sure they can do that)
that's unfortunate. I have the feeling something is wrong with my setup: the install-update-mathlib
script seems to install all dependencies, but then they are not imported when running update-mathlib
.
Maybe it's a python2 vs python3 issue
On a related note, and more naively, how do I tell if
update-mathlib
worked? I run the command and it says it extracts the nightly, but which repo can I compare it to?
If it says extracting
then I don't see what could fail after that. And you don't want to compare anything. You want to import stuff from mathlib in your project and see it working (without delay suggesting Lean is rebuilding everything from scratch).
I might have installed python now multiple times... so that might be a problem
Floris, aren't you in Pittsburgh like everyone else?
yes, I am
Why don't you walk down that corridor until you reach Simon? Then you could fix this once and for all?
@Simon Hudon you have 10 seconds... Run!
Remote debugging of an alien operating system is extremely difficult
Well, we're at different universities. But I'll do that
Makes sense. Thanks for you help anyway Patrick!
French people always have difficulties imagining USA length scale. We always speak of walking when you need to take a plane to go to the restroom
I would love to help you more, but I'm sure it will be easier for everyone, including you
:thumbs_up:
I didn't know there were several Lean university in Pittsburgh
The other Lean university was exclusively a HOL Light university until a few years ago...
I'm now in my office if you want me to have a look @Floris van Doorn
{% endraw %}Last updated: Apr 24 2020 at 19:02 UTC


It’sablog 2008/08/17
I really did make a mistake a few weeks ago, losing my old Wordpress blog, the theme, and all of the non-Wordpress extras I had in that directory tree. More fuel for the argument that upgrading Wordpress is too hard. I thought I was smart enough to do it. I was wrong. So I took that as motivation to build the command-line blog I’ve always wanted. Then I went on vacation. As you can see, it's finished now. More soon on the code.
I kept a text file open during my flights to and from Kentucky. On the plane I was reading The World Is Flat and it surprisingly tempered very few of the thoughts I liked enough to write down. (Afterthoughts in bold.)
 The rest is just details.
My del.icio.us network is better for me than Digg/Reddit/whatever because I trust the sources.  I’m the Commander and I pick my Generals carefully. (After reading Del.icio.us vs. Friendfeed.)
Neverminding your opinion of Chris Matthews and his Hardball show, it’s depressing that the airport cuts away from the last 20 minutes in favor of an Olympic human-interest segment on using chopsticks in Beijing.
I also spent some time thinking about my upcoming move. Moving within the city and with over a year’s experience living here have significantly changed my criteria. Most importantly, Katherine will be moving out, too. Beyond the need for a bigger apartment, here are some of my current considerations:
- Opportunity to grill.
- A deck or yard or something to go with the grilling.
- Dishwasher.
- A proper sink in the kitchen instead of the miniature joke of one I have now. This is perhaps less important with the addition of a dishwasher.
- More windows! I miss my 7-window bedroom from senior year of college.
- A grocery store within walking distance. (I’ve grown quite fond of Real Foods being 3 blocks from my house.)
Lesser concerns that didn't make the cut:
- A garage.
- Non-coin-operated laundry.
- Higher-speed Internet access (LAN, plz).
Anything I’m missing?
Comments (3)
- Bus lines nearby - That's all I can think of. best of luck finding the new place :)
— Dimitry — 2008-08-18 6:34 am
I'm desperately afraid of del.icio.us going away because my del network is the *only* way I keep up, everything else just gets in the way.
But mostly wanted to say *congratulations* on Katherine moving out, and on getting out of the Marina.
— kellan — 2008-08-18 6:11 pm
Check out the sunset district, if you can live with the daily fog.
— John — 2008/08/26 1:19 am


HTML
Hypertext Markup Language (HTML) is the standard markup language for documents designed to be displayed in a web browser.
CSS
CSS is a language that describes the style of an HTML document. CSS describes how HTML elements should be displayed.
JS
JavaScript (often shortened to JS) is a lightweight, interpreted, object-oriented language with first-class functions, and is best known as the scripting language for Web pages, but it's used in many non-browser environments as well. It is a prototype-based, multi-paradigm scripting language that is dynamic, and supports object-oriented, imperative, and functional programming styles.


Authenticated Encryption Algorithms - This scenario demonstrates how to perform Authenticated Encryption and Decryption with the WinRT APIs.


Are you sure you want to install all fields?
This will install all field(s) that are not installed in the database.
Are you sure you want to drop table?


Samantha Giles hints at return to Emmerdale just one day after her exit
Bernice left viewers heartbroken as she departed last night
by Carena CrawfordBernice Blackstock called off her wedding to Liam Cavanagh last night and departed Emmerdale for Australia.
While fans were left heartbroken over her exit as she went to care for her ex-husband, father of daughter Dee Dee, who'd had an accident, actress Samantha Giles has revealed it might not be the end after all...
Speaking on Friday's This Morning (November 29) to hosts Eamonn Holmes and Ruth Langsford, Samantha said she would never rule out a return.
Read more: Emmerdale fans predict more heartache for Tracy
"I've said so many times 'I wouldn't do this, I wouldn't do that' and you end up doing them, so never say never," she told Eamonn when he pointed out she could go back.
"But for now, the door's closed."
Samantha has played Bernice on and off for 21 years.
Her most recent run of seven years was the longest, and she told the presenters why it was time for a change.
"I just felt it was the right time, I'd been thinking about it for a couple of years and like a lot of actors I've got itchy feet.
"I need a change, I want to play something a bit more gritty, I want to do some other stuff, there's so many things out there..."
But her next project might not be acting - she told the hosts she's written two children's books.
The stories are inspired by the other side of her life where the actress practices witchcraft.
Read more: Emmerdale SPOILERS: David becomes a daddy at Christmas?
Samantha is a witch and uses wicker spells and charms and even told how she cast a spell to meet her ideal man - and then her husband came into her life.
It was also revealed This Morning's Sharon Marshall credits Samantha with helping her to have her miracle baby, Betsey.
"I gave her a change of luck charm which she used to help with the IVF," Sam admitted.
Leave us a comment on our Facebook page @EntertainmentDailyFix and let us know what you think!


SourceJS is a dynamic Style Guide platform. It allows to combine multiple project UI component libraries, based on any technologies.
Following Living Style Guide driven development,
SourceJS allows to code new components directly in the Style Guide.


|
| def | __init__ (self, machine_type, h=None, J=None, Q=None, king_graph=None, var_type=openjij.SPIN) |
| |
| def | get_ising_king_graph (self) |
| |
| def | king_indices (self) |
| |
| def | convert_to_index (self, x, y) |
| |
| def | __init__ (self, h=None, J=None, Q=None, var_type=openjij.SPIN) |
| |
| def | get_cxxjij_ising_graph (self, sparse=False) |
| |
| def | ising_interactions (self) |
| |
| def | interactions (self, re_calculate=False) |
| |
| def | calc_energy (self, state, need_to_convert_from_spin=False) |
| |
| def | ising_dictionary (self) |
| |
BQM for king graph of HITACHI CMOS Annealer
Attributes
---------
xrange : list of int
represents hardware (CMOS) restricts for coordinate. [xmin, xmax]
yrange : list of int
represents hardware (CMOS) restricts for coordinate. [ymin, ymax]
prange : list of int
represents hardware (CMOS) restricts for the strength of interactions 'p'. [pmin, pmax]
king_graph : list of list of int
Annealing cloud Web API format representation of interaction coefficients
Quadratic term [x1, y1, x2, y2, value]
Linear term [x1, y1, x1, y1, value]
| def openjij.model.king_graph.KingGraph.__init__ |
( |
|
self, |
|
|
|
machine_type, |
|
|
|
h = None , |
|
|
|
J = None , |
|
|
|
Q = None , |
|
|
|
king_graph = None , |
|
|
|
var_type = openjij.SPIN |
|
) |
| |
The constructor reformat interactions to Web API format (ising king graph),
and validates that the interaction is in King Graph.
----------
machine_type : int
choose 'ASIC' or 'FPGA'
king_graph : list of list
represents ising or QUBO interaction.
Each spins are decided by 2-d corrdinate x, y.
Quadratic term [x1, y1, x2, y2, value]
Linear term [x1, y1, x1, y1, value]


|
|
| Adafruit_FT6206 (void) |
| | Instantiates a new FT6206 class.
|
| |
| boolean | begin (uint8_t thresh=FT6206_DEFAULT_THRESSHOLD) |
| | Setups the I2C interface and hardware, identifies if chip is found. More...
|
| |
| uint8_t | touched (void) |
| | Determines if there are any touches detected. More...
|
| |
| TS_Point | getPoint (uint8_t n=0) |
| | Queries the chip and retrieves a point data. More...
|
| |
◆ begin()
| boolean Adafruit_FT6206::begin |
( |
uint8_t |
thresh = FT6206_DEFAULT_THRESSHOLD | ) |
|
Setups the I2C interface and hardware, identifies if chip is found.
- Parameters
-
| thresh | Optional threshhold-for-touch value, default is FT6206_DEFAULT_THRESSHOLD but you can try changing it if your screen is too/not sensitive. |
- Returns
- True if an FT6206 is found, false on any failure
◆ touched()
| uint8_t Adafruit_FT6206::touched |
( |
void |
| ) |
|
Determines if there are any touches detected.
- Returns
- Number of touches detected, can be 0, 1 or 2
◆ getPoint()
| TS_Point Adafruit_FT6206::getPoint |
( |
uint8_t |
n = 0 | ) |
|
Queries the chip and retrieves a point data.
- Parameters
-
| n | The # index (0 or 1) to the points we can detect. In theory we can detect 2 points but we've found that you should only use this for single-touch since the two points cant share the same half of the screen. |
- Returns
- TS_Point object that has the x and y coordinets set. If the z coordinate is 0 it means the point is not touched. If z is 1, it is currently touched.
The documentation for this class was generated from the following files: