Repository cleanup: citation metadata, unused files, and CI docs - #4741
Open
feliperodri wants to merge 5 commits into
Open
Repository cleanup: citation metadata, unused files, and CI docs#4741feliperodri wants to merge 5 commits into
feliperodri wants to merge 5 commits into
Conversation
Add a `CITATION.cff` (CFF 1.2.0) whose `preferred-citation` points at the ASE '26 paper, so GitHub's "Cite this repository" button emits the paper rather than a bare software reference, and add a "Citing Kani" section to the README with the ACM Reference Format and a ready-to-paste BibTeX entry. Validated with `cffconvert --validate` (schema 1.2.0) and rendered with `ruby-cff` (the library behind GitHub's citation widget).
The LaTeX sources for the VSTTE 2024 short paper were checked in but are not built by anything in the repository, and the paper itself is now published. The ASE 2026 paper is the citation of record, so point people at it via `CITATION.cff` and the README instead of carrying paper sources here. The sources remain available in the git history. Also drop the now-empty `papers/` entry from the AGENTS.md repository layout table.
Added alongside the logo in model-checking#1157 but never referenced. The documentation site is built by `scripts/build-docs.sh` and published from `docs/book/`, so a repository-root icon never reaches it; mdBook takes its favicon from `theme/favicon.{png,svg}`, which this repository does not override. It is also absent from the `include` list in `Cargo.toml`, so it is not packaged into the `kani-verifier` crate, and GitHub does not use repository-root icons.
These were built by the `TestAlternativePlatforms` job of `release.yml`, which was removed in model-checking#3744 when Ubuntu 18.04 and AL2 support was dropped. That PR deleted only the 18.04 Dockerfile and left the other six behind, so nothing in the repository has referenced them since November 2024. They are also stale: two still install `kani-verifier` from crates.io rather than the bundle under test, and the NixOS one carries a workaround for model-checking#1246. Installing a release bundle is now covered natively by the `TestBundle` job across the macOS and Ubuntu runners, without Docker. Only `Dockerfile.bundle-release-24-04` remains, which builds the image published to GHCR on release.
Add a README explaining what `Dockerfile.bundle-release-24-04` is for: it builds the `ghcr.io/model-checking/kani-ubuntu-24.04` image published by the `Package Docker` job on release tags. Because it installs Kani from the release bundle and the packaged `kani-verifier` crate, it cannot be built from a clean checkout, so record the two artifacts it expects in the build context and the commands that produce them. Also note that the root `.dockerignore` exists for this build, that bundle installation is tested natively by `TestBundle` rather than through Docker, and that `run-copyright-check.sh` depends on GNU `xargs`.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Housekeeping for a few files that are either stale or undocumented, plus proper
citation metadata now that the Kani paper is published. Each commit stands alone.
Citation metadata. Adds
CITATION.cffwhosepreferred-citationpoints at theASE '26 paper, so GitHub's Cite this repository button emits the paper rather than a
bare software reference, and adds a "Citing Kani" section to the README with the ACM
Reference Format and a ready-to-paste BibTeX entry.
Removes the VSTTE 2024 paper sources. Nothing builds them, the paper is published,
and the ASE 2026 paper is now the citation of record. Still available in git history.
Removes
favicon.ico. Added with the logo in #1157 and never referenced. The docssite is published from
docs/book/, so a repository-root icon never reaches it, andmdBook takes its favicon from
theme/favicon.{png,svg}, which we don't override. It'salso absent from the
includelist inCargo.toml, so it isn't packaged into thekani-verifiercrate.Removes six orphaned
Dockerfile.bundle-test-*files. They were built by theTestAlternativePlatformsjob ofrelease.yml, removed in #3744 when Ubuntu 18.04/AL2support was dropped; that PR deleted only the 18.04 Dockerfile and left the rest behind.
They're also stale —
bundle-test-al2installskani-verifierfrom crates.io with thebundle-install lines commented out, so it wasn't testing the bundle under test. Bundle
installation is covered natively by the
TestBundlejob across the macOS and Ubunturunners.
Documents the remaining CI helpers. Adds
scripts/ci/README.mdexplaining thatDockerfile.bundle-release-24-04builds theghcr.io/model-checking/kani-ubuntu-24.04image published by the
Package Dockerjob on release tags, why it can't be built froma clean checkout, and the commands that produce the artifacts it expects. Also records
why the root
.dockerignoreexists and thatrun-copyright-check.shneeds GNUxargs.Manual testing:
CITATION.cffvalidates against CFF schema 1.2.0 (cffconvert --validate), andruby-cff(the library behind GitHub's citation widget) renders it as a complete@inproceedingsentry with all authors and the DOI.CITATION.cff:passes. Note it needs a BSD-compatible
xargsinvocation to run on macOS.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.