Skip to content

Simplify AGENTS.md by delegating HOL tool docs to /hol skill #29

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
charles-cooper merged 2 commits into from
Dec 28, 2025
+4 −52
Merged

Simplify AGENTS.md by delegating HOL tool docs to /hol skill #29

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
da32a20
Simplify AGENTS.md by delegating HOL tool docs to /hol skill
charles-cooper Dec 28, 2025
d54e460
Update AGENTS.md to reference /hol4 skills
charles-cooper Dec 28, 2025
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
56 changes: 4 additions & 52 deletions AGENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@

Only use Bash for:
- Running `Holmake` builds
- Running `~/hol-agents/hol-agent-helper.sh` commands
- Git operations (`git grep`, `git status`, etc.)

**Why:** Bash file operations require permission prompts. The dedicated tools don't.
Expand Down Expand Up @@ -103,62 +102,15 @@ VFMDIR=/home/ubuntu/verifereum Holmake --qof

## Interactive HOL Sessions

Use the helper script for debugging proofs:
Use the `/hol4` skills for proof development.

```bash
# Start session (from theories directory)
~/hol-agents/hol-agent-helper.sh start

# Check status
~/hol-agents/hol-agent-helper.sh status

# Send simple commands (no backquotes)
~/hol-agents/hol-agent-helper.sh send 'open arithmeticTheory;'

# Send commands with backquotes - use a file
# Write to hol_cmd.sml, then:
~/hol-agents/hol-agent-helper.sh send:hol_cmd.sml

# IMPORTANT: ALWAYS check output using the helper script's log command
# NEVER use raw file paths like ~/.hol/hol_output.log directly
~/hol-agents/hol-agent-helper.sh log | tail -50

# Stop
~/hol-agents/hol-agent-helper.sh stop
```

**CRITICAL: Always use `~/hol-agents/hol-agent-helper.sh log` for checking HOL output. Do NOT access raw log files directly.**

### Initialization

For code that should always run at session start (loading theories, etc.), put it in `.hol_init.sml` in the working directory. This is auto-loaded by `start`.
### File Conventions (repo-specific)

**IMPORTANT:** Before issuing any commands, check the contents of `.hol_init.sml` to see what's already loaded. Don't duplicate load commands.

### Sending Commands

For commands with HOL term quotations (backquotes), **always use a temp file**:

```sml
(* .hol_cmd.sml *)
g `!n. n + 0 = n`;
e (Induct_on `n`);
```

Then: `~/hol-agents/hol-agent-helper.sh send:.hol_cmd.sml`

### File Naming Conventions

Local test/scratch files should use **dot prefixes** to keep them gitignored:

- `.hol_cmd.sml` - command file for sending to HOL session
Local test/scratch files use **dot prefixes** (gitignored):
- `.hol_init.sml` - auto-loaded on session start
- `.hol_test.sml` - temporary test scripts

These `.hol*` files are gitignored. Avoid unprefixed names like `test.sml` or `hol_cmd.sml` which will show up in git status.

### File Size
Try to keep files under 500 LOC for better context management (soft limit, not strict).
Try to keep theory files under 500 LOC (soft limit).

## HOL4 Tactics Reference

Expand Down