Move third-party MiniSat to 3p/, replacing download-and-patch#9115
Open
kroening wants to merge 2 commits into
Open
Move third-party MiniSat to 3p/, replacing download-and-patch#9115kroening wants to merge 2 commits into
kroening wants to merge 2 commits into
Conversation
Moves the vendored miniz sources from jbmc/src/miniz/ to 3p/miniz-3.0.2/, and adds 3p/copyright.miniz-3.0.2 (Debian copyright-format 1.0) documenting provenance (upstream commit 0c30a001bc3c70, Expat license) and the local modifications. The build glue remains in jbmc/src/miniz/. Also removes the stale src/miniz/module_dependencies.txt, left behind when miniz moved to jbmc/src. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
kroening
requested review from
a team,
peterschrammel and
tautschnig
as code owners
MiniSat 2.2.1, CBMC's default SAT solver, was downloaded from Debian at build time and patched via scripts/minisat-2.2.1-patch. This vendors it in the source tree instead: - 3p/minisat-2.2.1-original/ is byte-for-byte identical to the Debian source tarball minisat2_2.2.1.orig.tar.gz, for reference. - 3p/minisat-2.2.1-patched/ is the copy that is built; it equals the original plus the previous patch, which is hereby retired. The patch can be re-created by diffing the two directories. - 3p/copyright.minisat-2.2.1 (Debian copyright-format 1.0) documents provenance and the local modifications. The patch and the CMake download machinery are removed; the CMake glue from scripts/minisat2_CMakeLists.txt moves into src/solvers/CMakeLists.txt. The minisat2-download make target remains as a deprecated stub that prints a note that MiniSat is now in-tree. Building CBMC with the default solver no longer requires network access. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
3p/minisat-2.2.1-original/is byte-for-byte identical to the Debian source tarballminisat2_2.2.1.orig.tar.gz, for reference3p/minisat-2.2.1-patched/is the copy that is built; it equals the original plus the previousscripts/minisat-2.2.1-patch, which is hereby retired (it can be re-created by diffing the two directories)3p/copyright.minisat-2.2.1(Debian copyright-format 1.0) documents provenance and the local modificationsdownload_projectmachinery; the glue fromscripts/minisat2_CMakeLists.txtmoves intosrc/solvers/CMakeLists.txtminisat2-downloadmake target remains as a deprecated stub that prints a note that MiniSat is now in-treeIncludes the commit from #9114 (this PR needs its
3p/lint exclusions); the diff reduces to the MiniSat commit once #9114 merges.Test plan
cbmcbuild, and a verification run with--sat-solver minisat2succeedmake -C src/solversbuilds the MiniSat objects from3p/with-Werror;make cleanremoves them (keeps the CI cleanup check happy)make -C src minisat2-downloadprints the deprecation note🤖 Generated with Claude Code