Planet Python

#638 – JULY 16, 2024
View in Browser »

Customize VS Code Settings

In this course, Philipp helps you customize your Visual Studio Code settings to switch from a basic cluttered look to a clean presentable look. This is not just pleasant on the eyes, but also gives you a nice user interface if you want to share on a Zoom call or screen recording.
REAL PYTHON course

Incident Report: Leaked GitHub Personal Access Token

A PyPI admin accidentally leaked credentials into a Docker container. It has since been fixed and the credentials revoked. This is the report by that same admin outlining what happened and how to help prevent similar mistakes in the future.
EE DURBIN

GPU Accelerate Your Data Science Workflows End-to-End

Discover how to create, accelerate, and deploy data pipelines with RAPIDS for GPU-accelerated data science workflows. Take one of our Data Science courses for free when you join the NVIDIA Developer Program →
NVIDIA sponsor

Free-Threaded CPython Is Ready to Experiment With!

An overview of the ongoing efforts to improve and roll out support for free-threaded CPython throughout the Python open source ecosystem. Associated Hacker News discussion.
RALF GOMMERS

PSF Announces Infrastructure Engineer

PYTHON SOFTWARE FOUNDATION

DjangoCon US 2024 Announces Talks

DJANGOCON

Django Security Releases Issued: 5.0.7 and 4.2.14

DJANGO SOFTWARE FOUNDATION

Register for Kiwi PyCon, Aug 23-25

KIWIPYCON.NZ • Shared by Kiwi PyCon

Quiz: Split Datasets With scikit-learn.train_test_split()

REAL PYTHON

Python Jobs Python Tutorial Writer (Anywhere)

Real Python

Python Video Course Instructor (Anywhere)

Real Python

More Python Jobs >>>

Articles & Tutorials Free, Unbelievably Stupid Wi-Fi on Long-Haul Flights

Deep in a need to procrastinate on a flight between London and San Francisco, Robert discovered that changing his name on an airline’s frequent flyer account was free over the plane’s WiFi. What’s a developer to do? Work on their tickets? No, create an entire TCP/IP protocol using this loophole. The result is the PySkyWiFi package.
ROBERT HEATON

Digging Into Graph Theory in Python With David Amos

Have you wondered about graph theory and how to start exploring it in Python? What resources and Python libraries can you use to experiment and learn more? This week on the show, former co-host David Amos returns to talk about what he’s been up to and share his knowledge about graph theory in Python.
REAL PYTHON

My Programming Beliefs as of July 2024

This collection of thoughts outlines how Evan approaches coding, with the understanding that this might change in the future. His beliefs include using spikes, the difference between simple and easy, a preference for enums over booleans, and more.
EVAN HAHN

Breaking Out of Nested Loops With Generators

Have you ever had the situation where you’ve got a nested loop and need to break out of the outer one? One way of dealing with this problem is refactoring the loop to use a generator. This post shows you how.
RODRIGO GIRÃO SERRÃO

“Extracting Wisdom” From Conference Videos

There are so many conferences and so many videos, you can’t possibly watch them all. This post shows you how to extract information to summarize a talk so you can quickly decide what you want to watch.
GONÇALO VALÉRIO

Creating a Simple Pastebin Service in Python and Flask

Learn how to build a functional pastebin service using Python and Flask. This tutorial covers web development basics, file handling, and syntax highlighting.
MUHAMMAD RAZA

How a Decorator Crashed My Flask App

This blog post shows how failing to use functools.wraps can cause issues with FlaskAPI. Learn why you should always use wraps and what went wrong.
SUYOG DAHAL

Python Has Too Many Package Managers

Overview of Python’s Package management ecosystem in 2024 and associated Hacker News Discussion
LARRY DU

Creating Images in Your Terminal With Python and Rich Pixels

Rich Pixels, a package from one of the folks at Textual, allows you to create images in your terminal and display them.
MIKE DRISCOLL

How Do You Choose Python Function Names?

This tutorial discusses the rules and conventions for choosing Python function names and why they’re important.
REAL PYTHON

Using HTMX With FastAPI

This tutorial looks at how use HTMX with FastAPI by creating a simple todo web app and deploying it on Render.
PAUL ESCH-LAURENT • Shared by Michael Herman

Projects & Code ViperIDE: MicroPython IDE for Web and Mobile

GITHUB.COM/VSHYMANSKYY

ML System Design: 450 Case Studies to Learn From

EVIDENTLYAI.COM • Shared by Daria Maliugina

reladiff: High-Perf Diffing of Large Datasets Across Databases

GITHUB.COM/EREZSH

Yen: The Last Python Environment Manager You’ll Ever Need

GITHUB.COM/TUSHARSADHWANI • Shared by Tushar Sadhwani

Events Weekly Real Python Office Hours Q&A (Virtual)

July 17, 2024
REALPYTHON.COM

PyData Bristol Meetup

July 18, 2024
MEETUP.COM

PyLadies Dublin

July 18, 2024
PYLADIES.COM

Chattanooga Python User Group

July 19 to July 20, 2024
MEETUP.COM

PyKla Monthly Meetup

July 24, 2024
MEETUP.COM

PyLadies Amsterdam

July 24, 2024
MEETUP.COM

PyOhio 2024

July 27 to July 28, 2024
PYOHIO.ORG

Happy Pythoning!
This was PyCoder’s Weekly Issue #638.
View in Browser »

[ Subscribe to 🐍 PyCoder’s Weekly 💌 – Get the best Python news, articles, and tutorials delivered to your inbox once a week >> Click here to learn more ]

Web scraping is the process of collecting and parsing raw data from the Web, and the Python community has come up with some pretty powerful web scraping tools.

The Internet hosts the greatest source of information on the planet. Many disciplines, such as data science, business intelligence, and investigative reporting, can benefit enormously from collecting and analyzing data from websites.

In this course, you’ll practice:

• Parsing website data using string methods and regular expressions
• Parsing website data using an HTML parser
• Interacting with forms and other website components

[ Improve Your Python With 🐍 Python Tricks 💌 – Get a short & sweet Python Trick delivered to your inbox every couple of days. >> Click here to learn more and see examples ]

At the beginning one goes to the conferences to listen to the talks and make new contacts. You meet a lot of new faces every time. Over time a few of them will become great friends and then all conferences will become about friends.

We wait for the conferences so that we can meet our friends. I went back to PyCon US this year after 5 years, means I met many friends after 5 years. It was so happy feeling to see them again.

Last week I went to my first ever Euro Python in Prague, finally the visa was good in the right days of the year. This means I managed to meet more friends, a few of them just after a month (as they were present in PyCon US) and some after many many years. Really enjoyed the social event place selections by the organizers.

Personally the social events allowed me to go full scale nerd out on technical and social issues with friends. I was really missing these discussions. Heard more stories and discussed about fun ideas. One is below :)

$ python Python 3.12.4 (main, Jun 7 2024, 00:00:00) [GCC 14.1.1 20240607 (Red Hat 14.1.1-5)] on linux Type "help", "copyright", "credits" or "license" for more information. >>> hello 🤌🤌🤌 Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'hello' is not defined. Did you mean: 'help'? >>> [].set("different exception") 🤌🤌🤌 Traceback (most recent call last): File "<stdin>", line 1, in <module> AttributeError: 'list' object has no attribute 'set' >>>

A newer Python package called Rich Pixels allows you to create images in your terminal and display them. Darren Burns, one of the team members from the Textual project, created this package.

Anyway, let’s find out how to use Rich Pixels!

Installation

You can install Rich Pixels using Python’s pip utility. Here’s how:

python -m pip install rich-pixels

Once you have Rich Pixels installed, you can try it out!

Displaying Images in the Terminal

Rich Pixels lets you take a pre-existing image and show it in your terminal. The higher the image’s resolution, the better the output will be. However, if your image has too many pixels, it probably won’t fit in your terminal, and much of it will be drawn off-screen.

For this example, you will use the Python Show Podcast logo and attempt to draw it in your terminal.

Open up your favorite Python editor and add the following code to it:

from rich_pixels import Pixels from rich.console import Console console = Console() pixels = Pixels.from_image_path("python_show200.jpg") console.print(pixels)

For this example, you will use a square image that is 200×200 pixels. You can run the code like this in your terminal:

python pixels.py

When you execute the command above, you will see something like this in your terminal:

 

As you can see, the image is a little pixelated and gets cut off at the bottom. Of course, this all depends on your monitor’s resolution.

Here’s what happens when you use an image that is 80×80 pixels:

You can also. use the Pillow package to create an image object and pass that the Rich Pixels too. Here’s how that might look:

with Image.open("path/to/image.png") as image: pixels = Pixels.from_image(image)

You can create or draw your images using Pillow. There is some coverage of this topic in my article, Drawing Shapes on Images with Python and Pillow which you could then pass to Rich Pixels to display it.

Wrapping Up

Rich Pixels is a fun way to add extra pizzazz to your terminal applications. Rich Pixels can also be used in a Textual application. While there probably aren’t a lot of use cases for this package, it’s a lot of fun to play around with.

Give it a try, and let me know what you create!

The post Creating Images in Your Terminal with Python and Rich Pixels appeared first on Mouse Vs Python.

One of the key aspects of supervised machine learning is model evaluation and validation. When you evaluate the predictive performance of your model, it’s essential that the process be unbiased. Using train_test_split() from the data science library scikit-learn, you can split your dataset into subsets that minimize the potential for bias in your evaluation and validation process.

In this tutorial, you’ll learn:

• Why you need to split your dataset in supervised machine learning
• Which subsets of the dataset you need for an unbiased evaluation of your model
• How to use train_test_split() to split your data
• How to combine train_test_split() with prediction methods

In addition, you’ll get information on related tools from sklearn.model_selection.

Get Your Code: Click here to download the free sample code that you’ll use to learn about splitting your dataset with scikit-learn’s train_test_split().

Take the Quiz: Test your knowledge with our interactive “Split Your Dataset With scikit-learn's train_test_split()” quiz. You’ll receive a score upon completion to help you track your learning progress:

Interactive Quiz

Split Your Dataset With scikit-learn's train_test_split()

In this quiz, you'll test your understanding of how to use the train_test_split() function from the scikit-learn library to split your dataset into subsets for unbiased evaluation in machine learning.

The Importance of Data Splitting

Supervised machine learning is about creating models that precisely map the given inputs to the given outputs. Inputs are also called independent variables or predictors, while outputs may be referred to as dependent variables or responses.

How you measure the precision of your model depends on the type of a problem you’re trying to solve. In regression analysis, you typically use the coefficient of determination, root mean square error, mean absolute error, or similar quantities. For classification problems, you often apply accuracy, precision, recall, F1 score, and related indicators.

The acceptable numeric values that measure precision vary from field to field. You can find detailed explanations from Statistics By Jim, Quora, and many other resources.

What’s most important to understand is that you usually need unbiased evaluation to properly use these measures, assess the predictive performance of your model, and validate the model.

This means that you can’t evaluate the predictive performance of a model with the same data you used for training. You need evaluate the model with fresh data that hasn’t been seen by the model before. You can accomplish that by splitting your dataset before you use it.

Training, Validation, and Test Sets

Splitting your dataset is essential for an unbiased evaluation of prediction performance. In most cases, it’s enough to split your dataset randomly into three subsets:

1. The training set is applied to train or fit your model. For example, you use the training set to find the optimal weights, or coefficients, for linear regression, logistic regression, or neural networks.

2. The validation set is used for unbiased model evaluation during hyperparameter tuning. For example, when you want to find the optimal number of neurons in a neural network or the best kernel for a support vector machine, you experiment with different values. For each considered setting of hyperparameters, you fit the model with the training set and assess its performance with the validation set.

3. The test set is needed for an unbiased evaluation of the final model. You shouldn’t use it for fitting or validation.

In less complex cases, when you don’t have to tune hyperparameters, it’s okay to work with only the training and test sets.

Underfitting and Overfitting

Splitting a dataset might also be important for detecting if your model suffers from one of two very common problems, called underfitting and overfitting:

1. Underfitting is usually the consequence of a model being unable to encapsulate the relations among data. For example, this can happen when trying to represent nonlinear relations with a linear model. Underfitted models will likely have poor performance with both training and test sets.

2. Overfitting usually takes place when a model has an excessively complex structure and learns both the existing relations among data and noise. Such models often have bad generalization capabilities. Although they work well with training data, they usually yield poor performance with unseen test data.

You can find a more detailed explanation of underfitting and overfitting in Linear Regression in Python.

Prerequisites for Using train_test_split()

Now that you understand the need to split a dataset in order to perform unbiased model evaluation and identify underfitting or overfitting, you’re ready to learn how to split your own datasets.

You’ll use version 1.5.0 of scikit-learn, or sklearn. It has many packages for data science and machine learning, but for this tutorial, you’ll focus on the model_selection package, specifically on the function train_test_split().

Note: While this tutorial is tested with this specific version of scikit-learn, the features that you’ll use are core to the library and should work equivalently in other versions of scikit-learn as well.

You can install sklearn with pip:

Read the full article at https://realpython.com/train-test-split-python-data/ »

[ Improve Your Python With 🐍 Python Tricks 💌 – Get a short & sweet Python Trick delivered to your inbox every couple of days. >> Click here to learn more and see examples ]

In this quiz, you’ll test your understanding of Python generators.

Generators and the Python yield statement can help you when you’re working with large datasets that might overwhelm your machine’s memory. Another use case is when you have a complex function that needs to maintain an internal state every time it’s called.

When you understand Python generators, then you’ll be able to work with large datasets in a more Pythonic fashion, create generator functions and expressions, and apply your knowledge towards building efficient data pipelines.

[ Improve Your Python With 🐍 Python Tricks 💌 – Get a short & sweet Python Trick delivered to your inbox every couple of days. >> Click here to learn more and see examples ]

In this quiz, you’ll test your understanding of how to write beautiful Python code with PEP 8.

By working through this quiz, you’ll revisit the key guidelines laid out in PEP 8 and how to set up your development environment to write PEP 8 compliant Python code.

[ Improve Your Python With 🐍 Python Tricks 💌 – Get a short & sweet Python Trick delivered to your inbox every couple of days. >> Click here to learn more and see examples ]

If you are on the latest Firefox 128 (which is there on Fedora 40), you should uncheck the following preference to disable Privacy-Preserving Attribution. Firefox added this experimental feature and turn it on by default for everyone. Which should not be the case.

You can find it in the preferences window.

Network packet brokers and automation in Python 2024-07-15, by Dariusz Suchojad

Packet brokers are crucial for network engineers, providing a clear, detailed view of network traffic, aiding in efficient issue identification and resolution.

But what is a network packet broker (NBP) really? Why are they needed? And how to automate one in Python?

➤ Read this article about network packet brokers and their automation in Python to find out more.

More resources

➤ Click here to read more about using Python and Zato in telecommunications
➤ Python API integration tutorial
➤ What is an integration platform?

More blog posts➤

In this quiz, you’ll test your understanding of how to flatten a list in Python.

You’ll write code and answer questions to revisit the concept of converting a multidimensional list, such as a matrix, into a one-dimensional list.

[ Improve Your Python With 🐍 Python Tricks 💌 – Get a short & sweet Python Trick delivered to your inbox every couple of days. >> Click here to learn more and see examples ]

In this quiz, you’ll test your understanding of Python Type Checking.

By working through this quiz, you’ll revisit type annotations and type hints, adding static types to code, running a static type checker, and enforcing types at runtime.

[ Improve Your Python With 🐍 Python Tricks 💌 – Get a short & sweet Python Trick delivered to your inbox every couple of days. >> Click here to learn more and see examples ]

In June I was at the PLDI conference in Copenhagen to present a paper I co-authored with Max Bernstein. I also finally met John Regehr, who I'd been talking on social media for ages but had never met. John has been working on compiler correctness and better techniques for building compilers and optimizers since a very long time. The blog post Finding JIT Optimizer Bugs using SMT Solvers and Fuzzing was heavily inspired by this work. We talked a lot about his and his groups work on using Z3 for superoptimization and for finding missing optimizations. I have applied some of the things John told me about to the traces of PyPy's JIT, and wanted to blog about that. However, my draft felt quite hard to understand. Therefore I have now written this current post, to at least try to provide a somewhat gentler on-ramp to the topic.

In this post we will use the Python-API to Z3 to find local peephole rewrite rules for the operations in the intermediate representation of PyPy's tracing JIT. The code for this is simple enough that we can go through all of it.

The PyPy JIT produces traces of machine level instructions, which are optimized and then turned into machine code. The optimizer uses a number of approaches to make the traces more efficient. For integer operations it applies a number of arithmetic simplification rules rules, for example int_add(x, 0) -> x. When implementing these rules in the JIT there are two problems: How do we know that the rules are correct? And how do we know that we haven't forgotten any rules? We'll try to answer both of these, but the first one in particular.

We'll be using Z3, a satisfiability module theories (SMT) solver which has good bitvector support and most importantly an excellent Python API. We can use the solver to reason about bitvectors, which are how we will model machine integers.

To find rewrite rules, we will consider the binary operations (i.e. those taking two arguments) in PyPy traces that take and produce integers. The completely general form op(x, y) is not simplifiable on its own. But if either x == y or if one of the arguments is a constant, we can potentially simplify the operation into a simpler form. The results are either the variable x, or a (potentially different) constant. We'll ignore constant-folding where both arguments of the binary operation are constants. The possible results for a simplifiable binary operation are the variable x or another constant. This leaves the following patterns as possibilities:

• op(x, x) == x
• op(x, x) == c1
• op(x, c1) == x
• op(c1, x) == x
• op(x, c1) == c2
• op(c1, x) == c2

Our approach will be to take every single supported binary integer operation, instantiate all of these patterns, and try to ask Z3 whether the resulting simplification is valid for all values of x.

Quick intro to the Z3 Python-API

Here's a terminal session showing the use of the Z3 Python API:

>>>> import z3 >>>> # construct a Z3 bitvector variable of width 8, with name x: >>>> x = z3.BitVec('x', 8) >>>> # construct a more complicated formula by using operator overloading: >>>> x + x x + x >>>> x + 1 x + 1

Z3 checks the "satisfiability" of a formula. This means that it tries to find an example set of concrete values for the variables that occur in a formula, such that the formula becomes true. Examples:

>>>> solver = z3.Solver() >>>> solver.check(x * x == 3) unsat >>>> # meaning no x fulfils this property >>>> >>>> solver.check(x * x == 9) sat >>>> model = solver.model() >>>> model [x = 253] >>>> model[x].as_signed_long() -3 >>>> # 253 is the same as -3 in two's complement arithmetic with 8 bits

In order to use Z3 to prove something, we can ask Z3 to find counterexamples for the statement, meaning concrete values that would make the negation of the statement true:

>>>> solver.check(z3.Not(x ^ -1 == ~x)) unsat

The result unsat means that we just proved that x ^ -1 == ~x is true for all x, because there is no value for x that makes not (x ^ -1 == ~x) true (this works because -1 has all the bits set).

If we try to prove something incorrect in this way, the following happens:

>>>> solver.check(z3.Not(x ^ -1 == x)) sat

sat shows that x ^ -1 == x is (unsurprisingly) not always true, and we can ask for a counterexample:

>>>> solver.model() [x = 0]

This way of proving this works because the check calls try to solve an (implicit) "exists" quantifier, over all the Z3 variables used in the formula. check will either return z3.unsat, which means that no concrete values make the formula true; or z3.sat, which means that you can get some concrete values that make the formula true by calling solver.model().

In math terms we prove things using check by de-Morgan's rules for quantifiers:

$$ \lnot \exists x: \lnot f(x) \implies \forall x: f(x) $$

Now that we've seen the basics of using the Z3 API on a few small examples, we'll use it in a bigger program.

Encoding the integer operations of RPython's JIT into Z3 formulas

Now we'll use the API to reason about the integer operations of the PyPy JIT intermediate representation (IR). The binary integer operations are:

opnames2 = [ "int_add", "int_sub", "int_mul", "int_and", "int_or", "int_xor", "int_eq", "int_ne", "int_lt", "int_le", "int_gt", "int_ge", "uint_lt", "uint_le", "uint_gt", "uint_ge", "int_lshift", "int_rshift", "uint_rshift", "uint_mul_high", "int_pydiv", "int_pymod", ]

There's not much special about the integer operations. Like in LLVM, most of them are signedness-independent: int_add, int_sub, int_mul, ... work correctly for unsigned integers but also for two's-complement signed integers. Exceptions for that are order comparisons like int_lt etc. for which we have unsigned variants uint_lt etc. All operations that produce a boolean result return a full-width integer 0 or 1 (the PyPy JIT supports only word-sized integers in its intermediate representation)

In order to reason about the IR operations, some ground work:

import z3 INTEGER_WIDTH = 64 solver = z3.Solver() solver.set("timeout", 10000) # milliseconds, ie 10s xvar = z3.BitVec('x', INTEGER_WIDTH) constvar = z3.BitVec('const', INTEGER_WIDTH) constvar2 = z3.BitVec('const2', INTEGER_WIDTH) TRUEBV = z3.BitVecVal(1, INTEGER_WIDTH) FALSEBV = z3.BitVecVal(0, INTEGER_WIDTH)

And here's the a function to turn an integer IR operation of PyPy's JIT into Z3 formulas:

def z3_expression(opname, arg0, arg1=None): """ computes a tuple of (result, valid_if) of Z3 formulas. `result` is the formula representing the result of the operation, given argument formulas arg0 and arg1. `valid_if` is a pre-condition that must be true for the result to be meaningful. """ result = None valid_if = True # the precondition is mostly True, with few exceptions if opname == "int_add": result = arg0 + arg1 elif opname == "int_sub": result = arg0 - arg1 elif opname == "int_mul": result = arg0 * arg1 elif opname == "int_and": result = arg0 & arg1 elif opname == "int_or": result = arg0 | arg1 elif opname == "int_xor": result = arg0 ^ arg1 elif opname == "int_eq": result = cond(arg0 == arg1) elif opname == "int_ne": result = cond(arg0 != arg1) elif opname == "int_lt": result = cond(arg0 < arg1) elif opname == "int_le": result = cond(arg0 <= arg1) elif opname == "int_gt": result = cond(arg0 > arg1) elif opname == "int_ge": result = cond(arg0 >= arg1) elif opname == "uint_lt": result = cond(z3.ULT(arg0, arg1)) elif opname == "uint_le": result = cond(z3.ULE(arg0, arg1)) elif opname == "uint_gt": result = cond(z3.UGT(arg0, arg1)) elif opname == "uint_ge": result = cond(z3.UGE(arg0, arg1)) elif opname == "int_lshift": result = arg0 << arg1 valid_if = z3.And(arg1 >= 0, arg1 < INTEGER_WIDTH) elif opname == "int_rshift": result = arg0 << arg1 valid_if = z3.And(arg1 >= 0, arg1 < INTEGER_WIDTH) elif opname == "uint_rshift": result = z3.LShR(arg0, arg1) valid_if = z3.And(arg1 >= 0, arg1 < INTEGER_WIDTH) elif opname == "uint_mul_high": # zero-extend args to 2*INTEGER_WIDTH bit, then multiply and extract # highest INTEGER_WIDTH bits zarg0 = z3.ZeroExt(INTEGER_WIDTH, arg0) zarg1 = z3.ZeroExt(INTEGER_WIDTH, arg1) result = z3.Extract(INTEGER_WIDTH * 2 - 1, INTEGER_WIDTH, zarg0 * zarg1) elif opname == "int_pydiv": valid_if = arg1 != 0 r = arg0 / arg1 psubx = r * arg1 - arg0 result = r + (z3.If(arg1 < 0, psubx, -psubx) >> (INTEGER_WIDTH - 1)) elif opname == "int_pymod": valid_if = arg1 != 0 r = arg0 % arg1 result = r + (arg1 & z3.If(arg1 < 0, -r, r) >> (INTEGER_WIDTH - 1)) elif opname == "int_is_true": result = cond(arg0 != FALSEBV) elif opname == "int_is_zero": result = cond(arg0 == FALSEBV) elif opname == "int_neg": result = -arg0 elif opname == "int_invert": result = ~arg0 else: assert 0, "unknown operation " + opname return result, valid_if def cond(z3expr): """ helper function to turn a Z3 boolean result z3expr into a 1 or 0 bitvector, using z3.If """ return z3.If(z3expr, TRUEBV, FALSEBV)

We map the semantics of a PyPy JIT operation to Z3 with the z3_expression function. It takes the name of a JIT operation and its two (or one) arguments into a pair of Z3 formulas, result and valid_if. The resulting formulas are constructed with the operator overloading of Z3 variables/formulas.

The first element result of the result of z3_expression represents the result of performing the operation. valid_if is a bool that represents a condition that needs to be True in order for the result of the operation to be defined. E.g. int_pydiv(a, b) is only valid if b != 0. Most operations are always valid, so they return True as that condition (we'll ignore valid_if for a bit, but it will become more relevant further down in the post).

We can define a helper function to prove things by finding counterexamples:

def prove(cond): """ Try to prove a condition cond by searching for counterexamples of its negation. """ z3res = solver.check(z3.Not(cond)) if z3res == z3.unsat: return True elif z3res == z3.unknown: # eg on timeout return False elif z3res == z3.sat: return False assert 0, "should be unreachable" Finding rewrite rules

Now we can start finding our first rewrite rules, following the first pattern op(x, x) -> x. We do this by iterating over all the supported binary operation names, getting the z3 expression for op(x, x) and then asking Z3 to prove op(x, x) == x.

for opname in opnames2: result, valid_if = z3_expression(opname, xvar, xvar) if prove(result == xvar): print(f"{opname}(x, x) -> x, {result}")

This yields the simplifications:

int_and(x, x) -> x int_or(x, x) -> x Synthesizing constants

Supporting the next patterns is harder: op(x, x) == c1, op(x, c1) == x, and op(x, c1) == x. We don't know which constants to pick to try to get Z3 to prove the equality. We could iterate over common constants like 0, 1, MAXINT, etc, or even over all the 256 values for a bitvector of length 8. However, we will instead ask Z3 to find the constants for us too.

This can be done by using quantifiers, in this case z3.ForAll. The query we pose to Z3 is "does there exist a constant c1 such that for all x the following is true: op(x, c1) == x? Note that the constant c1 is not necessarily unique, there could be many of them. We generate several matching constant, and add that they must be different to the condition of the second and further queries.

We can express this in a helper function:

def find_constant(z3expr, number_of_results=5): condition = z3.ForAll( [xvar], z3expr ) for i in range(number_of_results): checkres = solver.check(condition) if checkres == z3.sat: # if a solver check succeeds, we can ask for a model, which is # concrete values for the variables constvar model = solver.model() const = model[constvar].as_signed_long() yield const # make sure we don't generate the same constant again on the # next call condition = z3.And(constvar != const, condition) else: # no (more) constants found break

We can use this new function for the three mentioned patterns:

# try to find constants for op(x, x) == c for opname in opnames2: result, valid_if = z3_expression(opname, xvar, xvar) for const in find_constant(result == constvar): print(f"{opname}(x, x) -> {const}") # try to find constants for op(x, c) == x and op(c, x) == x for opname in opnames2: result, valid_if = z3_expression(opname, xvar, constvar) for const in find_constant(result == xvar): print(f"{opname}(x, {const}) -> x") result, valid_if = z3_expression(opname, constvar, xvar) for const in find_constant(result == xvar): print(f"{opname}({const}, x) -> x") # this code is not quite correct, we'll correct it later

Together this yields the following new simplifications:

# careful, these are not all correct! int_sub(x, x) -> 0 int_xor(x, x) -> 0 int_eq(x, x) -> 1 int_ne(x, x) -> 0 int_lt(x, x) -> 0 int_le(x, x) -> 1 int_gt(x, x) -> 0 int_ge(x, x) -> 1 uint_lt(x, x) -> 0 uint_le(x, x) -> 1 uint_gt(x, x) -> 0 uint_ge(x, x) -> 1 uint_rshift(x, x) -> 0 int_pymod(x, x) -> 0 int_add(x, 0) -> x int_add(0, x) -> x int_sub(x, 0) -> x int_mul(x, 1) -> x int_mul(1, x) -> x int_and(x, -1) -> x int_and(-1, x) -> x int_or(x, 0) -> x int_or(0, x) -> x int_xor(x, 0) -> x int_xor(0, x) -> x int_lshift(x, 0) -> x int_rshift(x, 0) -> x uint_rshift(x, 0) -> x int_pydiv(x, 1) -> x int_pymod(x, 0) -> x

Most of these look good at first glance, but the last one reveals a problem: we've been ignoring the valid_if expression up to now. We can stop doing that by changing the code like this, which adds z3.And(valid_if, ...) to the argument of the calls to find_constant:

# try to find constants for op(x, x) == c, op(x, c) == x and op(c, x) == x for opname in opnames2: result, valid_if = z3_expression(opname, xvar, xvar) for const in find_constant(z3.And(valid_if, result == constvar)): print(f"{opname}(x, x) -> {const}") # try to find constants for op(x, c) == x and op(c, x) == x for opname in opnames2: result, valid_if = z3_expression(opname, xvar, constvar) for const in find_constant(z3.And(result == xvar, valid_if)): print(f"{opname}(x, {const}) -> x") result, valid_if = z3_expression(opname, constvar, xvar) for const in find_constant(z3.And(result == xvar, valid_if)): print(f"{opname}({const}, x) -> x")

And we get this list instead:

int_sub(x, x) -> 0 int_xor(x, x) -> 0 int_eq(x, x) -> 1 int_ne(x, x) -> 0 int_lt(x, x) -> 0 int_le(x, x) -> 1 int_gt(x, x) -> 0 int_ge(x, x) -> 1 uint_lt(x, x) -> 0 uint_le(x, x) -> 1 uint_gt(x, x) -> 0 uint_ge(x, x) -> 1 int_add(x, 0) -> x int_add(0, x) -> x int_sub(x, 0) -> x int_mul(x, 1) -> x int_mul(1, x) -> x int_and(x, -1) -> x int_and(-1, x) -> x int_or(x, 0) -> x int_or(0, x) -> x int_xor(x, 0) -> x int_xor(0, x) -> x int_lshift(x, 0) -> x int_rshift(x, 0) -> x uint_rshift(x, 0) -> x int_pydiv(x, 1) -> x Synthesizing two constants

For the patterns op(x, c1) == c2 and op(c1, x) == c2 we need to synthesize two constants. We can again write a helper method for that:

def find_2consts(z3expr, number_of_results=5): condition = z3.ForAll( [xvar], z3expr ) for i in range(number_of_results): checkres = solver.check(condition) if checkres == z3.sat: model = solver.model() const = model[constvar].as_signed_long() const2 = model[constvar2].as_signed_long() yield const, const2 condition = z3.And(z3.Or(constvar != const, constvar2 != const2), condition) else: return

And then use it like this:

for opname in opnames2: # try to find constants c1, c2 such that op(c1, x) -> c2 result, valid_if = z3_expression(opname, constvar, xvar) consts = find_2consts(z3.And(valid_if, result == constvar2)) for const, const2 in consts: print(f"{opname}({const}, x) -> {const2}") # try to find constants c1, c2 such that op(x, c1) -> c2 result, valid_if = z3_expression(opname, xvar, constvar) consts = find_2consts(z3.And(valid_if, result == constvar2)) for const, const2 in consts: print("%s(x, %s) -> %s" % (opname, const, const2))

Which yields some straightforward simplifications:

int_mul(0, x) -> 0 int_mul(x, 0) -> 0 int_and(0, x) -> 0 int_and(x, 0) -> 0 uint_lt(x, 0) -> 0 uint_le(0, x) -> 1 uint_gt(0, x) -> 0 uint_ge(x, 0) -> 1 int_lshift(0, x) -> 0 int_rshift(0, x) -> 0 uint_rshift(0, x) -> 0 uint_mul_high(0, x) -> 0 uint_mul_high(1, x) -> 0 uint_mul_high(x, 0) -> 0 uint_mul_high(x, 1) -> 0 int_pymod(x, 1) -> 0 int_pymod(x, -1) -> 0

A few require a bit more thinking:

int_or(-1, x) -> -1 int_or(x, -1) -> -1

The are true because in two's complement, -1 has all bits set.

The following ones require recognizing that -9223372036854775808 == -2**63 is the most negative signed 64-bit integer, and 9223372036854775807 == 2 ** 63 - 1 is the most positive one:

int_lt(9223372036854775807, x) -> 0 int_lt(x, -9223372036854775808) -> 0 int_le(-9223372036854775808, x) -> 1 int_le(x, 9223372036854775807) -> 1 int_gt(-9223372036854775808, x) -> 0 int_gt(x, 9223372036854775807) -> 0 int_ge(9223372036854775807, x) -> 1 int_ge(x, -9223372036854775808) -> 1

The following ones are true because the bitpattern for -1 is the largest unsigned number:

uint_lt(-1, x) -> 0 uint_le(x, -1) -> 1 uint_gt(x, -1) -> 0 uint_ge(-1, x) -> 1 Strength Reductions

All the patterns so far only had a variable or a constant on the target of the rewrite. We can also use the machinery to do strengh-reductions where we generate a single-argument operation op1(x) for input operations op(x, c1) or op(c1, x). To achieve this, we try all combinations of binary and unary operations. (We won't consider strength reductions where a binary operation gets turned into a "cheaper" other binary operation here.)

opnames1 = [ "int_is_true", "int_is_zero", "int_neg", "int_invert", ] for opname in opnames2: for opname1 in opnames1: result, valid_if = z3_expression(opname, xvar, constvar) # try to find a constant op(x, c) == g(x) result1, valid_if1 = z3_expression(opname1, xvar) consts = find_constant(z3.And(valid_if, valid_if1, result == result1)) for const in consts: print(f"{opname}(x, {const}) -> {opname1}(x)") # try to find a constant op(c, x) == g(x) result, valid_if = z3_expression(opname, constvar, xvar) result1, valid_if1 = z3_expression(opname1, xvar) consts = find_constant(z3.And(valid_if, valid_if1, result == result1)) for const in consts: print(f"{opname}({const}, x) -> {opname1}(x)")

Which yields the following new simplifications:

int_sub(0, x) -> int_neg(x) int_sub(-1, x) -> int_invert(x) int_mul(x, -1) -> int_neg(x) int_mul(-1, x) -> int_neg(x) int_xor(x, -1) -> int_invert(x) int_xor(-1, x) -> int_invert(x) int_eq(x, 0) -> int_is_zero(x) int_eq(0, x) -> int_is_zero(x) int_ne(x, 0) -> int_is_true(x) int_ne(0, x) -> int_is_true(x) uint_lt(0, x) -> int_is_true(x) uint_lt(x, 1) -> int_is_zero(x) uint_le(1, x) -> int_is_true(x) uint_le(x, 0) -> int_is_zero(x) uint_gt(x, 0) -> int_is_true(x) uint_gt(1, x) -> int_is_zero(x) uint_ge(x, 1) -> int_is_true(x) uint_ge(0, x) -> int_is_zero(x) int_pydiv(x, -1) -> int_neg(x) Conclusions

With not very little code we managed to generate a whole lot of local simplifications for integer operations in the IR of PyPy's JIT. The rules discovered that way are "simple", in the sense that they only require looking at a single instruction, and not where the arguments of that instruction came from. They also don't require any knowledge about the properties of the arguments of the instructions (e.g. that they are positive).

The rewrites in this post have mostly been in PyPy's JIT already. But now we mechanically confirmed that they are correct. I've also added the remaining useful looking ones, in particular int_eq(x, 0) -> int_is_zero(x) etc.

If we wanted to scale this approach up, we would have to work much harder! There are a bunch of problems that come with generalizing the approach to looking at sequences of instructions:

• Combinatorial explosion: if we look at sequences of instructions, we very quickly get a combinatorial explosion and it becomes untractable to try all combinations.

• Finding non-minimal patterns: Some complicated simplifications can be instances of simpler ones. For example, because int_add(x, 0) -> x, it's also true that int_add(int_sub(x, y), 0) -> int_sub(x, y). If we simply generate all possible sequences, we will find the latter simplification rule, which we would usually not care about.

• Unclear usefulness: if we simply generate all rewrites up to a certain number of instructions, we will get a lot of patterns that are useless in the sense that they typically aren't found in realistic programs. It would be much better to somehow focus on the patterns that real benchmarks are using.

In the next blog post I'll discuss an alternative approach to simply generating all possible sequences of instructions, that tries to address these problems. This works by analyzing the real traces of benchmarks and mining those for inefficiencies, which only shows problems that occur in actual programs.

Sources

I've been re-reading a lot of blog posts from John's blog:

• Let’s Work on an LLVM Superoptimizer
• Early Superoptimizer Results
• A Few Synthesizing Superoptimizer Results
• Synthesizing Constants

but also papers:

• A Synthesizing Superoptimizer
• Hydra: Generalizing Peephole Optimizations with Program Synthesis

Another of my favorite blogs has been Philipp Zucker's blog in the last year or two, lots of excellent posts about/using Z3 on there.

Lists are used to store and manipulate an ordered collection of things.

Table of contents

1. Lists are ordered collections
2. Containment checking
3. Length
4. Modifying the contents of a list
5. Indexing: looking up items by their position
6. Lists are the first data structure to learn

Lists are ordered collections

This is a list:

>>> colors = ["purple", "green", "blue", "yellow"]

We can prove that to ourselves by passing that object to Python's built-in type function:

>>> type(colors) <class 'list'>

Lists are ordered collections of things.

We can create a new list by using square brackets ([]), and inside those square brackets, we put each of the items that we'd like our list to contain, separated by commas:

>>> numbers = [2, 1, 3, 4, 7, 11] >>> numbers [2, 1, 3, 4, 7, 11]

Lists can contain any type of object. Each item in a list doesn't need to be of the same type, but in practice, they typically are.

So we might refer to this as a list of strings:

>>> colors = ["purple", "green", "blue", "yellow"]

While this is a list of numbers:

>>> numbers = [2, 1, 3, 4, 7, 11] Containment checking

We can check whether a …

Read the full article: https://www.pythonmorsels.com/what-are-lists/

Starting at 4°C, add +12 to the Celcius and mirror the number to get the Fahrenheit number.

We are thrilled to announce that our first-ever search for a dedicated PyPI Support Specialist has concluded with the hire of Maria Ashna, the newest member of the Python Software Foundation (PSF) staff. Reporting to Ee Durbin, Director of Infrastructure, Maria joins us from a background in academic research, technical consulting, and theatre.

Maria will help the PSF to support one of our most critical services, the Python Package Index (PyPI). Over the past 23 years, PyPI has seen essentially exponential growth in traffic and users, relying for the most part on volunteers to support it. With the addition of requirements to keep all Python maintainers and users safe, our support load has outstretched our support resources for some time now. The Python Software Foundation committed to hiring to increase this capacity in April and we’re excited to have Maria on board to begin providing crucially needed support.

From Maria, “I am a firm believer in democratizing tech. The Open Source community is the lifeblood of such democratization, which is why I am excited to be part of PSF and to serve this community.”

As you see Maria around the PyPI support inbox, issue tracker, and discuss.python.org in the future we hope that you’ll extend a warm welcome! We’re eager to get her up and running to reduce the stress that users have been experiencing around PyPI support and further our work to improve and extend PyPI sustainably.

Have you wondered about graph theory and how to start exploring it in Python? What resources and Python libraries can you use to experiment and learn more? This week on the show, former co-host David Amos returns to talk about what he's been up to and share his knowledge about graph theory in Python.

[ Improve Your Python With 🐍 Python Tricks 💌 – Get a short & sweet Python Trick delivered to your inbox every couple of days. >> Click here to learn more and see examples ]

Python is special. It's used by the big tech companies but also by those you would rarely classify as developers. On this episode, we get a look inside how Python is being used at a Children's Hospital to speed and improve patient care. We have Dr. Somak Roy here to share how he's using Python in his day to day job to help kids get well a little bit faster.<br/> <br/> <strong>Episode sponsors</strong><br/> <br/> <a href='https://talkpython.fm/sentry'>Sentry Error Monitoring, Code TALKPYTHON</a><br> <a href='https://talkpython.fm/posit'>Posit</a><br> <a href='https://talkpython.fm/training'>Talk Python Courses</a><br/> <br/> <strong>Links from the show</strong><br/> <br/> <div><b>Somak Roy</b>: <a href="https://www.linkedin.com/in/somak-roy-1034bb48/" target="_blank" rel="noopener">linkedin.com</a><br/> <b>Cincinnati Children's Hospital</b>: <a href="https://www.cincinnatichildrens.org" target="_blank" rel="noopener">cincinnatichildrens.org</a><br/> <b>CNVkit: Genome-wide copy number</b>: <a href="https://cnvkit.readthedocs.io/en/stable/" target="_blank" rel="noopener">readthedocs.io</a><br/> <b>cnaplotr</b>: <a href="https://github.com/roysomak4/cnaplotr" target="_blank" rel="noopener">github.com</a><br/> <b>hgvs</b>: <a href="https://hgvs.readthedocs.io/en/stable/" target="_blank" rel="noopener">readthedocs.io</a><br/> <b>openpyxl</b>: <a href="https://openpyxl.readthedocs.io/en/stable/" target="_blank" rel="noopener">readthedocs.io</a><br/> <b>Hera is an Argo Python SDK</b>: <a href="https://github.com/argoproj-labs/hera" target="_blank" rel="noopener">github.com</a><br/> <b>insiM: in silico Mutator software for bioinformatics</b>: <a href="https://github.com/thesushantpatil/insiM" target="_blank" rel="noopener">github.com</a><br/> <b>Bamsurgeon</b>: <a href="https://github.com/adamewing/bamsurgeon" target="_blank" rel="noopener">github.com</a><br/> <b>pysam - An interface for reading and writing SAM files</b>: <a href="https://niyunyun-pysam-fork.readthedocs.io/en/latest/api.html" target="_blank" rel="noopener">readthedocs.io</a><br/> <b>Scientists rename human genes to stop Microsoft Excel from misreading them as dates</b>: <a href="https://www.theverge.com/2020/8/6/21355674/human-genes-rename-microsoft-excel-misreading-dates" target="_blank" rel="noopener">theverge.com</a><br/> <b>BioPython</b>: <a href="https://biopython.org" target="_blank" rel="noopener">biopython.org</a><br/> <b>Watch this episode on YouTube</b>: <a href="https://www.youtube.com/watch?v=L6AAOmob07o" target="_blank" rel="noopener">youtube.com</a><br/> <b>Episode transcripts</b>: <a href="https://talkpython.fm/episodes/transcript/470/python-in-medicine-and-patient-care" target="_blank" rel="noopener">talkpython.fm</a><br/> <br/> <b>--- Stay in touch with us ---</b><br/> <b>Subscribe to us on YouTube</b>: <a href="https://talkpython.fm/youtube" target="_blank" rel="noopener">youtube.com</a><br/> <b>Follow Talk Python on Mastodon</b>: <a href="https://fosstodon.org/web/@talkpython" target="_blank" rel="noopener"><i class="fa-brands fa-mastodon"></i>talkpython</a><br/> <b>Follow Michael on Mastodon</b>: <a href="https://fosstodon.org/web/@mkennedy" target="_blank" rel="noopener"><i class="fa-brands fa-mastodon"></i>mkennedy</a><br/></div>

In this episode, we worked on a trial banner that could persist across all pages on the site. Because the banner needed data that was only available on the index page, we had to refactor the banner into an inclusion template tag to make the tag work consistently.

An overview of the ongoing efforts to improve and roll out support for free-threaded CPython throughout the Python open source ecosystem

We are excited to announce that Jacob Coffee has joined the Python Software Foundation staff as an Infrastructure Engineer bringing his experience as an Open Source maintainer, dedicated homelab maintainer, and professional systems administrator to the team. Jacob will be the second member of our Infrastructure staff, reporting to Director of Infrastructure, Ee Durbin.

Joining our team, Jacob will share the responsibility of maintaining the PSF systems and services that serve the Python community, CPython development, and our internal operations. This will add crucially needed redundancy to the team as well as capacity to undertake new initiatives with our infrastructure.

Jacob shares, “I’m living the dream by supporting the PSF mission AND working in open source! I’m thrilled to be a part of the PSF team and deepen my contributions to the Python community.”

In just the first few days, Jacob has already shown initiative on multiple projects and issues throughout the infrastructure and we’re excited to see the impact he’ll have on the PSF and broader Python community. We hope that you’ll wish him a warm welcome as you see him across the repos, issue trackers, mailing lists, and discussion forums!