repodb.md

Introduction

SAT solver can be used to implement xbps-repodb --index, that move packages from stagedata to repodata, ensuring consistency of package requirements.

Variables

Real packages, virtual packages and shared libraries are represented as boolean variables. Value of true represents presence of item in repo, false represent absence.

Notation for variable of real package is its pkver: pkg-1_1, for variable of virtual package: pkgver prefixed with virt: virt(pkg-1_1), for variable of shared libraries: its soname ending with version: libm.so.6.

Constraints

Constraints of dependencies

Constraints are created once all packages in repodata and stagedata are known, in order to generate right lists of packages providing solibs and virtuals.

• virtual package provides: virt(awk-0_1) ↔ (gawk-5.1.0_1 ∨ nawk-20210110_1). Every package will provide virtual package of itself: virt(libx-2_1) ↔ (libx-2_1 ∨ libxfresh-compat2-0.9_1)

• dependencies: xbps-0.59.1_5 → (virt(libarchive-3.5.1_2) ∨ virt(libarchive-3.5.2_1))

• used shared libraries: cmd-1_1 → libm.so.6

• provided shared libraries: libx.so.2 ↔ (libx-2_1 ∨ libxfresh-compat2-0.9_1)

Constraints of updates

• for package that is unmodified in stagedata, constraint of that package must be present: pkg-1.0_1

• for packages updated in stagedata: constraint of exactly one version present: (pkg-1.0_3 ↔ ¬ pkg-1.1_1)

• no constraint for added and removed packages

Process of updating index

First, construct state formula consisting of constraints of dependencies and presence of unmodified packages.

Then, for every every package different between stagedata and repodata, find solution of state formula extended with presence of package as in stagedata. If solution is found, fixate in state formula all packages of solution matching stagedata. Repeat for next difference.

If any package from stagedata was used, write state to repodata.