Remove dependency on corrosion.

We no longer need to keep the C++/Rust builds in sync, as the Rust build
now depends on the static library libcprover.x.y.z.a being present anywhere
in the user's computer, thus corrosion brings no benefits, and ties us down
to keeping two build systems in sync when we don't need to, along with waisting
time building the rust project twice when we want to run the tests.

To build the Rust project, please do from the src/libcprover-rust/ directory,
using `cargo`, based on the information present on its own directory.

Author: NlightNFotis

.github/workflows/pull-request-check-rust-api.yaml

@@ -52,7 +52,7 @@ jobs:
       # local experiments on the same platform, but it seems to be doing no harm to the build overall
       # and allows us to test the Rust API on Linux without issues.
       - name: Configure using CMake
-        run: cmake -S. -B${{env.default_build_dir}} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_COMPILER=/usr/bin/clang-13 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-13 -DWITH_RUST_API=ON
+        run: cmake -S. -B${{env.default_build_dir}} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_COMPILER=/usr/bin/clang-13 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-13
       - name: Build with CMake
         run: cmake --build ${{env.default_build_dir}} -j2
       - name: Print ccache stats
@@ -92,7 +92,7 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Configure using CMake
-        run: cmake -S. -B${{env.default_build_dir}} -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -DWITH_RUST_API=ON
+        run: cmake -S. -B${{env.default_build_dir}} -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++
       - name: Build with Ninja
         run: cd ${{env.default_build_dir}}; ninja -j3
       - name: Print ccache stats

CMakeLists.txt

@@ -257,33 +257,4 @@ if(WITH_JBMC)
     add_subdirectory(jbmc)
 endif()
 
-option(WITH_RUST_API "Build with the CPROVER Rust API" OFF)
-if(${CMAKE_VERSION} VERSION_LESS "3.19.0" AND WITH_RUST_API)
-    message("Unable to build the Rust API without version CMake 3.19.0")
-    message(FATAL_ERROR "(The Rust build depends on CMake plugins with dependencies on CMake 3.19.0 and above)")
-else()
-    if(WITH_RUST_API)
-    include(FetchContent)
-
-    FetchContent_Declare(
-        Corrosion
-        GIT_REPOSITORY https://github.com/corrosion-rs/corrosion.git
-        GIT_TAG v0.3.1
-    )
-
-    FetchContent_MakeAvailable(Corrosion)
-
-    corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml)
-    list(JOIN sat_impl " " sat_impl_str)
-    corrosion_set_env_vars(cprover-api-rust CBMC_LIB_DIR=${CMAKE_BINARY_DIR} CBMC_VERSION=${CBMC_VERSION})
-    corrosion_link_libraries(cprover-api-rust cprover-api-cpp)
-    install(TARGETS cprover-api-rust RUNTIME DESTINATION lib)
-    # NOTE: We want to rename to a name consistent with the name of the
-    # rest of the static libraries built as a result of a build. The reason
-    # we cannot set the target name directly is that Cargo doesn't support
-    # hyphens in names of packages, so it builds the name by default with
-    # an underscore.
-    endif()
-endif()
-
 include(cmake/packaging.cmake)