diff --git a/.devcontainer/postCreate.sh b/.devcontainer/postCreate.sh index 7d8af157..85a31ea8 100644 --- a/.devcontainer/postCreate.sh +++ b/.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 diff --git a/.github/workflows/black.yml b/.github/workflows/black.yml deleted file mode 100644 index ecb791a3..00000000 --- a/.github/workflows/black.yml +++ /dev/null @@ -1,11 +0,0 @@ -# Deprecated: use pre-commit instead -# name: Lint - -# on: [push, pull_request] - -# jobs: -# lint: -# runs-on: ubuntu-latest -# steps: -# - uses: actions/checkout@v4 -# - uses: psf/black@stable diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 729514e4..6937c605 100644 --- a/.github/workflows/test.yml +++ b/.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 }} diff --git a/.gitignore b/.gitignore index b7579872..2f368a47 100644 --- a/.gitignore +++ b/.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 diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 7dc2cb79..22bd3799 100644 --- a/.pre-commit-config.yaml +++ b/.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. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 47815608..4c385ca9 100644 --- a/CONTRIBUTING.md +++ b/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 git@github.com: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 + +# remove a dependency from the project: +uv remove + +# update a dependency to the latest version: +uv lock --upgrade-package + +# 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]: +[ruff]: ## GitHub Codespace diff --git a/README.md b/README.md index 168311b6..6820b5f0 100644 --- a/README.md +++ b/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] diff --git a/docs/getting-started.md b/docs/getting-started.md index c3ca1534..4fa2cd32 100644 --- a/docs/getting-started.md +++ b/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]: - -**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 - source /bin/activate - pip install halmos - ``` - You can activate or deactivate the virtual environment before or after using Halmos: - ``` - # to activate: - source /bin/activate - - # to deactivate: - deactivate - ``` +```sh +uv tool install halmos +``` ## 1. Write setUp() diff --git a/packages/halmos/Dockerfile b/packages/halmos/Dockerfile index 4a1deaa9..1a26a55d 100644 --- a/packages/halmos/Dockerfile +++ b/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 <=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 diff --git a/requirements-dev.txt b/requirements-dev.txt deleted file mode 100644 index 30544ac2..00000000 --- a/requirements-dev.txt +++ /dev/null @@ -1,3 +0,0 @@ -black -pre-commit -pytest