Add prettier and improve CI (#13)

* Add prettier and improve CI

To keep a consistent style with multiple editors, and to avoid manual reflowing of text, we add prettier as formatter for markdown and yml files.

I've intentionally left everything at default settings to rely on the work defining a good standard done by prettier's team and to avoid bikeshedding over the style.

The only non-default option is prose wrapping for markdown files, which adds the equivalent of a line length limit as we have it in rust and yaml to markdown, too. I find too long lines hard to read and soft-wrap isn't consistently available (e.g. github PR diffs become hard to read), though we could remove that option, too.

Prettier is enforced by CI. On CI, we also build the book for all PRs with an updated mdbook version and check compatibility with the latest mdbook version (non-blocking).

* Adds names to jobs

* Don't run CI twice for PRs

Author: konstin

.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.