cmake configure without internet access

[priv-kweihmann]

CBMC version: 5.48.0
Operating system: linux
Exact command line resulting in the issue:

• wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz build/minisat2-download/minisat2-download-prefix/src/minisat2_2.2.1.orig.tar.gz
• turn off internet connection
• cmake ../source/
  What behaviour did you expect:
  a way to prevent downloading of minisat2 sources again and again and again, as they are already in place
  What happened instead:

error: downloading 'http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz' failed

please add a way to define the sources of the download_project cmake snippet (

cbmc/src/solvers/CMakeLists.txt

Line 71 in 087296a

download_project(PROJ minisat2

) that uses prefetched sources for the default of minisat2

[priv-kweihmann]

or alternatively add the sources to those solvers as git submodules.
Whatever fits your development process best

[thomasspriggs]

Yes. I think it could be an improvement if we can avoid redownloading the minisat sources when they have already been downloaded and patched. However I currently have other priorities to work on. So I am unlikely to find time to make the required changes in the near future.

[tautschnig]

@priv-kweihmann Could you please confirm that there really even is such an issue? I just tried the following:

rm -rf build
mkdir -p build/minisat2-download/minisat2-download-prefix/src/
wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz -O build/minisat2-download/minisat2-download-prefix/src/minisat2_2.2.1.orig.tar.gz
cmake -H. -Bbuild
[...]
-- Building solvers with minisat2
-- Downloading/updating minisat2
-- Configuring done
-- Generating done
-- Build files have been written to: /X/build/minisat2-download
[1/9] Creating directories for 'minisat2-download'
[2/9] Performing download step (download, verify and extract) for 'minisat2-download'
-- verifying file...
       file='/X/build/minisat2-download/minisat2-download-prefix/src/minisat2_2.2.1.orig.tar.gz'
-- File already exists and hash match (skip download):
  file='/X/build/minisat2-download/minisat2-download-prefix/src/minisat2_2.2.1.orig.tar.gz'
  MD5='27faa19ee0508660bd6fb7f894646d42'
-- extracting...
     src='/X/build/minisat2-download/minisat2-download-prefix/src/minisat2_2.2.1.orig.tar.gz'
     dst='/X/build/minisat2-src'
-- extracting... [tar xfz]
-- extracting... [analysis]
-- extracting... [rename]
-- extracting... [clean up]
-- extracting... done
[3/9] No update step for 'minisat2-download'
[4/9] Performing patch step for 'minisat2-download'
patching file minisat/core/Solver.cc
patching file minisat/core/SolverTypes.h
patching file minisat/mtl/IntTypes.h
patching file minisat/mtl/Vec.h
patching file minisat/simp/SimpSolver.cc
patching file minisat/utils/Options.h
patching file minisat/utils/ParseUtils.h
patching file minisat/utils/System.h
patching file minisat/mtl/Vec.h
patching file minisat/mtl/XAlloc.h
[5/9] No configure step for 'minisat2-download'
[6/9] No build step for 'minisat2-download'
[7/9] No install step for 'minisat2-download'
[8/9] No test step for 'minisat2-download'
[9/9] Completed 'minisat2-download'
[...]

[priv-kweihmann]

@tautschnig will try that - but at first glance that looks like a valid workaround, even though a dedicated option to prevent network access would be really nice

[tautschnig]

@priv-kweihmann Can I just confirm that the desired added value of having a dedicated option is such that the user could specify the path to a pre-existing file?

[priv-kweihmann]

@tautschnig yes! In my use case I have the needed blob outside of the current build workspace and it would be nice to handle that without the need to know the internal path structure of cbmc's cmake implementation

[priv-kweihmann]

@tautschnig your proposed workaround works like a charm - this ticket could therefore be a very low priority enhancement

[tautschnig]

I propose #6649 as the fix: I decided not to introduce a new flag, as that flag itself would require documentation. Instead, the above procedure is now documented.

[priv-kweihmann]

Works for me - thanks