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.
Install with Tessl CLI
npx tessl i github:ArabelaTso/Skills-4-SE --skill library-advisor93
Does it follow best practices?
Validation for skill structure
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 its purpose (recommending standard library resources for theorem provers), provides comprehensive trigger conditions through a numbered list, and uses domain-specific terminology that users would naturally employ. The description is specific to Isabelle/HOL and Coq, making it highly distinctive and unlikely to conflict with other skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Recommend relevant Isabelle/HOL or Coq standard library theories, lemmas, and tactics based on proof goals' and mentions specific operations like 'list/set/arithmetic operations' and 'find_theorems/Search commands'. | 3 / 3 |
Completeness | Clearly answers both what (recommend library theories, lemmas, tactics) AND when with explicit numbered triggers covering six distinct use cases. The 'Use when:' clause is explicit and comprehensive. | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'library lemmas', 'proof goals', 'libraries to import', 'list/set/arithmetic operations', 'stuck', 'find_theorems/Search commands', 'Isabelle/HOL', 'Coq'. Good coverage of domain-specific terms users would naturally use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive with clear niche: specifically targets Isabelle/HOL and Coq theorem provers' standard libraries. The combination of proof assistants, library recommendations, and specific commands like 'find_theorems/Search' creates a unique, non-conflicting scope. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
85%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a well-structured skill that provides actionable guidance for library recommendations in both Isabelle/HOL and Coq. The workflow is clear and the code examples are executable and specific. The main weakness is some verbosity and repetition that could be tightened, particularly in the parallel Isabelle/Coq examples.
Suggestions
Consolidate the domain-specific recommendations into a more compact table format rather than repeated bullet lists
Remove explanatory phrases like 'Examine the goal to identify' and 'Based on the domain, recommend' - Claude understands the task from context
| 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 'Examine the goal to identify' are somewhat verbose for Claude. | 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 recommendations are specific and directly usable. | 3 / 3 |
Workflow Clarity | Clear 6-step workflow with logical progression from analysis to recommendation. Each step has explicit actions, and the pattern-based sections provide clear decision paths. The workflow is appropriate for an advisory skill that doesn't involve destructive operations. | 3 / 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 without deep nesting. | 3 / 3 |
Total | 11 / 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.
- 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.