Skip to content

Document LOGOS in the standard AutoDeduct image #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sinashm merged 1 commit into from
Oct 14, 2026
Merged

Document LOGOS in the standard AutoDeduct image #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions docs/AUTODEDUCT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

LOGOS supplies the contract-generation skill and verification wrapper used by
AutoDeduct's [`llm-skill-mode` branch](https://github.com/rse-verification/auto-deduct/tree/llm-skill-mode).
The compatible LOGOS changes are on `llm-host-runtime`.
The compatible LOGOS changes are on `main`.

Follow AutoDeduct's [LLM setup and usage guide](https://github.com/rse-verification/auto-deduct/blob/llm-skill-mode/docs/LLM.md)
for host installation, the supported LOGOS revision, and Docker image builds.
Expand Down Expand Up @@ -54,9 +54,10 @@ extracts its skill into a temporary host cache, and gives that path to Codex.
The wrapper runs from the same image ID. Users of a prepared image need no
local LOGOS checkout or `--llm-skill` flag.

Building that image from source still requires a LOGOS checkout as the named
Docker build context. This is a build requirement, separate from the runtime
requirements of someone using an already prepared image. Follow
The standard `auto-deduct:latest` image includes LOGOS alongside Saida, ISP
and TriCera. Its Dockerfile fetches a pinned LOGOS revision during the build;
no separate host LOGOS checkout or extra image layer is needed. Run the standard
image build from the AutoDeduct checkout on your host. Follow
[AutoDeduct's image build instructions](https://github.com/rse-verification/auto-deduct/blob/llm-skill-mode/docs/LLM.md#build-the-verifier-image).

## Why the Launcher Runs on the Host
Expand Down
5 changes: 3 additions & 2 deletions docs/SETUP.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,5 +118,6 @@ global skill installation is unnecessary for its local runtime. Its Docker
runtime extracts `/opt/logos/skill/SKILL.md` from the selected image into a
temporary host cache and uses the same pinned image for verification.
`--llm-skill` and a separate local LOGOS checkout are unnecessary for Docker
execution. Building the image from source still needs the LOGOS checkout as
the build context; see [AutoDeduct integration](AUTODEDUCT.md).
execution. AutoDeduct's standard Dockerfile fetches and includes LOGOS by
default, so building that image also needs no host LOGOS checkout; see
[AutoDeduct integration](AUTODEDUCT.md).
Loading