Switch Glucose download source to GitHub

[tautschnig]

www.labri.fr appears to be (temporarily?) offline, which already
happened several weeks ago, when it was offline for about one day. To
avoid spurious CI failures, switch to a GitHub source that hosts to
Glucose source. The use of Bruno Dutertre's fork also reduces the number
of patches that need to be applied, mostly leaving just Windows-specific
bits to be patched.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[NlightNFotis]

Just one question.

[NlightNFotis]

As far as I understand we are downloading the main branch, which seems to be something like a master branch of sorts.

How often is this being updated, and could random updates cause CI to fail by essence of this hash check failing?

[tautschnig]

The repo only has total of 12 commits, and the most recent commit was July 2021. I would expect the rate of updates to be very low, if any at all. So, yes, CI could fail, but when it does, it is right to do so: it would be a change that we should manually review to make sure it doesn't conflict with any of our expectations on this third-party component.

[thomasspriggs]

I am not entirely convinced that we should be following the main branch on someone else's fork. Depending on the development workflow they are using, we could be fetching untested or even non-compiling commits. Is there a way we can pin this to a release version?

[kroening]

An option would be to get
https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.zip

[chrisr-diffblue]

Is it worth stepping back a pace or two and consider whether using a submodule or subtree is appropriate? Also other fleeting thoughts... should we contribute our local patches back to Bruno to avoid maintaining them ourselves (and maintaining our local patch management)? Should we fork Bruno's repo, apply our patches there, and download from our fork? No major preferences from my side, but just feels worth a thought and explicit decisions.

[tautschnig]

I have now added a comment that indicates the exact revision and also states that our CI jobs will fail if "main" ever moves.

[tautschnig]

As we're in this situation once again (see #6986): pinging @NlightNFotis @thomasspriggs @peterschrammel for an update.

[thomasspriggs]

I am against merging this as-is, because I think that as a minimum we should be pinning the download to a fixed commit hash as suggested by @kroening rather than just taking the latest version of the main branch. @tautschnig Are you happy to make this update before we approve/merge this or would you like myself and @NlightNFotis to copy your branch and manage the change ourselves?

[tautschnig]

I've now changed download URL to use the specific commit hash rather than a branch.

[TGWDB]

Looks like the right solution for now. Thanks.

[codecov]

Codecov Report

Merging #6539 (151c8fe) into develop (8eef445) will decrease coverage by 0.03%.
The diff coverage is 84.43%.

@@             Coverage Diff             @@
##           develop    #6539      +/-   ##
===========================================
- Coverage    77.84%   77.81%   -0.04%     
===========================================
  Files         1570     1570              
  Lines       180439   180679     +240     
===========================================
+ Hits        140468   140598     +130     
- Misses       39971    40081     +110     

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	100.00% <ø> (ø)
src/goto-instrument/horn_encoding.cpp	72.70% <0.00%> (+0.43%)	⬆️
src/goto-symex/goto_symex_state.cpp	91.71% <ø> (ø)
src/goto-symex/goto_symex_state.h	100.00% <ø> (ø)
src/util/replace_symbol.cpp	78.20% <36.95%> (-10.10%)	⬇️
src/linking/linking.cpp	58.71% <50.00%> (-0.03%)	⬇️
src/util/rename_symbol.cpp	76.82% <69.38%> (-3.00%)	⬇️
src/ansi-c/c_typecheck_base.cpp	82.50% <92.30%> (+1.34%)	⬆️
src/goto-symex/field_sensitivity.cpp	91.27% <96.00%> (-0.24%)	⬇️
src/goto-instrument/contracts/contracts.cpp	94.31% <98.87%> (+0.21%)	⬆️
... and 22 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b466503...151c8fe. Read the comment docs.