Add infrastructure for packaging and distributing maraboupy

[wenkokke]

This PR creates a Python package for maraboupy and adds GitHub Actions infrastructure for building wheels for various platforms, architectures, and Python versions.

Version

PyPI packages require a version. Unfortunately, Marabou's version (1.0) has not changed in the past four years, and the project does not tag releases (see #626).

I've chosen to use a lightweight CalVer versioning scheme, following YYYY.BUILD, meaning the version is the current year followed by the build number, with some peculiarities to maintain a lexicographical order. For instance, the current version is v2023.1001. BumpVer is configured so that the version number can easily be updated by running bumpver update, which adjusts the year if necessary, bumps the build number, and commits & pushes a Git tag. (BumpVer is configured in pyproject.toml.)

There is no relation between the version of maraboupy as I've configured it, and the version of Marabou, which I've left untouched at 1.0. If that's welcome, I'd be happy to configure BumpVer to also automatically adjust the version of Marabou as set in CMakeLists.txt.

Marabou CLI

The wheels are built to include the Marabou CLI by exposing the main function to Python and generating a wrapper script on install. This means the Marabou command is automatically installed whenever the maraboupy wheel is installed.

Configuration

The wheels are built with the standard configuration. See setup.py for the flags passed to CMake. Notably, the wheels are not compatible with the proprietary Gurobi optimizer, so users of Gurobi will still have to build Marabou and maraboupy from source.

Changes

This PR makes the following MAIN changes:

• Adds pyproject.toml, which contains meta-information for the package and configures auxiliary tooling such as bumper and cibuildwheel (see below).
• Adds setup.py, which contains the code that builds the native extension with CMake.
• Adds MANIFEST.in, which excludes some files that would otherwise be included in the package.
• Adds .github/workflows/cibuildwheel.yml, which builds Python wheels for the package on GitHub Actions. (The underlying tool cibuildwheel is configured in pyproject.toml under [tool.cibuildwheel].)
• Adds a PYTHON_LIBRARY_OUTPUT_DIRECTORY setting to CMakeLists.txt to allow setup.py to where the compiled library is written.
• Adds the relevant paths to .gitignore.
• Adds BumpVer so that the version can be updated by running bumpver update. (BumpVer is configured in pyproject.toml under [tool.bumpver].)

This PR makes the folloing changes to enable bundling the Marabou CLI:

• Moves all code from src/engine/main.cpp to src/engine/MarabouMain.cpp and renames main to marabouMain.
• Adds a new src/engine/main.cpp which defines a main which simply calls marabouMain.
• Adds a new function in maraboupy/MarabouCore.cpp called maraboupyMain and adds this function to the pybind11 module definition. The function maraboupyMain takes (std::vector<std::string> args) as input, converts it to an (int argc, char **argv) pair, and calls marabouMain. (This is done because pybind11 cannot generate bindings for a function which takes an (int argc, char **argv) pair as input.)
• Changes CMakeLists.txt to build protobuf with -fPIC. (This is needed to allow compiling it into the Python library.)
• Adds a new module maraboupy/MarabouMain which defines a main function. (This passes sys.argv to maraboupyMain and exits with the appropriate exit code.)
• Registers maraboupy.MarabouMain:main as a script called Marabou in pyproject.toml. (This causes setuptools to install a script calling this main function on the PATH whenever installing maraboupy.)
• Adds a new module maraboupy/__main__.py which imports the main function and calls it. (This is done so that maraboupy can be called via python -m maraboupy.)

This PR makes the following changes to enable running the Python tests on CI without errors or warnings:

• Fixes the broken test requirements for maraboupy:

  • Removes codecov from maraboupy/test_requirements.txt, which was pulled from PyPI. The package is not required on CI, as the main workflow uses the codecov action.
  • Relaxes the version constraints from exact versions to version bounds, e.g., numpy==1.21.0 changes to numpy>=1.21.0,<2, to ensure greater compatibility across Python versions.

• Disables the failing regression test mnist-bnn_index0_eps0.001_target9_unsat.ipq by suffixing the filename with .disabled.

• Adds support for Python 3.11:

  • Bumps pybind11 from 2.3.0 to 2.10.4, as 2.3.0 was too old to build Python 3.11 wheels without deprecation warnings (which the CMake configuration elevates to errors).
  • Adds the relevant files for the new pybind11 to the .gitignore file.

• Changes the tests for maraboupy to use absolute rather than relative imports, as the tests are not considered part of the distributed package. (The test directory is stripped out by MANIFEST.in.)

• Prunes unused imports of pytest from the tests for maraboupy.

This PR makes the following changes to fix issues with the existing CI workflow:

• Adds support for macOS to the CI:

  • Adds the OS to the matrix, with ubuntu-latest as its only value.
  • Splits the step which installs packages into (1) a step which installs system packages, which runs only on Linux, and (2) a step which installs Python packages, which runs on every OS.
  • Adds a step which installs system packages via Homebrew, which runs only on macOS.
  • Adds an entry to the matrix, which runs a Release build with clang++ on macOS.

• Fixes the broken badges in README.md:

  • Renames .github/workflows/ci-with-production.yml back to .github/workflows/ci.yml. The badges in README.md still referenced the old name, and therefore hadn't updated since the renaming took place.

• Fixes the outdated actions in the main workflow:

  • Bumps actions/cache from v1 to v3, as v1 requires the deprecated Node.js 12, which will soon be removed.
  • Adds .github/dependabot.yml, which configures dependabot to automatically open PRs when the used GitHub actions become out-of-date, to prevent this from happening in the future.

• Fixes the on clause in run the CI:

  • when changes are pushed to master;
  • when a PR is openend or changes are pushed to the PR;
  • every Monday at 7AM to catch bugs due to changes in the ecosystem; and
  • whenever someone with the appropriate privileges requests it.

  Before this change, the CI would run on every push on every branch, and on every pull request trigger, which, amongst other things, cause the CI to run twice on PRs from branches in the same repository—for example, here and here.

[wenkokke]

Unfortunately, 8fcdb3b changes the job names—see above—and as such, merging this PR would require administrative intervention, since the job names Debug build ($compiler, $build_type) are hard-coded in the branch protections.

Either someone with the privileges to override the branch protections would have to merge this PR, or they would have to be removed and reinstated. (They're listed under "Require status checks to pass before merging" in Settings > Branches > Branch protection rules > Edit.)

[wu-haoze]

• README.md:

Hi @wenkokke , thanks for taking the initiative on this. There was indeed internal discussions to make maraboupy a python package. I'll gradually make progress on reviewing this PR.

[wenkokke]

I've tried to keep the commits clean, so the easiest way to review this is probably commit by commit, and it's probably worth not squashing the commits when merging.

[wenkokke]

The only change I'm unsure about is that exporting Marabou's main in the Python extension requires compiling protobuf with -fPIC. I've conditionally set this property in CMakeLists.txt based on whether you're building maraboupy, but to keep things simple, I've changed the download script for protobuf to always build with -fPIC.

[wu-haoze]

Hi Wen, thanks for the updates. My final request is that could the authors just be "the Marabou development team", optionally with a link to https://github.com/NeuralNetworkVerification/Marabou/blob/master/AUTHORS ?

This is what Clark suggested.

[wenkokke]

It won't be possible to link to the authors file, but I can at least package it.

[wenkokke]

@anwu1219 Would you be happy for me to publish the first release to PyPI and setup the GitHub Actions workflow to automatically publish future releases as well? As a follow-up PR, of course.

[wenkokke]

I've set the authors as required (9fbac3d).

I've also:

• Added pull requests being reopened as a CI trigger (03320a6)
• Set the target architecture for wheel builds to 'native' rather than 'auto64'. The 'auto64' target includes cross-compilation to 'arm64' on macOS, which I then had to exclude in the macOS configuration, as it is unsupported by our CMake configuration (d6612b9)
• Set the OS for the cibuildwheel runners to always use the latest version. Pinning specific OS versions adds maintenance burden, and cibuildwheel takes care of backwards compatibility—Linux wheels are built in containers, and macOS wheels are built after downgrading the SDK to the specified version (45fec26)

I've also merged 'master', as #630 broke Marabou on macOS, and I needed #640 to fix it.

As far as I'm concerned, this is ready to merge.

[wenkokke]

I've pushed fixes for the bugs introduced in #630.

I asked @MatthewDaggitt to review these changes, and he approved them.

@anwu1219 Would it be possible to prioritize merging this over other PRs, to avoid further breakage?

[wenkokke]

Amazing, thanks!