library-advisor

Recommend relevant Isabelle/HOL or Coq standard library theories, lemmas, and tactics based on proof goals. Use when: (1) Users need library lemmas for their proof, (2) Proof goals match standard library patterns, (3) Users ask what libraries to import, (4) Specific lemmas are needed for list/set/arithmetic operations, (5) Users are stuck and need to know what library support exists, or (6) Guidance on find_theorems/Search commands is needed. Supports both Isabelle/HOL and Coq standard libraries.

1.03x

Quality

92%

Does it follow best practices?

Impact

96%

1.03x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Quality

Content

85%Weight 40%Scale 1-5

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

The content is highly actionable with executable examples for both proof assistants, a clear workflow, and well-structured references to real bundle files. Its main weakness is redundancy across the recommendation-patterns, common-recommendations, and examples sections, which inflates token usage.

Suggestions

Consolidate the overlapping 'Recommendation Patterns', 'Common Recommendations by Goal Type', and 'Examples' sections — the rev/length/add_commute goals appear repeatedly — to reduce redundancy and save tokens.

Move the exhaustive per-domain lemma name lists (Lists/Arithmetic/Sets/Logic 'Common goals') into the existing reference files, keeping only one representative example per domain in SKILL.md.

Trim the 'Tips' list, which largely restates guidance already embedded in the workflow and search-strategy sections.

Dimension	Reasoning	Score
Conciseness	Mostly efficient and free of basic-concept over-explanation, but the same example goals (rev_rev_ident, add_commute, length_append) recur across 'Recommendation Patterns', 'Common Recommendations by Goal Type', and 'Examples', which is noticeable padding that could be tightened.	3 / 5
Actionability	Provides copy-paste ready, executable Isabelle and Coq code blocks for each pattern, plus concrete search commands and tactics (lia, sledgehammer) covering the common cases comprehensively.	5 / 5
Workflow Clarity	A clear six-step sequence (Analyze goal → Determine system → Identify libraries → Search lemmas → Recommend → Suggest search) with well-ordered steps; this is advisory recommendation work with no destructive/batch operations requiring validation checkpoints.	5 / 5
Progressive Disclosure	The body is an overview with clearly signaled, one-level-deep markdown links to three real reference files (isabelle_library.md, coq_library.md, examples.md) that exist in references/, splitting detail appropriately from the main skill.	5 / 5
	Total	18 / 20 Passed

Description

100%Weight 40%Scale 1-5

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

A strong description: it states concrete capabilities, includes a detailed six-part 'Use when' trigger list, and is tightly scoped to Isabelle/HOL and Coq libraries. It avoids fluff and uses appropriate third-person voice throughout.

Dimension	Reasoning	Score
Specificity	Lists multiple concrete actions tied to the domain — recommending theories, lemmas, and tactics, plus guidance on find_theorems/Search commands — giving comprehensive coverage rather than just 1-2 actions.	5 / 5
Completeness	Explicitly states what the skill does (recommend theories/lemmas/tactics) and provides a six-clause 'Use when' trigger list answering when to invoke it with concrete trigger phrases.	5 / 5
Trigger Term Quality	Covers natural user phrases ('Users need library lemmas for their proof', 'what libraries to import', 'stuck and need to know what library support exists') plus tool-specific terms and synonyms (lemmas, tactics, find_theorems, Search).	5 / 5
Distinctiveness Conflict Risk	Narrows to a clear niche (Isabelle/HOL and Coq standard libraries) anchored by tool-specific triggers (find_theorems, Search), giving minimal overlap risk with unrelated skills.	5 / 5
	Total	20 / 20 Passed

Validation

100%

Warnings & errors only

Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.

Validation — 16 / 16 Passed

Validation for skill structure

No warnings or errors.

Repository: ArabelaTso/Skills-4-SE
Path: skills/library-for-proof-advisor/SKILL.md
Commit: 4f38503

Reviewed: 19 days ago

Table of Contents

Discovery Implementation Validation

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.