Skip to content

What we redistribute, and under which terms

Generated by tools/redistribution_report.py from the pin files the build and the mirror actually use. Editing this page by hand would make it a second, drifting claim; change the pins instead.

This is not legal advice. It is the dossier for a licence review: every artifact we publish, what its licence asks of a distributor, and what we do about it. What it does not cover is listed at the end.

1. Software we build ourselves

We compile these from pinned sources and publish the result. That makes us a distributor of the compiled work and of the libraries it links.

Gappa 1.4.0 (Windows x86_64)

  • Licence: CECILL-2.1 AND GPL-3.0-or-later
  • Source: https://gappa.gitlabpages.inria.fr/releases/gappa-1.4.0.tar.gz (sha256 6bf17688f0d0d0815713f3c3ad567747…)
  • Upstream: https://gitlab.inria.fr/gappa/gappa
  • Linked dynamically, libraries shipped beside the binary:
Library From Licence
libgcc_s_seh-1.dll mingw-w64-x86_64-gcc-libs spdx:GPL-3.0-or-later WITH GCC-exception-3.1 AND LGPL-2.1-or-later
libgmp-10.dll mingw-w64-x86_64-gmp LGPL3 GPL
libmpfr-6.dll mingw-w64-x86_64-mpfr spdx:LGPL-3.0-or-later
libstdc++-6.dll mingw-w64-x86_64-gcc-libs spdx:GPL-3.0-or-later WITH GCC-exception-3.1 AND LGPL-2.1-or-later
libwinpthread-1.dll mingw-w64-x86_64-libwinpthread spdx:MIT AND BSD-3-Clause-Clear
  • How the obligations are discharged:
    • full licence texts inside the package, under licenses/;
    • NOTICE.txt naming every bundled library and its licence;
    • SOURCES.txt naming where each compiled source came from;
    • the source archive published in the same directory as the binary;
    • dynamic linking, so an LGPL library can be replaced in place.

Why dynamic: GMP und MPFR stehen unter LGPLv3. Statisch gelinkt laeuft gappa.exe zwar allein (gemessen: 21434128 Bytes, keine fremde DLL), verpflichtet uns aber, eine Relink-Moeglichkeit beizulegen. Dynamisch plus die fuenf DLLs ist der lizenzsaubere Weg und der, den das Paket geht.

matiec 0.1 (Windows x86_64)

  • Licence: GPL-3.0-or-later AND LGPL-3.0-or-later
  • Source: https://github.com/beremiz/matiec/archive/7949c0bda1787de9c7cacaa4876ede49f85262dd.tar.gz (sha256 e99d845747f3a53b0d052e511a8d43da…)
  • Upstream: https://github.com/beremiz/matiec
  • Linked dynamically, libraries shipped beside the binary:
Library From Licence
libgcc_s_seh-1.dll mingw-w64-x86_64-gcc-libs spdx:GPL-3.0-or-later WITH GCC-exception-3.1 AND LGPL-2.1-or-later
libstdc++-6.dll mingw-w64-x86_64-gcc-libs spdx:GPL-3.0-or-later WITH GCC-exception-3.1 AND LGPL-2.1-or-later
libwinpthread-1.dll mingw-w64-x86_64-libwinpthread spdx:MIT AND BSD-3-Clause-Clear
  • How the obligations are discharged:
    • full licence texts inside the package, under licenses/;
    • NOTICE.txt naming every bundled library and its licence;
    • SOURCES.txt naming where each compiled source came from;
    • the source archive published in the same directory as the binary;
    • dynamic linking, so an LGPL library can be replaced in place.

Why dynamic: Wie bei gappa: die beiliegenden GCC-Laufzeitbibliotheken stehen unter GPL-3.0 mit Runtime Library Exception bzw. LGPL-2.1. Dynamisch plus beiliegende DLLs ist der Weg, bei dem sich die Bibliothek austauschen laesst.

zqel itself

The standalone builds embed a Python runtime, the packages Nuitka reports as included, and Z3's native library. The package carries a NOTICE.txt generated from Nuitka's own report and from the licence metadata each package publishes — not from a hand-kept list. Licence texts land under licenses/.

2. Software we mirror unchanged

Byte-for-byte copies of upstream releases. We do not repack them: repacking would turn passing something on into modifying it, and different obligations would apply. Each copy has a .notice.txt beside it naming origin, checksum and licence.

cvc5 1.2.0

  • Licence: BSD-3-Clause
  • Upstream: https://github.com/cvc5/cvc5
  • Artifacts: 1
    • cvc5-Win64-x86_64-static.zip — sha256 256f4af3f4181e770801df436852cb3c…
  • Licence texts inside the archive (verified on every mirror run):
    • cvc5-Win64-x86_64-static/COPYING
    • cvc5-Win64-x86_64-static/licenses/gpl-3.0.txt
    • cvc5-Win64-x86_64-static/licenses/lgpl-3.0.txt
    • cvc5-Win64-x86_64-static/licenses/minisat-LICENSE

Modifizierte BSD. cvc5 KANN gegen GPL-Bibliotheken (CLN, GLPK) gelinkt werden, tut es aber standardmaessig nicht - wir spiegeln die Variante OHNE '-gpl' im Namen. Das Archiv fuehrt zusaetzlich gpl-3.0.txt und lgpl-3.0.txt mit, weil cvc5 gegen GMP (LGPLv3) linkt; nach cvc5s eigener COPYING bleibt das kombinierte Werk unter der modifizierten BSD.

cbmc 6.4.0

  • Licence: BSD-4-Clause
  • Upstream: https://github.com/diffblue/cbmc
  • Artifacts: 1
    • cbmc-6.4.0-win64.msi — sha256 4891b45b83b4540e9d69e9b5d898e250…
  • Licence text shipped beside it: cbmc-6.4.0-LICENSE.txt

BSD mit Werbeklausel (Ziffer 3): wer in Werbematerial Merkmale dieser Software nennt, muss die Danksagung an Kroening, Clarke, Oxford und Carnegie Mellon anzeigen. Ziffer 2 verlangt, dass Hinweis, Bedingungen und Haftungsausschluss bei einer Binaerweitergabe 'in der Dokumentation oder anderen beiliegenden Materialien' wiedergegeben werden - genau dafuer ist der Beipackzettel da. Ein .msi laesst sich nicht ohne Windows durchsehen, deshalb liegt der Lizenztext hier als eigene Datei statt als Verweis ins Archiv.

kani 0.67.0

  • Licence: Apache-2.0 OR MIT
  • Upstream: https://github.com/model-checking/kani
  • Artifacts: 4
    • kani-0.67.0-aarch64-apple-darwin.tar.gz — sha256 7fd0b71130aa37bd1e346eba675aad09…
    • kani-0.67.0-aarch64-unknown-linux-gnu.tar.gz — sha256 974128f44dd43618a06d21e5fe6d9ff6…
    • kani-0.67.0-x86_64-apple-darwin.tar.gz — sha256 e394c3d940ed9df4f67ef5388c5612f1…
    • kani-0.67.0-x86_64-unknown-linux-gnu.tar.gz — sha256 3b5f7afd3b51603ee720db7bc1bc4fe4…
  • Licence texts inside the archive (verified on every mirror run):
    • kani-0.67.0/license-notes.txt

Doppelt lizenziert. Apache-2.0 verlangt die Behandlung einer NOTICE-Datei, falls vorhanden - kani hat keine (gemessen 2026-09-13: HTTP 404). Das Archiv fuehrt license-notes.txt mit.

3. What this dossier does not cover

  • The transitive dependency closure of the Windows build machine. tools/windows/msys2.lock.json pins the packages we install and the owners of the DLLs we ship. Everything those pull in is not pinned.
  • A legal reading. Nobody with a licence qualification has looked at this. The obligations above are what the licence texts say, read by an engineer.
  • cvc5's exact binary configuration. We mirror the release variant without -gpl in its name. Whether that build links GMP statically, and what that means for the LGPL relink provision, has not been established by inspecting the binary.
  • Anything distributed outside dl.zqel.org and the forgejo package registry.