Add prettier and improve CI

.github/workflows/ci.yml

@@ -0,0 +1,47 @@
+name: CI
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+
+      - name: Setup mdBook
+        uses: peaceiris/actions-mdbook@v2
+        with:
+          mdbook-version: "0.4.43"
+
+      - run: mdbook build
+
+  # Report when we become incompatible with latest mdbook, but don't fail the workflow
+  build-mdbook-latest:
+    name: Build (mdbook latest)
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+
+      - name: Setup mdBook
+        uses: peaceiris/actions-mdbook@v2
+        with:
+          mdbook-version: "latest"
+
+      - run: mdbook build
+
+  lint:
+    name: Lint
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+
+      - name: Prettier
+        run: npx prettier --check .

.github/workflows/cloudflare.yml

@@ -1,3 +1,4 @@
+name: Cloudflare
 on: [push]
 
 jobs:
@@ -13,10 +14,9 @@ jobs:
 
       # Build the guide to ./book
       - name: Setup mdBook
-        uses: peaceiris/actions-mdbook@v1
+        uses: peaceiris/actions-mdbook@v2
         with:
-          mdbook-version: '0.4.37'
-          # mdbook-version: 'latest'
+          mdbook-version: "0.4.43"
       - run: mdbook build
 
       - name: Publish to Cloudflare Pages

.prettierrc.toml

@@ -0,0 +1 @@
+proseWrap = "always"

README.md

@@ -1,12 +1,19 @@
 # PubGrub guide
 
-Source for the PubGrub guide.
-The published version is available at https://pubgrub-rs-guide.pages.dev.
-This guide is made with [mdBook][mdbook].
-To compile it locally, install mdBook and run
+Source for the PubGrub guide. The published version is available at
+https://pubgrub-rs-guide.pages.dev. This guide is made with [mdBook][mdbook]. To
+compile it locally, install mdBook and run
 
 ```sh
 mdbook serve
 ```
 
+We use prettier for consistent formatting. The easiest way to run it is through
+npx:
+
+```sh
+npx prettier --write --print-width 80 --prose-wrap always "**/*.md"
+npx prettier --write "**/*.yml"
+```
+
 [mdbook]: https://github.com/rust-lang/mdBook

book.toml

@@ -1,8 +1,6 @@
 [book]
 authors = ["Matthieu Pizenberg"]
 language = "en"
-multilingual = false
-src = "src"
 title = "PubGrub Guide"
 
 [output.html]

src/contributing.md

@@ -1,15 +1,13 @@
 # How can I contribute? Here are some ideas
 
-- Use it!
-  Indeed there is quite some work left for custom
-  dependency providers. So just using the crate, building
-  you own dependency provider for your favorite programming language
-  and letting us know how it turned out
-  would be amazing feedback already!
+- Use it! Indeed there is quite some work left for custom dependency providers.
+  So just using the crate, building you own dependency provider for your
+  favorite programming language and letting us know how it turned out would be
+  amazing feedback already!
 
-- Non failing extension for multiple versions.
-  Currently, the solver works by allowing only one version per package.
-  In some contexts however, we may want to not fail if multiple versions are required,
-  and return instead multiple versions per package.
-  Such situations may be for example allowing multiple major versions of the same crate.
-  But it could be more general than that exact scenario.
+- Non failing extension for multiple versions. Currently, the solver works by
+  allowing only one version per package. In some contexts however, we may want
+  to not fail if multiple versions are required, and return instead multiple
+  versions per package. Such situations may be for example allowing multiple
+  major versions of the same crate. But it could be more general than that exact
+  scenario.

src/internals/conflict_resolution.md

@@ -1,47 +1,41 @@
 # Conflict resolution
 
-As stated before, a conflict is a satisfied incompatibility
-that we detected in the unit propagation loop.
-The goal of conflict resolution is to backtrack the partial solution
-such that we have the following guarantees:
+As stated before, a conflict is a satisfied incompatibility that we detected in
+the unit propagation loop. The goal of conflict resolution is to backtrack the
+partial solution such that we have the following guarantees:
 
-1. The root cause incompatibility of the conflict is almost satisfied
-   (such that we can continue unit propagation).
+1. The root cause incompatibility of the conflict is almost satisfied (such that
+   we can continue unit propagation).
 2. The following derivations will be different than before conflict resolution.
 
-Let the "satisfier" be the earliest assignment in the partial solution
-making the incompatibility fully satisfied by the partial solution up to that point.
-We know that we want to backtrack the partial solution at least previous to that assignment.
-Backtracking only makes sense if done at decision levels frontiers.
-As such the conflictual incompatibility can only become "almost satisfied"
-if there is only one package term related to incompatibility satisfaction
-at the decision level of that satisfier.
-When the satisfier is a decision this is trivial since all previous assignments
-are of lower decision levels.
-When the satisfier is a derivation however we need to check that property.
-We do that by computing the "previous satisfier" decision level.
-The previous satisfier is (if it exists) the earliest assignment
-previous to the satisfier such that the partial solution up to that point,
-plus the satisfier, makes the incompatibility satisfied.
-Once we found it, we know that property (1) is guaranteed as long as
-we backtrack to a decision level between the one of the previous satisfier
-and the one of the satisfier, as long as these are different.
+Let the "satisfier" be the earliest assignment in the partial solution making
+the incompatibility fully satisfied by the partial solution up to that point. We
+know that we want to backtrack the partial solution at least previous to that
+assignment. Backtracking only makes sense if done at decision levels frontiers.
+As such the conflictual incompatibility can only become "almost satisfied" if
+there is only one package term related to incompatibility satisfaction at the
+decision level of that satisfier. When the satisfier is a decision this is
+trivial since all previous assignments are of lower decision levels. When the
+satisfier is a derivation however we need to check that property. We do that by
+computing the "previous satisfier" decision level. The previous satisfier is (if
+it exists) the earliest assignment previous to the satisfier such that the
+partial solution up to that point, plus the satisfier, makes the incompatibility
+satisfied. Once we found it, we know that property (1) is guaranteed as long as
+we backtrack to a decision level between the one of the previous satisfier and
+the one of the satisfier, as long as these are different.
 
-If the satisfier and previous satisfier decisions levels are the same,
-we cannot guarantee (1) for that incompatibility after backtracking.
-Therefore, the key of conflict resolution is to derive a new incompatibility
-for which we will be able to guarantee (1).
-And we have seen how to do that with the
-[rule of resolution](incompatibilities.md#rule-of-resolution).
-We will derive a new incompatibility called the "prior cause"
-as the resolvent of the current incompatibility and
-the incompatibility which is the cause of the satisfier.
-If necessary, we repeat that procedure until finding an incompatibility,
-called the "root cause" for which we can guarantee that it will
-be almost satisfied after backtracking (1).
+If the satisfier and previous satisfier decisions levels are the same, we cannot
+guarantee (1) for that incompatibility after backtracking. Therefore, the key of
+conflict resolution is to derive a new incompatibility for which we will be able
+to guarantee (1). And we have seen how to do that with the
+[rule of resolution](incompatibilities.md#rule-of-resolution). We will derive a
+new incompatibility called the "prior cause" as the resolvent of the current
+incompatibility and the incompatibility which is the cause of the satisfier. If
+necessary, we repeat that procedure until finding an incompatibility, called the
+"root cause" for which we can guarantee that it will be almost satisfied after
+backtracking (1).
 
-Now the question is where do we cut?
-Is there a reason we cut at the previous satisfier decision level?
-Is it to guarantee (2)? Would that not be guaranteed if we picked
-another decision level? Is it because backtracking further back
+Now the question is where do we cut? Is there a reason we cut at the previous
+satisfier decision level? Is it to guarantee (2)? Would that not be guaranteed
+if we picked another decision level? Is it because backtracking further back
 will reduce the number of potential conflicts?

src/internals/incompatibilities.md

@@ -1,28 +1,25 @@
 # Incompatibilities
 
-
 ## Definition
 
-Incompatibilities are called "nogoods" in [CDNL-ASP][ass] terminology.
-**An incompatibility is a [conjunction][conjunction] of package terms that must
-be evaluated false**, meaning at least one package term must be evaluated false.
-Otherwise we say that the incompatibility has been "satisfied".
-Satisfied incompatibilities represent conflicts and thus
-the goal of the PubGrub algorithm is to build a solution
-such that none of the produced incompatibilities are ever satisfied.
-If one incompatibility becomes satisfied at some point,
-the algorithm finds the root cause of it and backtracks the partial solution
-before the decision at the origin of that root cause.
-
-> Remark: incompatibilities (nogoods) are the opposite of clauses
-> in traditional conflict-driven clause learning ([CDCL][cdcl])
-> which are disjunctions of literals that must be evaluated true,
-> so have at least one literal evaluated true.
+Incompatibilities are called "nogoods" in [CDNL-ASP][ass] terminology. **An
+incompatibility is a [conjunction][conjunction] of package terms that must be
+evaluated false**, meaning at least one package term must be evaluated false.
+Otherwise we say that the incompatibility has been "satisfied". Satisfied
+incompatibilities represent conflicts and thus the goal of the PubGrub algorithm
+is to build a solution such that none of the produced incompatibilities are ever
+satisfied. If one incompatibility becomes satisfied at some point, the algorithm
+finds the root cause of it and backtracks the partial solution before the
+decision at the origin of that root cause.
+
+> Remark: incompatibilities (nogoods) are the opposite of clauses in traditional
+> conflict-driven clause learning ([CDCL][cdcl]) which are disjunctions of
+> literals that must be evaluated true, so have at least one literal evaluated
+> true.
 >
-> The gist of CDCL is that it builds a solution to satisfy a
-> [conjunctive normal form][cnf] (conjunction of clauses) while
-> CDNL builds a solution to unsatisfy a [disjunctive normal form][dnf]
-> (disjunction of nogoods).
+> The gist of CDCL is that it builds a solution to satisfy a [conjunctive normal
+> form][cnf] (conjunction of clauses) while CDNL builds a solution to unsatisfy
+> a [disjunctive normal form][dnf] (disjunction of nogoods).
 >
 > In addition, PubGrub is a lazy CDNL algorithm since the disjunction of nogoods
 > (incompatibilities) is built on the fly with the solution.
@@ -33,84 +30,77 @@ before the decision at the origin of that root cause.
 [cnf]: https://en.wikipedia.org/wiki/Conjunctive_normal_form
 [dnf]: https://en.wikipedia.org/wiki/Disjunctive_normal_form
 
-In this guide, we will note incompatibilities with curly braces.
-An incompatibility containing one term \\(T_a\\) for package \\(a\\)
-and one term \\(T_b\\) for package \\(b\\) will be noted
+In this guide, we will note incompatibilities with curly braces. An
+incompatibility containing one term \\(T_a\\) for package \\(a\\) and one term
+\\(T_b\\) for package \\(b\\) will be noted
 
 \\[ \\{ a: T_a, b: T_b \\}. \\]
 
-> Remark: in a more "mathematical" setting, we would probably have noted
-> \\( T_a \land T_b \\), but the chosen notation maps well
-> with the representation of incompatibilities as hash maps.
-
+> Remark: in a more "mathematical" setting, we would probably have noted \\( T_a
+> \land T_b \\), but the chosen notation maps well with the representation of
+> incompatibilities as hash maps.
 
 ## Properties
 
-**Packages only appear once in an incompatibility**.
-Since an incompatibility is a conjunction,
-multiple terms for the same package are merged with the intersection of those terms.
+**Packages only appear once in an incompatibility**. Since an incompatibility is
+a conjunction, multiple terms for the same package are merged with the
+intersection of those terms.
 
-**Terms that are always satisfied can be removed from an incompatibility**.
-We previously explained that the term \\( \neg [\varnothing] \\) is always evaluated true.
-As a consequence, it can safely be removed from the conjunction of terms that is the incompatibility.
+**Terms that are always satisfied can be removed from an incompatibility**. We
+previously explained that the term \\( \neg [\varnothing] \\) is always
+evaluated true. As a consequence, it can safely be removed from the conjunction
+of terms that is the incompatibility.
 
 \\[ \\{ a: T_a, b: T_b, c: \neg [\varnothing] \\} = \\{ a: T_a, b: T_b \\} \\]
 
-**Dependencies can be expressed as incompatibilities**.
-Saying that versions in range \\( r_a \\) of package \\( a \\)
-depend on versions in range \\( r_b \\) of package \\( b \\)
-can be expressed by the incompatibility
+**Dependencies can be expressed as incompatibilities**. Saying that versions in
+range \\( r_a \\) of package \\( a \\) depend on versions in range \\( r_b \\)
+of package \\( b \\) can be expressed by the incompatibility
 
 \\[ \\{ a: [r_a], b: \neg [r_b] \\}. \\]
 
-
 ## Unit propagation
 
 If all terms but one of an incompatibility are satisfied by a partial solution,
-we can deduce that the remaining unsatisfied term must be evaluated false.
-We can thus derive a new unit term for the partial solution
-which is the negation of the remaining unsatisfied term of the incompatibility.
-For example, if we have the incompatibility
-\\( \\{ a: T_a, b: T_b, c: T_c \\} \\)
-and if \\( T_a \\) and \\( T_b \\) are satisfied by terms in the partial solution
-then we can derive that the term \\( \overline{T_c} \\) can be added for package \\( c \\)
+we can deduce that the remaining unsatisfied term must be evaluated false. We
+can thus derive a new unit term for the partial solution which is the negation
+of the remaining unsatisfied term of the incompatibility. For example, if we
+have the incompatibility \\( \\{ a: T_a, b: T_b, c: T_c \\} \\) and if \\( T_a
+\\) and \\( T_b \\) are satisfied by terms in the partial solution then we can
+derive that the term \\( \overline{T_c} \\) can be added for package \\( c \\)
 in the partial solution.
 
-
 ## Rule of resolution
 
-Intuitively, we are able to deduce things such as if package \\( a \\)
-depends and package \\( b \\) which depends on package \\( c \\),
-then \\( a \\) depends on \\( c \\).
-With incompatibilities, we would note
+Intuitively, we are able to deduce things such as if package \\( a \\) depends
+and package \\( b \\) which depends on package \\( c \\), then \\( a \\) depends
+on \\( c \\). With incompatibilities, we would note
 
-\\[               \\{ a: T_a, b: \overline{T_b} \\}, \quad
-                  \\{ b: T_b, c: \overline{T_c} \\}  \quad
-\Rightarrow \quad \\{ a: T_a, c: \overline{T_c} \\}. \\]
+\\[ \\{ a: T_a, b: \overline{T_b} \\}, \quad \\{ b: T_b, c: \overline{T_c} \\}
+\quad \Rightarrow \quad \\{ a: T_a, c: \overline{T_c} \\}. \\]
 
-This is the simplified version of the rule of resolution.
-For the generalization, let's reuse the "more mathematical" notation of conjunctions
-for incompatibilities \\( T_a \land T_b \\) and the above rule would be
+This is the simplified version of the rule of resolution. For the
+generalization, let's reuse the "more mathematical" notation of conjunctions for
+incompatibilities \\( T_a \land T_b \\) and the above rule would be
 
-\\[               T_a \land \overline{T_b}, \quad
-                  T_b \land \overline{T_c}  \quad
-\Rightarrow \quad T_a \land \overline{T_c}. \\]
+\\[ T_a \land \overline{T_b}, \quad T_b \land \overline{T_c} \quad \Rightarrow
+\quad T_a \land \overline{T_c}. \\]
 
 In fact, the above rule can also be expressed as follows
 
-\\[               T_a \land \overline{T_b}, \quad
-                  T_b \land \overline{T_c}  \quad
-\Rightarrow \quad T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c} \\]
+\\[ T_a \land \overline{T_b}, \quad T_b \land \overline{T_c} \quad \Rightarrow
+\quad T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c} \\]
 
-since for any term \\( T \\), the disjunction \\( T \lor \overline{T} \\) is always true.
-In general, for any two incompatibilities \\( T_a^1 \land T_b^1 \land \cdots \land T_z^1 \\)
-and \\( T_a^2 \land T_b^2 \land \cdots \land T_z^2 \\) we can deduce a third,
-called the resolvent whose expression is
+since for any term \\( T \\), the disjunction \\( T \lor \overline{T} \\) is
+always true. In general, for any two incompatibilities \\( T_a^1 \land T_b^1
+\land \cdots \land T_z^1 \\) and \\( T_a^2 \land T_b^2 \land \cdots \land T_z^2
+\\) we can deduce a third, called the resolvent whose expression is
 
-\\[ (T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2). \\]
+\\[ (T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land
+T_z^2). \\]
 
-In that expression, only one pair of package terms is regrouped as a union (a disjunction),
-the others are all intersected (conjunction).
-If a term for a package does not exist in one incompatibility,
-it can safely be replaced by the term \\( \neg [\varnothing] \\) in the expression above
-as we have already explained before.
+In that expression, only one pair of package terms is regrouped as a union (a
+disjunction), the others are all intersected (conjunction). If a term for a
+package does not exist in one incompatibility, it can safely be replaced by the
+term \\( \neg [\varnothing] \\) in the expression above as we have already
+explained before.