forked from verus-lang/verus
verus source docs guide src install-singular.md
1.6 kB · 19 lines
Markdown

Installing and configuring Singular #

Singular must be installed in order to use the integer_ring solver mode.

Steps:

  1. Install Singular

    • To use Singular's standard library, you need more than just the Singular executable binary. Hence, when possible, we strongly recommend using your system's package manager. Regardless of the method you select, please install Singular version 4.3.2: other versions are untested, and 4.4.0 is known to be incompatible with Verus. Here are some suggested steps for different platforms.
      • Mac: brew install Singular and set the VERUS_SINGULAR_PATH environment variable when running Verus. (e.g. VERUS_SINGULAR_PATH=/usr/local/bin/Singular). For more options, see Singular's OS X installation guide.

      • Debian-based Linux: apt-get install singular and set the VERUS_SINGULAR_PATH environment variable when running Verus. (e.g. VERUS_SINGULAR_PATH=/usr/bin/Singular). For more options, see Singular's Linux installation guide.

      • Windows: See Singular's Windows installation guide.

  2. Compiling Verus with Singular Support

    • The integer_ring functionality is conditionally compiled when the singular feature is set. To add this feature, add the --features singular flag when you invoke cargo build to compile Verus.