github.com/HOL-Theorem-Prover/HOL (link)

commit signals (797)

source signals (5)

• CLAUDE.mdvia claude-code

  # HOL4 — quick notes for AI assistants
  
  Long-form developer documentation lives under `Manual/Developers/`
  and `developers/`.  This file is the always-loaded "things to
  remember before you touch anything" tier.
  
  ## Branching
  
  Branch new work off `origin/develop`, not local HEAD or arbitrary
  tags.  PRs target `develop`.
  
  ## Building
  
  Fresh checkout: `poly < tools/smart-configure.sml`.
  
  Routine sanity check after edits to compiled sources:
  
      bin/build -t --seq=tools/sequences/upto-parallel
  
  builds up to 

• .claudedirectoryvia claude-code
• .claudedirectoryvia claude-code
• .claude/skills/hol4-development/SKILL.mdvia unspecified

  ---
  name: hol4-development
  description: Conventions, build commands, and idioms for working on the HOL4 codebase as software — editing `.sml`/`.sig`/`*Script.sml` files, running `bin/build` or `Holmake`, refactoring modules, cleaning up dead code or stale comments, and navigating HOL4's directory structure. Trigger this skill whenever the working directory is a HOL4 checkout and the task touches source files, the build system, code style, or module/identifier naming — even if the user doesn't say "HOL4"

• .claude/skills/holmake-development/SKILL.mdvia unspecified

  ---
  name: holmake-development
  description: Working on Holmake itself — modifying `tools/Holmake/`, diagnosing why a target rebuilds spuriously, debugging the dep graph, understanding the three-phase `bin/build` flow, the heap-as-implicit-dep mechanism, BIC node semantics, the `HFS_NameMunge` `.hol/objs/` indirection, `--rebuild=mtime` vs `--rebuild=cachekey`, mosml/poly portability of `HM_Cline` options, and how to write Holmake regression tests. Use this skill whenever the task touches `tools/Holmake/**`

ignorefile signals (1)