diff --git a/.codespellrc b/.codespellrc new file mode 100644 index 0000000..604a0d7 --- /dev/null +++ b/.codespellrc @@ -0,0 +1,5 @@ +[codespell] +skip = .git,target,node_modules,dist,*.yaml,*.lock,./book/book,*.min.js +ignore-words-list = implementor,implementors,ser,crate +count = +quiet-level = 3 diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml new file mode 100644 index 0000000..3c0d424 --- /dev/null +++ b/.github/workflows/book.yml @@ -0,0 +1,28 @@ +name: publish-tutorial + +on: + commit: + branches: + - "main" + +jobs: + tutorial: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + + - name: Install Nix + uses: cachix/install-nix-action@v17 + with: + extra_nix_config: | + access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} + + - name: Build Tutorial + run: nix develop --command cd book && mdbook build + + - uses: JamesIves/github-pages-deploy-action@v4.3.0 + with: + token: ${{ secrets.GITHUB_TOKEN }} + branch: gh-pages + folder: ./book/book + clean: true diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bb914e1..f16a1f8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -14,12 +14,13 @@ jobs: test: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - - name: Setup - uses: ./.github/workflows/setup - - - name: Argus tests - uses: actions-rs/cargo@v1 + - name: Install Nix + uses: cachix/install-nix-action@v17 with: - command: test + extra_nix_config: | + access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} + + - name: Argus Test + run: nix develop --command ci-test diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index e440ffd..efa73ba 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -10,37 +10,33 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 - - uses: actions-rs/install@v0.1 + - name: Install Nix + uses: cachix/install-nix-action@v17 with: - crate: cargo-workspaces - version: latest - use-tool-cache: true - - name: Setup - uses: ./.github/workflows/setup - - run: cargo ws publish skip --no-remove-dev-deps --from-git --yes --token ${{ secrets.CRATES_IO }} + extra_nix_config: | + access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} + - run: nix develop --command \ + cargo ws publish skip --no-remove-dev-deps --from-git --yes --token ${{ secrets.CRATES_IO }} publish-ide: runs-on: ubuntu-latest needs: publish-crates steps: - uses: actions/checkout@v3 - - uses: actions/setup-node@v4 + - name: Install Nix + uses: cachix/install-nix-action@v17 with: - node-version: 20 + extra_nix_config: | + access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} - - name: Setup - uses: ./.github/workflows/setup + - name: Build TS bindings + run: nix develop --command cargo make init-bindings - - name: Publish to Open VSX Registry - uses: HaaLeo/publish-vscode-extension@v1 - id: publishToOpenVSX - with: - pat: ${{ secrets.OVSX_MRKT }} - packagePath: "./ide/packages/extension" + - name: Build VSIX + run: nix develop --command cd ide/packages/extension && vsce package - - name: Publish to Visual Studio Marketplace - uses: HaaLeo/publish-vscode-extension@v1 - with: - pat: ${{ secrets.VSCODE_MRKT }} - registryUrl: https://marketplace.visualstudio.com - packagePath: "./ide/packages/extension" + - name: Publish VS Code Marketplace + run: nix develop --command cd ide/packages/extension && vsce publish -p ${{ secrets.VSCODE_MRKT }} --packagePath *.vsix + + - name: Publish OVSX Marketplace + run: nix develop --command cd ide/packages/extension && pnpx ovsx publish *.vsix -p ${{ secrets.OVSX_MRKT }} diff --git a/.github/workflows/setup/action.yml b/.github/workflows/setup/action.yml deleted file mode 100644 index f1d953b..0000000 --- a/.github/workflows/setup/action.yml +++ /dev/null @@ -1,33 +0,0 @@ -name: setup -runs: - using: composite - steps: - - uses: actions/checkout@v3 - - - uses: davidB/rust-cargo-make@v1 - with: - version: '0.36.4' - - - name: Install Guile - run: sudo apt-get install -y guile-3.0 - shell: bash - - - name: Install Depot - run: curl https://raw.githubusercontent.com/cognitive-engineering-lab/depot/main/scripts/install.sh | sh - shell: bash - - - name: Install Test Libraries - run: sudo apt-get install -y libasound2-dev libudev-dev - shell: bash - - - name: Gen bindings - run: cargo make init-bindings - shell: bash - - - name: Prepare IDE - run: cd ide && depot build - shell: bash - - - name: Install Argus - run: cargo install --path crates/argus-cli --debug --locked - shell: bash diff --git a/.gitignore b/.gitignore index dced3e1..2edd08e 100644 --- a/.gitignore +++ b/.gitignore @@ -17,7 +17,6 @@ gha-creds-*.json /org/meeting* /org/*.png /org/media/ -sample-book/ # Rust things target/ diff --git a/book/.envrc b/book/.envrc deleted file mode 100644 index a5dbbcb..0000000 --- a/book/.envrc +++ /dev/null @@ -1 +0,0 @@ -use flake . diff --git a/book/book.toml b/book/book.toml index 8214726..e765ce2 100644 --- a/book/book.toml +++ b/book/book.toml @@ -6,10 +6,20 @@ src = "src" title = "Argus: a trait debugger for Rust" [output.html] +default-theme = "light" + curly-quotes = true additional-js = ["mermaid.min.js", "mermaid-init.js"] +additional-css = ["./mdbook-admonish.css"] [preprocessor] +[preprocessor.image-size] +command = "mdbook-image-size" + [preprocessor.mermaid] command = "mdbook-mermaid" + +[preprocessor.admonish] +command = "mdbook-admonish" +assets_version = "3.0.2" # do not edit: managed by `mdbook-admonish install` diff --git a/book/flake.lock b/book/flake.lock deleted file mode 100644 index 5e1e2f1..0000000 --- a/book/flake.lock +++ /dev/null @@ -1,61 +0,0 @@ -{ - "nodes": { - "flake-utils": { - "inputs": { - "systems": "systems" - }, - "locked": { - "lastModified": 1710146030, - "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "nixpkgs": { - "locked": { - "lastModified": 1724224976, - "narHash": "sha256-Z/ELQhrSd7bMzTO8r7NZgi9g5emh+aRKoCdaAv5fiO0=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "c374d94f1536013ca8e92341b540eba4c22f9c62", - "type": "github" - }, - "original": { - "owner": "nixos", - "ref": "nixos-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, - "root": { - "inputs": { - "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs" - } - }, - "systems": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "owner": "nix-systems", - "repo": "default", - "type": "github" - } - } - }, - "root": "root", - "version": 7 -} diff --git a/book/flake.nix b/book/flake.nix deleted file mode 100644 index 6ec3208..0000000 --- a/book/flake.nix +++ /dev/null @@ -1,21 +0,0 @@ -{ - inputs = { - nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; - flake-utils.url = "github:numtide/flake-utils"; - }; - - outputs = { self, nixpkgs, flake-utils }: - flake-utils.lib.eachDefaultSystem (system: - let - pkgs = import nixpkgs { - inherit system; - }; - in { - devShell = with pkgs; mkShell { - buildInputs = [ - mdbook - mdbook-mermaid - ]; - }; - }); -} diff --git a/book/mdbook-admonish.css b/book/mdbook-admonish.css new file mode 100644 index 0000000..45aeff0 --- /dev/null +++ b/book/mdbook-admonish.css @@ -0,0 +1,348 @@ +@charset "UTF-8"; +:is(.admonition) { + display: flow-root; + margin: 1.5625em 0; + padding: 0 1.2rem; + color: var(--fg); + page-break-inside: avoid; + background-color: var(--bg); + border: 0 solid black; + border-inline-start-width: 0.4rem; + border-radius: 0.2rem; + box-shadow: 0 0.2rem 1rem rgba(0, 0, 0, 0.05), 0 0 0.1rem rgba(0, 0, 0, 0.1); +} +@media print { + :is(.admonition) { + box-shadow: none; + } +} +:is(.admonition) > * { + box-sizing: border-box; +} +:is(.admonition) :is(.admonition) { + margin-top: 1em; + margin-bottom: 1em; +} +:is(.admonition) > .tabbed-set:only-child { + margin-top: 0; +} +html :is(.admonition) > :last-child { + margin-bottom: 1.2rem; +} + +a.admonition-anchor-link { + display: none; + position: absolute; + left: -1.2rem; + padding-right: 1rem; +} +a.admonition-anchor-link:link, a.admonition-anchor-link:visited { + color: var(--fg); +} +a.admonition-anchor-link:link:hover, a.admonition-anchor-link:visited:hover { + text-decoration: none; +} +a.admonition-anchor-link::before { + content: "§"; +} + +:is(.admonition-title, summary.admonition-title) { + position: relative; + min-height: 4rem; + margin-block: 0; + margin-inline: -1.6rem -1.2rem; + padding-block: 0.8rem; + padding-inline: 4.4rem 1.2rem; + font-weight: 700; + background-color: rgba(68, 138, 255, 0.1); + print-color-adjust: exact; + -webkit-print-color-adjust: exact; + display: flex; +} +:is(.admonition-title, summary.admonition-title) p { + margin: 0; +} +html :is(.admonition-title, summary.admonition-title):last-child { + margin-bottom: 0; +} +:is(.admonition-title, summary.admonition-title)::before { + position: absolute; + top: 0.625em; + inset-inline-start: 1.6rem; + width: 2rem; + height: 2rem; + background-color: #448aff; + print-color-adjust: exact; + -webkit-print-color-adjust: exact; + mask-image: url('data:image/svg+xml;charset=utf-8,'); + -webkit-mask-image: url('data:image/svg+xml;charset=utf-8,'); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-size: contain; + content: ""; +} +:is(.admonition-title, summary.admonition-title):hover a.admonition-anchor-link { + display: initial; +} + +details.admonition > summary.admonition-title::after { + position: absolute; + top: 0.625em; + inset-inline-end: 1.6rem; + height: 2rem; + width: 2rem; + background-color: currentcolor; + mask-image: var(--md-details-icon); + -webkit-mask-image: var(--md-details-icon); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-size: contain; + content: ""; + transform: rotate(0deg); + transition: transform 0.25s; +} +details[open].admonition > summary.admonition-title::after { + transform: rotate(90deg); +} + +:root { + --md-details-icon: url("data:image/svg+xml;charset=utf-8,"); +} + +:root { + --md-admonition-icon--admonish-note: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-abstract: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-info: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-tip: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-success: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-question: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-warning: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-failure: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-danger: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-bug: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-example: url("data:image/svg+xml;charset=utf-8,"); + --md-admonition-icon--admonish-quote: url("data:image/svg+xml;charset=utf-8,"); +} + +:is(.admonition):is(.admonish-note) { + border-color: #448aff; +} + +:is(.admonish-note) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(68, 138, 255, 0.1); +} +:is(.admonish-note) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #448aff; + mask-image: var(--md-admonition-icon--admonish-note); + -webkit-mask-image: var(--md-admonition-icon--admonish-note); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-abstract, .admonish-summary, .admonish-tldr) { + border-color: #00b0ff; +} + +:is(.admonish-abstract, .admonish-summary, .admonish-tldr) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(0, 176, 255, 0.1); +} +:is(.admonish-abstract, .admonish-summary, .admonish-tldr) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #00b0ff; + mask-image: var(--md-admonition-icon--admonish-abstract); + -webkit-mask-image: var(--md-admonition-icon--admonish-abstract); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-info, .admonish-todo) { + border-color: #00b8d4; +} + +:is(.admonish-info, .admonish-todo) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(0, 184, 212, 0.1); +} +:is(.admonish-info, .admonish-todo) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #00b8d4; + mask-image: var(--md-admonition-icon--admonish-info); + -webkit-mask-image: var(--md-admonition-icon--admonish-info); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-tip, .admonish-hint, .admonish-important) { + border-color: #00bfa5; +} + +:is(.admonish-tip, .admonish-hint, .admonish-important) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(0, 191, 165, 0.1); +} +:is(.admonish-tip, .admonish-hint, .admonish-important) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #00bfa5; + mask-image: var(--md-admonition-icon--admonish-tip); + -webkit-mask-image: var(--md-admonition-icon--admonish-tip); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-success, .admonish-check, .admonish-done) { + border-color: #00c853; +} + +:is(.admonish-success, .admonish-check, .admonish-done) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(0, 200, 83, 0.1); +} +:is(.admonish-success, .admonish-check, .admonish-done) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #00c853; + mask-image: var(--md-admonition-icon--admonish-success); + -webkit-mask-image: var(--md-admonition-icon--admonish-success); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-question, .admonish-help, .admonish-faq) { + border-color: #64dd17; +} + +:is(.admonish-question, .admonish-help, .admonish-faq) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(100, 221, 23, 0.1); +} +:is(.admonish-question, .admonish-help, .admonish-faq) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #64dd17; + mask-image: var(--md-admonition-icon--admonish-question); + -webkit-mask-image: var(--md-admonition-icon--admonish-question); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-warning, .admonish-caution, .admonish-attention) { + border-color: #ff9100; +} + +:is(.admonish-warning, .admonish-caution, .admonish-attention) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(255, 145, 0, 0.1); +} +:is(.admonish-warning, .admonish-caution, .admonish-attention) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #ff9100; + mask-image: var(--md-admonition-icon--admonish-warning); + -webkit-mask-image: var(--md-admonition-icon--admonish-warning); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-failure, .admonish-fail, .admonish-missing) { + border-color: #ff5252; +} + +:is(.admonish-failure, .admonish-fail, .admonish-missing) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(255, 82, 82, 0.1); +} +:is(.admonish-failure, .admonish-fail, .admonish-missing) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #ff5252; + mask-image: var(--md-admonition-icon--admonish-failure); + -webkit-mask-image: var(--md-admonition-icon--admonish-failure); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-danger, .admonish-error) { + border-color: #ff1744; +} + +:is(.admonish-danger, .admonish-error) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(255, 23, 68, 0.1); +} +:is(.admonish-danger, .admonish-error) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #ff1744; + mask-image: var(--md-admonition-icon--admonish-danger); + -webkit-mask-image: var(--md-admonition-icon--admonish-danger); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-bug) { + border-color: #f50057; +} + +:is(.admonish-bug) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(245, 0, 87, 0.1); +} +:is(.admonish-bug) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #f50057; + mask-image: var(--md-admonition-icon--admonish-bug); + -webkit-mask-image: var(--md-admonition-icon--admonish-bug); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-example) { + border-color: #7c4dff; +} + +:is(.admonish-example) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(124, 77, 255, 0.1); +} +:is(.admonish-example) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #7c4dff; + mask-image: var(--md-admonition-icon--admonish-example); + -webkit-mask-image: var(--md-admonition-icon--admonish-example); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +:is(.admonition):is(.admonish-quote, .admonish-cite) { + border-color: #9e9e9e; +} + +:is(.admonish-quote, .admonish-cite) > :is(.admonition-title, summary.admonition-title) { + background-color: rgba(158, 158, 158, 0.1); +} +:is(.admonish-quote, .admonish-cite) > :is(.admonition-title, summary.admonition-title)::before { + background-color: #9e9e9e; + mask-image: var(--md-admonition-icon--admonish-quote); + -webkit-mask-image: var(--md-admonition-icon--admonish-quote); + mask-repeat: no-repeat; + -webkit-mask-repeat: no-repeat; + mask-size: contain; + -webkit-mask-repeat: no-repeat; +} + +.navy :is(.admonition) { + background-color: var(--sidebar-bg); +} + +.ayu :is(.admonition), +.coal :is(.admonition) { + background-color: var(--theme-hover); +} + +.rust :is(.admonition) { + background-color: var(--sidebar-bg); + color: var(--sidebar-fg); +} +.rust .admonition-anchor-link:link, .rust .admonition-anchor-link:visited { + color: var(--sidebar-fg); +} diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 18bff22..6640634 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -2,9 +2,9 @@ [Introduction](README.md) +- [Whirlwind Tour](whirlwind.md) + - [Trait Debugging 101](trait-debugging-101.md) - [Trait Methods and Typestate]() -- [Advanced Trait Solving]() - diff --git a/book/src/trait-debugging-101.md b/book/src/trait-debugging-101.md index a44c850..a5bd6cb 100644 --- a/book/src/trait-debugging-101.md +++ b/book/src/trait-debugging-101.md @@ -4,7 +4,11 @@ Traits are a pervasive language feature in Rust: Copying, printing, indexing, mu Static checks and type safety is great, but compiler errors can become increasingly complex alongside the types and traits you use. This guide serves to teach "trait debugging" in Rust, using a new tool, Argus, developed by the Cognitive Engineering Lab at Brown University. -> If you're already familiar with traits and trait solving, [click here](#your-first-web-server) to start debugging. +```admonish info +If you're already familiar with the process of trait solving, [click here](#your-first-web-server) to dive straight into start debugging. + +However if you're **participating** in a user study with us, please read this section. +``` Traits define units of *shared behavior* and serve a similar purpose as Java interfaces. In Java, you would declare an interface with a given name, and list some number of functions for which the interface implementors need to provide an implementation. Below is an example definition of a `Year`, simply a wrapper around an integer, that implements `Comparable`, meaning a year is only comparable to other years. @@ -14,7 +18,7 @@ interface Comparable { } class Year implements Comparable { - private int raw_year; + private int rawYear; int compareTo(Year that) { // ... implementation elided ... @@ -40,19 +44,23 @@ impl Comparable for Year { } ``` -Notice in Rust that the trait implementation and struct definition are *separate.* In the Java example we both defined the class `Year` and declared it an implementor using the one line `class Year implements Comparable`. In Rust, we defined the struct `Year`, and separately provided its implementation for the `Comparable` trait. The separation between definition and trait implementation means that for the compiler to answer the question `Year: Comparable`, it must *search* for the relevant implementation block. If no block exists, or if multiple blocks exist, this is a type error. The component inside the compiler responsible for this search is called the *trait solver*. +Notice in Rust that the trait implementation and struct definition are *separate.* In the Java example we both defined the class `Year` and declared it an implementor using a single line. In Rust, we defined the struct `Year`, and separately provided its implementation for the `Comparable` trait. The separation between definition and trait implementation means that for the compiler to answer the question "Does `Year` implement `Comparable`?" it must *search* for the relevant implementation block. If no block exists, or if multiple blocks exist, this is a type error. We call The component inside the compiler responsible for this search the *trait solver*. ## An Overview of The Trait Solver -The trait solver has a single goal: respond to questions about types implementing traits. Here's some examples of how the trait solver can be invoked, and what the solver would say in response. +The trait solver has a single goal: respond to questions about types implementing traits. These so called "questions" come from trait bounds, the Rust syntax looks like this: `Year: Comparable`. This trait bound says that `Year` must implement `Comparable`. In this post we refer to bounds as questions, "does `Year` implement `Comparable`?" We do this because the trait solver is only responsible for answering questions, not determining if an 'No' answer becomes a type error. Here's some examples of questions the trait solver can get, and how the solver would respond. - Does `Year: Comparable` hold? *Response: No* +- Does `Year: Sized` hold? *Response: Yes* + - Does `Year: Comparable` hold? *Response: Yes* - Does `Year: Comparable` hold? *Response: Maybe, if `T = Year`* -If the response is *maybe*, as in the third example above, the compiler will perform extra inference to check if `T = Year`, if it isn't, that is a type error. After reading this section you should know how the Rust trait solver determines its response to a question. +If the response is *maybe*, as in the third example above, the compiler will perform extra inference to check if `T = Year`, if it isn't, then it may become a type error. After reading this section you should know how the Rust trait solver determines its response to a question. + +### A simple algorithm for trait solving The steps to respond for a question `Ty: Trait` proceed as follows. @@ -71,6 +79,13 @@ The steps to respond for a question `Ty: Trait` proceed as follows. if `T` and `Ty` *unify*, restart from (1) with the question `Constrint_i`. Respond with *yes* if all constraint responses are *yes*. + You may not know what I mean with "if they unify," so let's go over some examples. Two types unify in the trait solver if we can instantiate type variables such that they are equivalent. + + - `String` and `Year` don't unify + - `T` and `Year` unify because `T` is a type variable. So if `T = Year`, then they're equivalent + - `Vec` and `Vec` unify if `T = String` + - `Vec` and `Vec` unify if `U = T` + 3. Respond with *yes* if exactly one implementation block responded with *yes*. Notice that these steps are recursive. Checking the constrain from a where block starts the process over again, as if it were the original question. Listed in prose the process may seem confusing, but we think it's more enlightening as a diagram. Consider the `Comparable` trait, we'll extend the previous program with one more implementation block as shown below. @@ -93,8 +108,8 @@ impl Comparable for Year { // NEW implementation impl Comparable for T where - T: Into, - U: Into, + T: ToString, + U: ToString, { fn compare_to(&self, o: &U) -> i32 { // ... implementation elided ... @@ -108,56 +123,48 @@ Let's consider how the trait solver would go about responding to the question `Y ```mermaid graph TD; root["Year: Comparable<Year>"] - implPar["impl Comparable<U> for T"] - toStr0["Year: Into<String>"] - toStr1["Year: Into<String>"] - implCon["impl Comparable<Year> for Year"] - succ["✔"] - fail0["❌"] - fail1["❌"] - + implPar["impl Comparable<U> for T\nwhere\n    T: ToString\n    U: ToString"] + toStr0["❌ Year: ToString"] + toStr1["❌ Year: ToString"] + implCon["✔ impl Comparable<Year> for Year"] + root -.-> implPar implPar --T = Year--> toStr0 implPar --U = Year--> toStr1 - toStr0 --> fail0 - toStr1 --> fail1 root -.-> implCon - implCon --> succ - linkStyle 0,1,2,3,4 stroke:red - linkStyle 5,6 stroke:green, stroke-width:4px -``` + classDef default fill:#fafafa, stroke-width:3px, text-align:left + classDef cssSuccess stroke:green + classDef cssFailure stroke:red -In the above diagram the dotted lines represent an "Or" relationship with child and parent. That is, exactly one of the child blocks needs to respond with "yes." We see these lines coming from the root question and extending to the implementation blocks. This models step (3) in the listed algorithm because one of the implementation blocks must match, no more and no fewer. + class root,implCon cssSuccess + class implPar,toStr0,toStr1 cssFailure -Solid lines represent "And" relationships, in other words every child with a solid line must respond with "yes." + linkStyle 0,1,2 stroke:red + linkStyle 3 stroke:green, stroke-width:4px +``` -TODO: finish this thought +In the above diagram the dotted lines represent an **Or** relationship between parent and child. That is, exactly one of the child blocks needs to respond with "yes." We see these lines coming from the root question and extending to the implementation blocks. Implementation blocks always form an Or relationship with their parents.This models step (3) in the listed algorithm because one of the implementation blocks must match, no more and no fewer. +Solid lines represent **And** relationships between parent and child. That is, every one of the child blocks needs to respond with "yes." We see these lines coming from implementation blocks and extending to the constraints. Constraints always form an And relationship because all the constraints in a where clause must hold. -## Your First Web Server +```admonish question +**Why did the trait solver check the implementation block for `T` when there exists one directly for `Year`?** -To do some real debugging we should to use a real crate. Axum is a popular Rust web application framework and we're going to use it to build a web server. Here's some starting code for the server, if you want to follow along locally, which we recommend doing, the code is [available on GitHub](TODO). +The trait solver must consider all potentially matching implementation blocks. Because `T` unifies with `Year`, the trait solver must check this block as well. Remember, if multiple end up working then that *is also* an error, an ambiguous trait usage. Exactly one implementation block must match for there to be a success. +``` -```rust -use axum::{routing::get, Router, body::Bytes}; +A neat pattern to observe is that a question always has a implementation block as a child, with a dotted line. We can never have two questions in a row; you shouldn't answer a question with a question! Implementation blocks always have a question as a child, with a solid line. If you follow a specific path in the tree the pattern of relationships will be "Or, And, Or, And, Or, And, …" -struct LoginAttempt { - user_id: u64, - password: String, -} +The tree diagram above actually has a name, it's called the *search tree*. Search trees represent the execution of the trait solver! Just as you may have traced your own programs to debug strange behavior, we can trace the trait solver to help us understand why a particular outcome occurred. Search trees are the core data structure used in the Argus trait debugger, let's size up to a real example and see how we can use Argus to do some trait debugging. -fn login(attempt: LoginAttempt) -> bool { - todo!() -} -#[tokio::main] -async fn main() { - let app = Router::new().route("/login", get(login)); +## Your First Web Server - let listener = tokio::net::TcpListener::bind("0.0.0.0:3000").await.unwrap(); - axum::serve(listener, app).await.unwrap(); -} +To do some real debugging we should use a real crate. Axum is a popular Rust web application framework and we're going to use it to build a web server. Here's some starting code for the server + +```rust,compile_fail,noplayground +{{#include ../../examples/hello-server/src/main.rs}} ``` Unfortunately, our server does not work! Compiling the above code results in the ambiguous error diagnostic @@ -177,27 +184,68 @@ error[E0277]: the trait bound `fn(LoginAttempt) -> bool {login}: Handler<_, _>` note: required by a bound in `axum::routing::get` ``` -The above diagnostic, in a long-winded way, is telling us that the function `login` does not implement `Handler`. As the authors, we *intended* to use `login` as a handler, so I'm stumped why it doesn't. +The above diagnostic, in a long-winded way, tells us that the function `login` does not implement `Handler`. As the authors, we *intended* to use `login` as a handler, so I'm stumped why it doesn't. + +```admonish note +Going forward we will write `{login}` to abbreviate the type of `login`, `fn(LoginAttempt) -> bool`, which is far too verbose to repeat over and over. +``` -> TODO: describe the process of trait resolution. It should answer the following questions: -> What is the Trait Solver? -> How does the trait solver try to resolve predicates? (This should roughly be "how does Prolog resolution work" ;)) -> What does Top-Down mean (with pictures) -> What does Bottom-Up mean (with pictures) +Fortunately, Argus is coming to the rescue! -Fortunately, Argus is coming to the rescue! If you're following along locally, open the provided crate in VS Code (or an Argus-compatible editor of choice) and let's get started. + ## Through the Search Tree -The diagnostic from rustc isn't totally useless; we learned that the type `fn(LoginAttempt) -> bool`, the signature of `login`, should implement the Axum trait `Handler`. Additionally, we know that this bound was introduced by the call `get(login)`. This information is useful, but it fails to answer why `login` doesn't implement `Handler`. +The diagnostic from rustc isn't totally useless; we learned that the type `fn(LoginAttempt) -> bool`, the signature of `login`, should implement the Axum trait `Handler`. Additionally, we know that this bound was introduced by the call `get(login)`. Both pieces of information help us get started, but fail to answer why `login` doesn't implement `Handler`. + +To help us inspect the problem, we will look at the *search tree* produced by the trait solver. The search tree is exposed in the Argus VS Code extension, and for now we'll be looking at the "Top-Down" view. + +````admonish example +Before jumping into the Argus interface for search trees, I will show you the initial search tree in the familiar diagrammatic notation. This tree was produced by type checking the above code and explains the same error as the included diagnostic message. + +```mermaid +--- +title: Search tree produced by the Axum trait error +--- +graph TD + root["{login}: Handler<_, _>"] + implRespH["impl Handler for T\nwhere\n    T: IntoResponse"] + intoResp["{login}: IntoResponse"] + implH["impl Handler for F\nwhere\n    F: FnOnce(T1) -> Fut,\n    Fut: Future + Send,\n    T1: FromRequest"] + isFunc["{login}: FnOnce(LoginAttempt) -> bool"] + boolFut["bool: Future"] + loginARqst["LoginAttempt: FromRequest<_, _>"] + + root -.-> implRespH + implRespH --T = {login}--> intoResp + root -.-> implH + implH --F = {login}, T1 = LoginAttempt, Fut = bool--> isFunc + implH --Fut = bool--> boolFut + implH --T1 = LoginAttempt--> loginARqst + + class root,implRespH,intoResp,implH,boolFut,loginARqst cssFailure + class isFunc cssSuccess + + classDef default fill:#fafafa, stroke-width:3px, text-align:left + classDef cssSuccess stroke:green + classDef cssFailure stroke:red + linkStyle 0,1,2,4,5 stroke:red + linkStyle 3 stroke:green, stroke-width:4px +``` +> Elided are a few trivial bounds like `Sized` and `Send` that held true, but clutter the diagram. Don't panic if you open the Argus panel and see a few things that aren't shown here. -To help us inspect the problem, we will look at the search tree produced by the Rust trait solver. The search tree is exposed in the Argus VS Code extension as the "Top-Down" view. +When traversing a tree it's natural to start at the root, and following the direction of the arrows, move from top downward. In the Argus panel we call this default view the "Top-Down" view, which highlights the direction of traversal when you expand the nodes. +```` -![Search tree initial bound](assets/axum-hello-server/top-down-root-highlighted.png) +Notice that the compiler diagnostic produced by Rust mentioned the *root question*, `{login}: Handler<_, _>`, instead of the failing nodes at the tree leaves. The Rust compiler is conservative, so it doesn't want to accidentally assume you had a particular intention. In the diagram there are two potentially matching implementation blocks. There's one for a function with a single argument, and there's one for things that implement `IntoResponse`. It turns out the latter is useful if you want a handler that returns the same static value on every request; instead of using a function, you can simply write the static value and Axum will turn that into a handler as well. However, the second implementation option means Rust can't decide which is the actual error! Should it report `{login}: IntoResponse`, or the set `bool: Future` and `LoginAttempt: FromRequest<_, _>`? Instead of deciding, Rust will choose the node that unifies all the failures, which for this particular goal, is just the root node of the tree. -The trait search tree always starts with a trait bound, which we read like questions. For example `String: Display` reads "Does `String` implement `Display`?" In our case, that question is the same failing trait bound that appeared in the Rust error diagnostic, `fn(LoginAttempt) -> bool: Handler<_, _>`, and it's highlighted in orange in the above search tree. +Now that you've seen the search tree in diagram form. Let's walk through the search tree using the Argus interface representation. -> For brevity we will abbreviate types of functions as `{login}: Handler<_, _>`, where `{login}` reads as "the type of `login`", which is in this case `fn(LoginAttempt) -> bool`. +![Search tree initial bound](assets/axum-hello-server/top-down-root-highlighted.png =600x center) + +The trait search tree always starts with a trait bound, which as previously stated, we read like questions. For example `String: Display` reads "Does `String` implement `Display`?" The root question for the search is highlighted in orange in the above. For a type to implement a trait there must be a matching *implementation block*. Implementation blocks come in two flavors, non-parameterized implementations and parameterized implementations. @@ -219,7 +267,7 @@ are parameterized by types, like the type parameter `T` in the above. Parameteri Let's bring the conversation back to our problem. Rust finds an appropriate implementation block that matches the initial trait bound ([RustDoc link](https://docs.rs/axum/latest/axum/handler/trait.Handler.html#impl-Handler%3C(M,+T1),+S%3E-for-F)). This is highlighted below in green. -![Search tree found impl](assets/axum-hello-server/top-down-impl-highlighted.png) +![Search tree found impl](assets/axum-hello-server/top-down-impl-highlighted.png =600x center) In order to use this implementation block to satisfy the root trait bound, `{login}: Handler<_, _>`, Rust now needs to satisfy all of the conditions in the where clause. The trait solver performs the following steps following the list of constraints in the where clause. @@ -231,7 +279,7 @@ In order to use this implementation block to satisfy the root trait bound, `{log This failing bound tells us that the output of the function needs to be a future. Argh, 🤦 we forgot to make the handler function asynchronous! What a silly mistake. However, before we jump back to our code and fix the issue, let's reflect on the Argus interface and see how we could have reached this same conclusion faster. -![Search tree found impl](assets/axum-hello-server/top-down-error-highlighted.png) +![Search tree found impl](assets/axum-hello-server/top-down-error-highlighted.png =600x center) The screenshots included so far of the trait search tree are from the Top-Down view in Argus. This means we view the search just as Rust performed it: We started at the root question `{login}: Handler<_, _>`, descended into the implementation blocks, and found the failing where-clause in a tree leaf. This failing leaf is highlighted in the above image in red. There's also another failing trait bound, `LoginAttempt: FromRequest<_, _>`, which we'll come back to in a moment. The insight is that all of the errors reside in the search tree *leaves,* so the Top-Down view doesn't show you the errors first but rather the process Rust went through to find the errors. The process is helpful to know which implementation blocks and trait bounds were involved from tree root to failing leaf. @@ -242,7 +290,46 @@ What if you want to see the errors first? Lucky for you, Argus provides a second -The above video demonstrates that Argus identifies `bool: Future` as a root cause of the overall failure, but also the second failure `LoginAttempt: FromRequestParts<_, _>`. Argus also indicates that these two failing trait bounds need to be resolved *together* to satisfy the root bound, `{login}: Handler<_, _>`. We'll first make the function `login` asynchronous, now let's get on to fixing the second failing bound: `{login}: Handler<_, _>`. + +````admonish example +The Bottom-Up view is what you'd get by *inverting* the search tree. That is, you start at the leaves and traverse to the root. This may be easier to see with the diagram from before, but we'll invert all the edges and present it bottom up. + +```mermaid +--- +title: Bottom-Up view of the search tree. +--- +graph TD + root["{login}: Handler<_, _>"] + implRespH["impl Handler for T\nwhere\n    T: IntoResponse"] + intoResp["{login}: IntoResponse"] + implH["impl Handler for F\nwhere\n    F: FnOnce(T1) -> Fut,\n    Fut: Future + Send,\n    T1: FromRequest"] + isFunc["{login}: FnOnce(LoginAttempt) -> bool"] + boolFut["bool: Future"] + loginARqst["LoginAttempt: FromRequest<_, _>"] + + + implRespH -.-> root + intoResp --> implRespH + implH -.-> root + isFunc --> implH + boolFut --> implH + loginARqst --> implH + + class root,implRespH,intoResp,implH,boolFut,loginARqst cssFailure + class isFunc cssSuccess + + classDef default fill:#fafafa, stroke-width:3px, text-align:left + classDef cssSuccess stroke:green + classDef cssFailure stroke:red + linkStyle 0,1,2,4,5 stroke:red + linkStyle 3 stroke:green, stroke-width:4px +``` +The bottom up view in Argus always shows you the leaves that failed. By expanding the tree nodes you traverse the path from tree leaf to root, this shows you the *provenance* of a failing bound, or in other words from where the failing bound originated. + +In the Bottom-Up view Argus also sorts the failing leaves by which are "most-likely" to the error you should debug. No tool is perfect, and Argus can be wrong! If you click on "Other failures," which appears below the first shown failure, Argus provides you the full list of failures. +```` + +The above video demonstrates that Argus identifies `bool: Future` as a root cause of the overall failure, but also the second failure `LoginAttempt: FromRequestParts<_, _>`. Argus also indicates that these two failing trait bounds need to be resolved *together* to satisfy the root bound, `{login}: Handler<_, _>`. ## Fixing Trait Bounds with Argus @@ -250,7 +337,7 @@ The above video demonstrates that Argus identifies `bool: Future` as a root caus -It turns out there are a lot of problems with our handler. Above is a video demonstrating that after marking the `login` function asynchronous, the bound `bool: IntoResponse` is unsatisfied. This happened because the associated type `Output` of the `Future`, in this case our boolean, needs to implement `IntoResponse`. The video demonstrates additional ways in which you can use Argus for debugging. +It turns out there are a lot of problems with our handler. Above is a video demonstrating that after marking the `login` function asynchronous, the bound `bool: IntoResponse` remains unsatisfied. This happened because the associated type `Output` of the `Future`, in this case our boolean, needs to implement `IntoResponse`. The video demonstrates additional ways in which you can use Argus for debugging. 1. We expanded the Bottom Up view to see the lineage of implementation blocks used to arrive at the failure. In this case there was only one between the root bound and the failing leaf, but we looked at the constraints in the where clause to find the origin of the bound. @@ -270,7 +357,7 @@ The above video contains a lot of information. Let's break down what happened. - Implementing `FromRequestParts` didn't seem feasible, but we never checked why this bound was introduced. Expanding the Bottom Up view revealed that the bound `FromRequest` was introduced in a where clause of the `Handler`, and that `FromRequestParts` was an attempt to satisfy the `FromRequest` bound. Here's an image from the Top Down view that shows this same lineage. - ![FromRequestParts provenance](assets/axum-hello-server/from-rqst-prts-annotated.png) + ![FromRequestParts provenance](assets/axum-hello-server/from-rqst-prts-annotated.png =600x center) What happened is the implementation block `impl FromRequest for T ...` unified `T` and `LoginAttempt`. But if we can satisfy the bound `LoginAttempt: FromRequest<_, _>` this also fixes the trait error. @@ -280,7 +367,9 @@ The above video contains a lot of information. Let's break down what happened. Finally, after all of these errors inserted by our initial careless typing, we have fixed all trait errors. -> Note, when Argus doesn't see any failing obligations it may prompt you to open a bug report. Argus is research software and sometimes it might not show failing obligations when you expect there to be some; this scenario would be a bug and we'd appreciate a report. If the code does type check, happily close the Argus window and move on with your programming endeavors. +```admonish note +When Argus doesn't see any failing obligations it will prompt you to open a bug report. Argus is research software and sometimes doesn't show failing obligations when you expect there to be some; this scenario would be a bug and we'd appreciate a report. If the code **successfully** type checks, happily close the Argus window and move on with your programming endeavors. +``` # Wrapping up diff --git a/book/src/whirlwind.md b/book/src/whirlwind.md new file mode 100644 index 0000000..1185010 --- /dev/null +++ b/book/src/whirlwind.md @@ -0,0 +1 @@ +# Whirlwind Tour diff --git a/crates/argus-ser/src/lib.rs b/crates/argus-ser/src/lib.rs index 9fb6e80..56f1e61 100644 --- a/crates/argus-ser/src/lib.rs +++ b/crates/argus-ser/src/lib.rs @@ -18,7 +18,7 @@ //! If a type requires expansion into a richer form, this is done inside the `new` function. //! //! If a type needs to be used within a serde `with` attribute, then an associated function -//! `serialize` is defined, and actual serialization will be deffered to the `serialize` +//! `serialize` is defined, and actual serialization will be deferred to the `serialize` //! extension method. //! //! If you need to serialize an optional type then prefix it with `Option__`, and diff --git a/crates/argus-ser/src/path/default.rs b/crates/argus-ser/src/path/default.rs index e197c7b..aa633ad 100644 --- a/crates/argus-ser/src/path/default.rs +++ b/crates/argus-ser/src/path/default.rs @@ -1,4 +1,4 @@ -//! Default implementaitons from `rustc_middle::ty::print` +//! Default implementations from `rustc_middle::ty::print` use rustc_data_structures::sso::SsoHashSet; use rustc_hir::{def_id::DefId, definitions::DefPathData}; diff --git a/crates/argus-ser/src/ty.rs b/crates/argus-ser/src/ty.rs index 1ace998..edaad43 100644 --- a/crates/argus-ser/src/ty.rs +++ b/crates/argus-ser/src/ty.rs @@ -1767,7 +1767,7 @@ pub enum BoundVariable { impl BoundVariable { pub fn new(didx: ty::DebruijnIndex, var: ty::BoundVar) -> Self { - // FIXME: bound varialbes shouldn't be in serialized types, I haven't + // FIXME: bound variables shouldn't be in serialized types, I haven't // encountered one in the raw output, and before release this was a // `panic`, which never fired. Self::Error(format!("{var:?}^{didx:?}").to_string()) diff --git a/crates/argus/src/aadebug/tree.rs b/crates/argus/src/aadebug/tree.rs index 54a6267..4123374 100644 --- a/crates/argus/src/aadebug/tree.rs +++ b/crates/argus/src/aadebug/tree.rs @@ -462,7 +462,7 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> { /// A local type failing to implement a trait (local/external). /// NOTE that `T: C` where `T` is an external type is considered impossible /// to change, if this is the only option a relaxed rule might suggest - /// creating a wapper for the type. + /// creating a wrapper for the type. /// /// Intrusive changes /// diff --git a/crates/argus/src/analysis/transform.rs b/crates/argus/src/analysis/transform.rs index b85d60d..5e917e3 100644 --- a/crates/argus/src/analysis/transform.rs +++ b/crates/argus/src/analysis/transform.rs @@ -232,7 +232,7 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> { // Filter down the set of obligations as much as possible. // // 1. Remove obligations that shouldn't have been checked. (I.e., a failed - // precondition dissallows it from succeeding.) Hopefully, in the future these + // precondition disallows it from succeeding.) Hopefully, in the future these // aren't even solved for. retain_error_sources( &mut obligations, @@ -250,7 +250,7 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> { let obligations = obligations .into_iter() - // marge back in indices without data + // merge back in indices without data .chain(obligations_no_data.into_iter()) .map(|idx| *self.obligations[idx]) .collect::>(); @@ -447,7 +447,7 @@ mod tree_search { /// Search for the target obligation along the non-branching tree path. /// - /// This is usefull if a predicate, reported as a trait error, does not + /// This is useful if a predicate, reported as a trait error, does not /// match one of the stored roots. This can happen when the start of /// the "trait tree" is a stick, e.g., /// diff --git a/crates/argus/src/ext.rs b/crates/argus/src/ext.rs index 8552a8b..36d0246 100644 --- a/crates/argus/src/ext.rs +++ b/crates/argus/src/ext.rs @@ -79,7 +79,7 @@ impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> { /// Determine what level of "necessity" an obligation has. /// /// For example, obligations with a cause `SizedReturnType`, - /// with a `self_ty` `()` (unit), is *unecessary*. Obligations whose + /// with a `self_ty` `()` (unit), is *unnecessary*. Obligations whose /// kind is not a Trait Clause, are generally deemed `ForProfessionals` /// (that is, you can get them when interested), and others are shown /// `OnError`. Necessary obligations are trait predicates where the diff --git a/crates/argus/src/find_bodies.rs b/crates/argus/src/find_bodies.rs index d8c11a7..90777c7 100644 --- a/crates/argus/src/find_bodies.rs +++ b/crates/argus/src/find_bodies.rs @@ -1,6 +1,6 @@ //! This is a copy of the `BodyFinder` from `rustc_utils` but it //! does *not* skip const/static items. Funny enough, these items -//! often have imporant trait contraints evaluated (think derive macros). +//! often have important trait constraints evaluated (think derive macros). use rustc_hir::{intravisit::Visitor, BodyId}; use rustc_middle::{hir::nested_filter::OnlyBodies, ty::TyCtxt}; use rustc_span::Span; diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs index fd7b062..6f87b8d 100644 --- a/crates/argus/src/proof_tree/serialize.rs +++ b/crates/argus/src/proof_tree/serialize.rs @@ -153,7 +153,7 @@ impl SerializedTreeVisitor<'_> { // comparing the JSON values is a bad idea in general. (This is what comparing // interned keys does essentially). We should wait until the new trait solver // has some mechanism for detecting cycles and piggy back off that. - // FIXME: this is currently dissabled but we should check for cycles again... + // FIXME: this is currently disabled but we should check for cycles again... #[allow(dead_code)] fn check_for_cycle_from(&mut self, from: ProofNodeIdx) { if self.cycle.is_some() { diff --git a/crates/argus/src/tls.rs b/crates/argus/src/tls.rs index a4ed6f8..0b189f4 100644 --- a/crates/argus/src/tls.rs +++ b/crates/argus/src/tls.rs @@ -27,7 +27,7 @@ use crate::{ const DRAIN_WINDOW: usize = 100; // NOTE: we use thread local storage to accumulate obligations -// accross call to the obligation inspector in `typeck_inspect`. +// across call to the obligation inspector in `typeck_inspect`. // DO NOT set this directly, make sure to use the function `push_obligaion`. // // TODO: documentation diff --git a/flake.nix b/flake.nix index 4204072..547881f 100644 --- a/flake.nix +++ b/flake.nix @@ -6,58 +6,110 @@ }; outputs = { self, nixpkgs, flake-utils, rust-overlay }: - flake-utils.lib.eachDefaultSystem (system: - let - overlays = [ (import rust-overlay) ]; - pkgs = import nixpkgs { - inherit system overlays; - }; - toolchain = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml; - depotjs = pkgs.rustPlatform.buildRustPackage rec { - pname = "depot"; - version = "0.2.17"; - - # Depot tests require lots of external toolchains, node, typedoc, biome, ... - # so we'll just skip all tests for now and figure this out later. - doCheck = false; - - src = pkgs.fetchFromGitHub { - owner = "cognitive-engineering-lab"; - repo = pname; - rev = "v${version}"; - hash = "sha256-kiQXxTVvzfovCn0YmOH/vTUQHyRS39gH7iBGaKyRZFg="; - }; - - cargoHash = "sha256-m9sG//vBUqGLwWHkyq+sJ8rkQOeaif56l394dgPU1uQ="; - buildInputs = with pkgs; lib.optionals stdenv.isDarwin [ - darwin.apple_sdk.frameworks.SystemConfiguration - ]; - }; - in { - devShell = with pkgs; mkShell { - buildInputs = [ - # Deployment only - vsce - cargo-workspaces - - llvmPackages_latest.llvm - llvmPackages_latest.lld - - guile - depotjs - nodejs_22 - nodePackages.pnpm - - cargo-make - cargo-watch - rust-analyzer - - toolchain - ] ++ lib.optionals stdenv.isDarwin [ - darwin.apple_sdk.frameworks.SystemConfiguration - ]; - - RUSTC_LINKER = "${pkgs.llvmPackages.clangUseLLVM}/bin/clang"; - }; - }); + flake-utils.lib.eachDefaultSystem (system: + let + overlays = [ (import rust-overlay) ]; + pkgs = import nixpkgs { + inherit system overlays; + }; + entry-crate = ./crates/argus-cli; + toolchain = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml; + meta = (builtins.fromTOML (builtins.readFile (entry-crate/Cargo.toml))).package; + inherit (meta) name version; + + depotjs = pkgs.rustPlatform.buildRustPackage rec { + pname = "depot"; + version = "0.2.17"; + + # Depot tests require lots of external toolchains, node, typedoc, biome, ... + # so we'll just skip all tests for now and figure this out later. + doCheck = false; + + src = pkgs.fetchFromGitHub { + owner = "cognitive-engineering-lab"; + repo = pname; + rev = "v${version}"; + hash = "sha256-kiQXxTVvzfovCn0YmOH/vTUQHyRS39gH7iBGaKyRZFg="; + }; + + cargoHash = "sha256-m9sG//vBUqGLwWHkyq+sJ8rkQOeaif56l394dgPU1uQ="; + buildInputs = with pkgs; lib.optionals stdenv.isDarwin [ + darwin.apple_sdk.frameworks.SystemConfiguration + ]; + }; + + mdbook-image-size = with pkgs; rustPlatform.buildRustPackage rec { + pname = "mdbook-image-size"; + version = "0.2.0"; + + src = fetchFromGitHub { + owner = "lhybdv"; + repo = pname; + rev = version; + hash = "sha256-fySGDx3vbLsc3fL/54nMVjVRHNlQ2ZYSM4LMDHxUUvs="; + }; + cargoHash = "sha256-iOTIjZr7vyduGTzK0xUssCKBKc8O0AYLpSdcozKPF2o="; + doCheck = false; + }; + + checkProject = pkgs.writeScriptBin "ci-check" '' + cargo fmt --check + cargo clippy + codespell . + cargo test + ''; + in { + devShell = pkgs.mkShell { + buildInputs = [ checkProject ] ++ (with pkgs; [ + llvmPackages_latest.llvm + llvmPackages_latest.lld + + toolchain + + guile + depotjs + nodejs_22 + nodePackages.pnpm + codespell + + cargo-make + cargo-watch + rust-analyzer + + mdbook + mdbook-mermaid + mdbook-admonish + mdbook-image-size + + vsce + cargo-workspaces + ] ++ lib.optionals stdenv.isDarwin [ + darwin.apple_sdk.frameworks.SystemConfiguration + ] ++ lib.optionals stdenv.isLinux [ + # Libraries needed in testing + alsa-lib + systemd + ]); + + RUSTC_LINKER = "${pkgs.llvmPackages.clangUseLLVM}/bin/clang"; + }; + + # packages = rec { + # default = cargo-argus; + + # cargo-argus = pkgs.rustPlatform.buildRustPackage { + # pname = name; + # inherit version; + # src = ./.; + # cargoSha256 = pkgs.lib.fakeHash; + # release = true; + # }; + + # # TODO package and release tutorial with nix + # # argus-tutorial = {}; + + # # TODO package and release extension with nix + # # vscode-argus = {}; + # }; + }); } diff --git a/ide/packages/common/src/TreeInfo.ts b/ide/packages/common/src/TreeInfo.ts index feaef1d..2d44b46 100644 --- a/ide/packages/common/src/TreeInfo.ts +++ b/ide/packages/common/src/TreeInfo.ts @@ -245,7 +245,7 @@ export class TreeInfo { const goalData = tree.goals[node.Goal]; const result = tree.results[goalData.result]; return "keep"; - // FIXME: I belive that this logic is correct, but argus crashes when enabled + // FIXME: I believe that this logic is correct, but argus crashes when enabled // return isHiddenObl({ necessity: goalData.necessity, result }) // ? "remove-tree" // : "remove-node"; @@ -426,7 +426,7 @@ export class TreeInfo { /** * Define the heuristic used for inertia in the system. Previously we were - * using `momentum / velocity` but this proved too sporatic. Some proof trees + * using `momentum / velocity` but this proved too sporadic. Some proof trees * were deep, needlessely, and this threw a wrench in the order. */ public static setInertia = (set: SetHeuristic) => { diff --git a/ide/packages/extension/src/view.ts b/ide/packages/extension/src/view.ts index dc62e31..69f88da 100644 --- a/ide/packages/extension/src/view.ts +++ b/ide/packages/extension/src/view.ts @@ -73,7 +73,7 @@ export class View { ); // Listen for when the panel is disposed - // This happens when the user closes the panel or when the panel is closed programatically + // This happens when the user closes the panel or when the panel is closed programmatically this.disposables.push( panel.onDidDispose(() => { log("Disposing panel"); diff --git a/ide/packages/panoptes/src/TreeView/Panels.tsx b/ide/packages/panoptes/src/TreeView/Panels.tsx index f6caf50..3f71afc 100644 --- a/ide/packages/panoptes/src/TreeView/Panels.tsx +++ b/ide/packages/panoptes/src/TreeView/Panels.tsx @@ -26,7 +26,7 @@ export interface PanelDescription { interface PanelState { activePanel: number; node?: number; - programatic?: boolean; + programmatic?: boolean; } export function usePanelState() { @@ -70,13 +70,13 @@ const Panels = ({ }, []); // NOTE: rerenders should not occur if the user clicks on a tab. We cache the - // elements in state to avoid this. IFF the change is *programatic*, meaning + // elements in state to avoid this. IFF the change is *programmatic*, meaning // some GUI action caused the change, we always want to force a rerender so that // state change visuals are shown. useEffect(() => { console.debug(`Panel(${id}) params changed`, active, programaticSwitch); if (programaticSwitch) { - // On a programatic switch only rerender the active tab + // On a programmatic switch only rerender the active tab rerender(active); } }, [active, programaticSwitch]); diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx index 66a5721..0006c70 100644 --- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx +++ b/ide/packages/panoptes/src/TreeView/TreeApp.tsx @@ -66,7 +66,7 @@ const TreeApp = ({ // Callback passed to the BottomUp panel to jump to the TopDown panel. - setState({ activePanel: 1, node: n, programatic: true }) + setState({ activePanel: 1, node: n, programmatic: true }) } /> ) @@ -93,7 +93,7 @@ const TreeApp = ({ manager={[ state.activePanel, n => setState({ activePanel: n }), - state.programatic + state.programmatic ]} description={tabs} /> diff --git a/ide/packages/panoptes/src/Workspace.tsx b/ide/packages/panoptes/src/Workspace.tsx index 7a7c471..9a3e7c6 100644 --- a/ide/packages/panoptes/src/Workspace.tsx +++ b/ide/packages/panoptes/src/Workspace.tsx @@ -45,7 +45,7 @@ const Workspace = observer( ({ fn }) => fn === HighlightTargetStore.value?.file ); if (0 <= idx && idx !== state.activePanel) - setState({ activePanel: idx, programatic: true }); + setState({ activePanel: idx, programmatic: true }); }, [HighlightTargetStore.value?.file]); const viewProps = { @@ -79,7 +79,7 @@ const Workspace = observer( manager={[ state.activePanel, n => setState({ activePanel: n }), - state.programatic + state.programmatic ]} /> diff --git a/ide/packages/print/src/lib.tsx b/ide/packages/print/src/lib.tsx index 356c3df..f349d30 100644 --- a/ide/packages/print/src/lib.tsx +++ b/ide/packages/print/src/lib.tsx @@ -30,7 +30,7 @@ import { // `PrintWithFallback`. Pretty printing is still a fragile process and // I don't have full confidence in it yet. // -// Additionally, this component sets the contents to stlye with the editor monospace font. +// Additionally, this component sets the contents to style with the editor monospace font. export const PrintWithFallback = ({ object, Content diff --git a/ide/packages/print/src/private/syntax.tsx b/ide/packages/print/src/private/syntax.tsx index 82dae84..08b93aa 100644 --- a/ide/packages/print/src/private/syntax.tsx +++ b/ide/packages/print/src/private/syntax.tsx @@ -41,7 +41,7 @@ export const Kw = ({ children }: React.PropsWithChildren) => ( /** * Create a wrapper around the children using a `stx-wrapper` class and the - * additional class `c`. This makes a wrapper that breakes around the wrapped + * additional class `c`. This makes a wrapper that breaks around the wrapped * elements. */ const makeCSSWrapper = diff --git a/ide/packages/print/src/private/term.tsx b/ide/packages/print/src/private/term.tsx index 1f531b3..4a31068 100644 --- a/ide/packages/print/src/private/term.tsx +++ b/ide/packages/print/src/private/term.tsx @@ -83,7 +83,7 @@ export const PrintExpr = ({ o }: { o: ExprDef }) => { }; // NOTE: this is the mir BinOp enum so not all operators are "source representable." -// Exluding "Cmp" as it rearranges the operands and doesn't follow the pattern. +// Excluding "Cmp" as it rearranges the operands and doesn't follow the pattern. const PrintBinOp = ({ o }: { o: Exclude }) => { if (o === "Add") { return "+"; diff --git a/ide/packages/print/src/private/ty.tsx b/ide/packages/print/src/private/ty.tsx index e1b1717..f88602c 100644 --- a/ide/packages/print/src/private/ty.tsx +++ b/ide/packages/print/src/private/ty.tsx @@ -520,7 +520,7 @@ export const PrintRegion = ({ case "Anonymous": { // NOTE: by default we don't print anonymous lifetimes. There are times // when it looks better, e.g., when the region is `mut`. One gotcha right now - // is that we don't rename them, which makes reasoning about anonymouse lifetimes + // is that we don't rename them, which makes reasoning about anonymous lifetimes // tricky. if (forceAnonymous) { return "'_"; @@ -568,7 +568,7 @@ export const PrintBoundTyKind = ({ o }: { o: BoundTyKind }) => { export const PrintBoundVariableKind = ({ o }: { o: BoundVariableKind }) => { if ("Const" === o) { - // TODO: not sure what to do with boudn "consts", we don't have data for them. + // TODO: not sure what to do with bound "consts", we don't have data for them. return null; } else if ("Ty" in o) { return ;