embrace uv (#422)

.devcontainer/postCreate.sh

@@ -1,8 +1,7 @@
 #!/bin/bash
 python -m venv .venv
 source .venv/bin/activate
-python -m pip install -e .
-python -m pip install -r requirements-dev.txt
+python -m pip install -e .[dev]
 pre-commit install
 pre-commit run --all-files
 

.github/workflows/test.yml

@@ -40,18 +40,18 @@ jobs:
       - name: Install foundry
         uses: foundry-rs/foundry-toolchain@v1
 
-      - name: Set up python ${{ matrix.python-version }}
-        uses: actions/setup-python@v5
+      - name: Install uv
+        uses: astral-sh/setup-uv@v4
         with:
-          python-version: ${{ matrix.python-version }}
+          # Install a specific version of uv.
+          version: "0.5.6"
 
-      - name: Install dependencies
-        run: |
-          python -m pip install --upgrade pip
-          python -m pip install -r requirements-dev.txt
+      - name: Set up python ${{ matrix.python-version }}
+        run: uv python install ${{ matrix.python-version }}
 
-      - name: Install halmos
-        run: python -m pip install -e .
+      - name: Install halmos and its dependencies
+        run: |
+          uv sync --extra dev
 
       - name: Run pytest
-        run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-st --disable-gc --solver-threads 1 --storage-layout ${{ matrix.storage-layout }} ${{ matrix.cache-solver }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }}
+        run: uv run pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-st --disable-gc --solver-threads 1 --storage-layout ${{ matrix.storage-layout }} ${{ matrix.cache-solver }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }}

.gitignore

@@ -24,3 +24,10 @@ out/
 
 # VS Code
 .vscode/
+
+# https://docs.astral.sh/uv/concepts/projects/layout/#the-lockfile
+# we go against the recommended best practice and don't add it to source control:
+# - adds too much noise
+# - adds friction to CI
+# (at the cost of reproducible builds)
+uv.lock

.pre-commit-config.yaml

@@ -1,13 +1,4 @@
 repos:
-  # - repo: https://github.com/psf/black
-  #   rev: 23.7.0
-  #   hooks:
-  #     - id: black
-  #       # It is recommended to specify the latest version of Python
-  #       # supported by your project here, or alternatively use
-  #       # pre-commit's default_language_version, see
-  #       # https://pre-commit.com/#top_level-default_language_version
-  #       language_version: python3.12
 
 - repo: https://github.com/astral-sh/ruff-pre-commit
   # Ruff version.

CONTRIBUTING.md

@@ -8,50 +8,81 @@ Join the [Halmos Telegram Group][chat] for any inquiries or further discussions.
 
 ## Development Setup
 
-If you want to submit a pull request, fork the repository:
+Clone or fork the repository:
 
 ```sh
+# if you want to submit a pull request, fork the repository:
 gh repo fork a16z/halmos
-```
-
-Or, if you just want to develop locally, clone it:
 
-```sh
+# Or, if you just want to develop locally, clone it:
 git clone [email protected]:a16z/halmos.git
+
+# navigate to the project directory
+cd halmos
 ```
 
-Create and activate a virtual environment:
+**Recommended**: set up the development environment using [uv](https://docs.astral.sh/uv/):
 
 ```sh
-python3.12 -m venv .venv && source .venv/bin/activate
-```
+# install uv
+curl -LsSf https://astral.sh/uv/install.sh | sh
 
-Install the dependencies:
+# this does a lot of things:
+# - install a suitable python version if one is not found
+# - create a virtual environment in `.venv`
+# - install the main dependencies
+# - install the development dependencies
+# - generates a `uv.lock` file
+uv sync --extra dev
 
-```sh
-# install halmos and its runtime dependencies
-python -m pip install -e .
+# install and run the pre-commit hooks
+uv run pre-commit install
+uv run pre-commit run --all-files
+
+# make changes to halmos, then run it with:
+uv run halmos
 
-# install the dev dependencies
-python -m pip install -r requirements-dev.txt
+# run the tests with:
+uv run pytest
+
+# add a dependency to the project:
+uv add <dependency>
+
+# remove a dependency from the project:
+uv remove <dependency>
+
+# update a dependency to the latest version:
+uv lock --upgrade-package <dependency>
+
+# to manually update the environment and activate it:
+uv sync
+source .venv/bin/activate
 ```
 
-Install and run the git hook scripts (this is optional but will make sure that your PR will follow the style convention):
+Alternatively, you can manage the python version and the virtual environment manually using `pip` (not recommended for most users):
 
 ```sh
+# create and activate a virtual environment with a suitable python version
+python3.12 -m venv .venv && source .venv/bin/activate
+
+# install halmos and its runtime dependencies in editable mode
+python -m pip install -e ".[dev]"
+
+# install and run the pre-commit hooks
 pre-commit install
 pre-commit run --all-files
 ```
 
+
 ## Coding Style
 
-We recommend enabling the [black] formatter in your editor, but you can run it manually if needed:
+We recommend enabling the [ruff] formatter in your editor, but you can run it manually if needed:
 
 ```sh
-python -m black src/
+python -m ruff check src/
 ```
 
-[black]: <https://black.readthedocs.io/en/stable/>
+[ruff]: <https://docs.astral.sh/ruff/>
 
 ## GitHub Codespace
 

README.md

@@ -23,39 +23,58 @@ Join the [Halmos Telegram Group][chat] for any inquiries or further discussions.
 
 ## Installation
 
+### ⭐ Using `uv` (recommended for most users)
+
 ```sh
-pip install halmos
+# install uv if you don't have it already
+curl -LsSf https://astral.sh/uv/install.sh | sh
+
+# install the latest version of halmos for the current user and add it to PATH
+uv tool install halmos
+
+# or, install the development version from the repository
+# uv tool install git+https://github.com/a16z/halmos
+
+# after installing, you can update halmos to the latest version with:
+uv tool upgrade halmos
 ```
 
-Or, if you want to try out the nightly build version:
+### Using `docker`
+
+You can download a pre-built Docker image that contains python, halmos, its dependencies, foundry, solvers, etc.:
 
 ```sh
-pip install git+https://github.com/a16z/halmos
+docker pull ghcr.io/a16z/halmos:latest
 ```
 
-Alternatively, you can download the Docker image that contains halmos and its dependencies:
+### Using `pip` (for advanced users)
+
+Note: this is not recommended because of the extra work required to manage the python version and the virtual environment. But if you know what you are doing, and need the extra control, you can do it like this:
 
 ```sh
-docker pull .:/workspace ghcr.io/a16z/halmos:0.1.14
-```
+# make sure you have a suitable python version installed, e.g.:
+python3.12 --version
 
-And finally, if you want to install halmos into an isolated virtual environment (so you don't have to deal with dependency issues), you can install it with [uv](https://docs.astral.sh/uv/getting-started/installation/):
+# create and activate a virtual environment with an explicit python version
+python3.12 -m venv .venv && source .venv/bin/activate
 
-```
-curl -LsSf https://astral.sh/uv/install.sh | sh # install UV (see docs for other install methods)
-uv tool install halmos
+# install the latest version of halmos
+pip install halmos
+
+# or, install the development version from the repository
+pip install git+https://github.com/a16z/halmos
 ```
 
 ## Usage
 
-```
+```sh
 cd /path/to/src
 halmos
 ```
 
 For more details:
 
-```
+```sh
 halmos --help
 ```
 
@@ -65,14 +84,14 @@ Alternatively, you can run the latest halmos Docker image available at [ghcr.io/
 cd /path/to/src
 
 # mount '.' under /workspace in the container
-docker run -v .:/workspace ghcr.io/a16z/halmos:0.1.14
+docker run -v .:/workspace ghcr.io/a16z/halmos:latest
 ```
 
-## Examples
+## Getting Started
 
 Refer to the [getting started guide](docs/getting-started.md) and the [examples](examples/README.md) directory.
 
-## Contributing
+## Contributing / Developing
 
 Refer to the [contributing guidelines](CONTRIBUTING.md), and explore the list of issues labeled ["good first issue" or "help wanted."][issues]
 

docs/getting-started.md

@@ -8,34 +8,11 @@ Symbolic tests looks similar to fuzz tests, but there are certain differences th
 
 ## 0. Install Halmos
 
-Halmos is available as a [Python package][Halmos Package], and can be installed using `pip`:
-```
-pip install halmos
-```
-
-[Halmos Package]: <https://pypi.org/project/halmos/>
-
-**Tips:**
-
-- If you want to try out the nightly build version, you can install it from the Github repository:
-  ```
-  pip install git+https://github.com/a16z/halmos
-  ```
+If you haven't installed Halmos yet, please refer to the [installation guide](../README.md#installation) or quickly install it with:
 
-- If you're not familiar with managing Python packages, we recommend using `venv`. Create a virtual environment and install Halmos within it:
-  ```
-  python3 -m venv <venv-dir>
-  source <venv-dir>/bin/activate
-  pip install halmos
-  ```
-  You can activate or deactivate the virtual environment before or after using Halmos:
-  ```
-  # to activate:
-  source <venv-dir>/bin/activate
-
-  # to deactivate:
-  deactivate
-  ```
+```sh
+uv tool install halmos
+```
 
 ## 1. Write setUp()
 

packages/halmos/Dockerfile

@@ -1,19 +1,36 @@
 FROM ghcr.io/a16z/halmos-builder:latest
 
-# Enable the virtual environment
-ENV PATH="/halmos/.venv/bin:$PATH"
-ENV VIRTUAL_ENV='/halmos/.venv'
+# inspired by https://hynek.me/articles/docker-uv/
 
-# Install halmos, assuming it is checked out in the context directory
-WORKDIR /halmos
+# - enable the virtual environment
+# - install halmos and its dependencies in UV_PROJECT_ENVIRONMENT
+# - enable bytecode compilation for faster startup
+# - disable downloading any additional packages
+# - use copy mode for linking instead of symlinking (because we mount to /src temporarily)
+ENV PATH="/halmos/bin:$PATH" \
+    VIRTUAL_ENV='/halmos' \
+    UV_PROJECT_ENVIRONMENT='/halmos' \
+    UV_COMPILE_BYTECODE=1 \
+    UV_PYTHON=python3.13 \
+    UV_PYTHON_DOWNLOADS=never \
+    UV_LINK_MODE=copy
+
+# Install halmos, assuming it is checked out in the current host directory
+# we don't specify --frozen or --locked because we don't check in uv.lock
 RUN --mount=type=bind,source=../..,target=/src,readonly=false \
-    uv venv && \
-    uv pip install --no-cache /src && \
-    uv pip install --no-cache -r /src/requirements-dev.txt
+    cd /src && \
+    uv sync --extra dev --no-editable
 
 # Set a nicer prompt
 ENV IMAGE_NAME=halmos
 RUN echo 'PS1="($IMAGE_NAME) \[\033[1;32m\]\u@\h \[\033[1;35m\]\w \$\[\033[0m\] "' >> /root/.bashrc
 
+# optional: print python version, site packages, and check that halmos can be imported
+RUN <<EOT
+python -V
+python -Im site
+python -Ic 'import halmos'
+EOT
+
 WORKDIR /workspace
 CMD ["halmos"]

pyproject.toml

@@ -36,8 +36,17 @@ halmos = "halmos.__main__:main"
 [project.urls]
 "Homepage" = "https://github.com/a16z/halmos"
 
-[tool.black]
-target-version = ["py311", "py312"]
+# development dependencies, can be installed with
+#   uv sync --extra dev
+# or
+#   pip install -e ".[dev]"
+# (see CONTRIBUTING.md for more details)
+[project.optional-dependencies]
+dev = [
+    "pre-commit>=4.0.1",
+    "pytest>=8.3.4",
+    "ruff>=0.8.1",
+]
 
 [tool.pytest.ini_options]
 # TODO: re-add test_traces.py when we have a better way to support it in CI