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.
90
86%
Does it follow best practices?
Impact
96%
1.03xAverage score across 3 eval scenarios
Passed
No known issues
Quality
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly defines a specialized niche in theorem prover library assistance. It provides specific capabilities, comprehensive trigger conditions with six enumerated use cases, and uses domain-specific terminology that theorem prover users would naturally employ. The description effectively distinguishes itself from general coding or documentation skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Recommend relevant Isabelle/HOL or Coq standard library theories, lemmas, and tactics', 'library lemmas for their proof', 'list/set/arithmetic operations', 'find_theorems/Search commands'. These are concrete, domain-specific capabilities. | 3 / 3 |
Completeness | Clearly answers both what (recommend library theories, lemmas, tactics) AND when with explicit numbered triggers covering six specific scenarios. The 'Use when:' clause with enumerated conditions provides comprehensive guidance on when to select this skill. | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'Isabelle/HOL', 'Coq', 'standard library', 'lemmas', 'tactics', 'proof goals', 'libraries to import', 'list/set/arithmetic operations', 'find_theorems', 'Search commands'. Good coverage of terms theorem prover users would naturally use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting Isabelle/HOL and Coq theorem provers specifically. The combination of 'standard library', 'lemmas', 'tactics', and specific tool names like 'find_theorems/Search' creates clear boundaries unlikely to conflict with general programming or documentation skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
72%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This skill provides comprehensive, actionable guidance for library recommendations in both Isabelle/HOL and Coq, with excellent concrete examples and good progressive disclosure through external references. The main weaknesses are moderate verbosity from parallel Isabelle/Coq examples and missing validation/recovery steps in the workflow for when recommendations don't match the user's needs.
Suggestions
Add a validation step to the workflow explaining how to verify that recommended lemmas actually apply to the goal (e.g., 'If the lemma doesn't apply, check types match and try Search with more specific patterns')
Consolidate some of the parallel Isabelle/Coq examples into a more compact table format to reduce redundancy while preserving actionability
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is reasonably efficient but includes some redundancy, particularly in the repeated pattern examples across Isabelle and Coq. The domain-specific recommendations section could be more condensed, and some explanations (like the workflow steps) add modest overhead. | 2 / 3 |
Actionability | Provides fully executable code examples for both Isabelle and Coq, with concrete lemma names, specific search commands, and copy-paste ready proof patterns. The examples are complete and directly usable. | 3 / 3 |
Workflow Clarity | The 6-step workflow is clearly sequenced, but lacks explicit validation checkpoints. There's no feedback loop for when recommended lemmas don't work or when searches return no results. The workflow describes what to do but not how to verify success. | 2 / 3 |
Progressive Disclosure | Well-structured with clear overview sections and appropriate references to external files (isabelle_library.md, coq_library.md, examples.md). Content is organized by domain and pattern type, making navigation easy. | 3 / 3 |
Total | 10 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Repository
- ArabelaTso/Skills-4-SE
- Commit
0f00a4f
- Reviewed
Table of Contents
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.