An application that glibly searches for RH counterexamples, while also teaching software engineering principles.
Blog posts:
- Setting up Pytest
- Adding a Database
- Search Strategies
- Unbounded Integers
- Deploying with Docker
- Performance Profiling
- Scaling Up
- Productionizing
- Exploring data
Requires Python 3.7 and
On Mac OS X these can be installed via brew as follows
brew install gmp mpfr libmpc postgresql
Or using apt
apt install -y libgmp3-dev libmpfr-dev libmpc-dev postgresql-12
Then, in a virtualenv,
pip install -r requrements.txt
For postgres, create a new database cluster and start the server.
initdb --locale=C -E UTF-8 /usr/local/var/postgres
pg_ctl -D /usr/local/var/postgres -l /tmp/logfile start
Then create a database like
CREATE DATABASE divisor
WITH OWNER = jeremy; -- or whatever your username is
Then install the pgmp extension using pgxn
sudo pip install pgxnclient
pgxn install pgmp
pgxn load -d divisor pgmp
Note you may need to add the location of gmp.h
to $C_INCLUDE_PATH
so that the build step for pgmp
can find it.
This appears to be a problem mostly on Mac OSX.
See dvarrazzo/pgmp#4 if you run into issues.
# your version may be different than 6.2.0. Find it by running
# brew info gmp
export C_INCLUDE_PATH="/usr/local/Cellar/gmp/6.2.0/include:$C_INCLUDE_PATH"
In this case, you may also want to build pgmp from source,
git clone https://github.com/j2kun/pgmp && cd pgmp
make
sudo make install
Run some combination of the following three worker jobs
python -m riemann.generate_search_blocks
python -m riemann.process_search_blocks
python -m riemann.cleanup_stale_blocks
Running with docker removes the need to install postgres and dependencies.
docker build -t divisordb -f docker/divisordb.Dockerfile .
docker build -t generate -f docker/generate.Dockerfile .
docker build -t process -f docker/process.Dockerfile .
docker build -t cleanup -f docker/cleanup.Dockerfile .
docker volume create pgdata
docker run -d --name divisordb -p 5432:5432 -v pgdata:/var/lib/postgresql/data divisordb:latest
export PGHOST=$(docker inspect -f "{{ .NetworkSettings.IPAddress }}" divisordb)
docker run -d --name generate --env PGHOST="$PGHOST" generate:latest
docker run -d --name cleanup --env PGHOST="$PGHOST" cleanup:latest
docker run -d --name process --env PGHOST="$PGHOST" process:latest
After the divisordb
container is up, you can test whether it's working by
pg_isready -d divisor -h $PGHOST -p 5432 -U docker
or by going into the container and checking the database manually
$ docker exec -it divisordb /bin/bash
# now inside the container
$ psql
divisor=# \d # \d is postgres for 'describe tables'
List of relations
Schema | Name | Type | Owner
--------+--------------------+-------+--------
public | riemanndivisorsums | table | docker
public | searchmetadata | table | docker
(2 rows)
# install docker, see get.docker.com
curl -fsSL https://get.docker.com -o get-docker.sh
sudo sh get-docker.sh
sudo usermod -aG docker ubuntu
# log out and log back in
git clone https://github.com/j2kun/riemann-divisor-sum && cd riemann-divisor-sum
Fill out the environment variables from .env.template
in .env
,
then run python deploy.py
.
This will only work if the application has been set up initially (docker installed and the repository cloned).
sudo apt install -y python3-pip ssmtp
pip3 install -r alerts/requirements.txt
sudo -E alerts/configure_ssmtp.sh
nohup python3 -m alerts.monitor_docker &
python -m riemann.export_for_plotting --data_source_name='dbname=divisor' --divisor_sums_filepath=divisor_sums.csv
# sort the csv by log_n using gnu sort
sort -t , -n -k 1 divisor_sums.csv -o divisor_sums_sorted.csv
# convert to hdf5
python -c "import vaex; vaex.from_csv('divisor_sums.csv', convert=True, chunk_size=5_000_000)"
python -m plot.plot_divisor_sums --divisor_sums_hdf5_path=divisor_sums.hdf5