docs and crates

[navicore]

Workspace versioning (Cargo.toml):

• [workspace.package] with version = "0.1.0", edition, authors, license
• Both crates use version.workspace = true
• patch-prolog-core dependency pinned with version = "=0.1.0" (exact match)

Release workflow (.github/workflows/release.yml):

1. Triggered on GitHub release with v* tag
2. Extracts version from tag, updates [workspace.package] version and dependency pins via awk
3. Commits + pushes the version bump
4. Runs tests
5. Verifies all crates use workspace version and pins match
6. Publishes patch-prolog-core first, waits 60s for indexing, then publishes patch-prolog
7. Builds static Linux (musl), macOS ARM64, and macOS x86_64 binaries
8. Attaches all binaries to the GitHub release

To use: Create a release tagged v0.2.0 on GitHub. The workflow handles everything else. You'll need CRATES_IO_TOKEN and PAT secrets configured in the
repo.

[claude]

Prolog Engine Review

This PR is a crate rename plus a release workflow; engine source files are unchanged but appear in the diff.

---

1. Parser: \+ operator precedence is wrong

crates/patch-prolog-core/src/parser.rs, lines 305-313

\+ calls self.parse_primary() for its argument, so \+ X = Y parses as (\+ X) = Y. ISO gives \+ priority 900 and = priority 700, so the correct parse is \+(X = Y). Any source writing \+ Var = Term or \+ Var is Expr silently gets wrong term structure with no parse error.

---

2. Tokenizer: overflowing float literals silently become f64::INFINITY

crates/patch-prolog-core/src/tokenizer.rs, lines 556-564

str::parse::<f64>() returns f64::INFINITY (not an error) when a digit string exceeds f64::MAX. A literal with 310+ digits before the decimal silently produces Term::Float(inf). check_float is never called during tokenization so the Infinity propagates into the compiled database undetected. A .is_infinite() guard after parse is needed.

---

3. =../2 and functor/3: error in main solver, silent failure in NAF/once/findall

crates/patch-prolog-core/src/solver.rs

=../2 with an empty list: the main solve loop (~line 672) returns SolveResult::Error; try_exec_misc (~line 1994) returns Some(false).

functor/3 with negative arity: the main solve loop (~line 581) returns SolveResult::Error; try_exec_misc (~line 1908) returns Some(false).

Consequence: \+(X =.. []) succeeds (NAF sees failure) while a bare X =.. [] errors. Same inconsistency inside once/1, findall, and if-then conditions. The try_exec_misc path must propagate errors rather than convert them to silent failure.

---

4. atom_chars/2 and atom_length/2 reject integer/float first arguments

crates/patch-prolog-core/src/solver.rs, lines 389-403 and 426-481

Both predicates handle only Term::Atom and return a runtime error for integers or floats. ISO 6903-1 requires atom_length(42, L) to succeed with L=2 and atom_chars(3.14, Cs) to give Cs=['3','.','1','4']. Programs that use these for number-to-char conversion get a hard error instead.

---

5. Rust call-stack overflow risk in try_solve_once / try_solve_collecting

crates/patch-prolog-core/src/solver.rs, lines 1233 and 1536

Both functions recurse via Rust call frames for every resolution step of user-defined predicates, with no Rust stack depth tracking — only a step counter. With max_depth = 10_000, deeply recursive Prolog programs inside \+, once/1, findall, or if-then conditions can create thousands of Rust frames and overflow the OS 8 MB default stack. A separate recursion-depth counter (threshold ~1,000-2,000) returning SolveResult::Error would prevent the crash.

---

6. First-argument index returns all clauses on a ground-arg miss

crates/patch-prolog-core/src/index.rs, lines 97-105

The None => entry.all_clause_indices.clone() fallback is only reached when var_clause_indices is empty (guarded at line 78), meaning every clause has a ground first argument. If the goal's ground first arg is absent from arg_index, no clause can unify — the correct return is vec![]. Returning all clauses causes O(N) unnecessary head-unification attempts. For color(red). color(blue). queried as color(purple), the engine tries both clauses before failing rather than immediately returning empty.

---

7. between/3 in try_solve_once: O(M × N) goal-list cloning

crates/patch-prolog-core/src/solver.rs, lines 1428 and 1438

remaining.clone() allocates a full copy of the remaining goal list on every iteration of the range. For \+ between(1, N, X), rest_goals this is O(|rest_goals| × N) total allocation. Since the loop already returns on first success, hoisting the clone or passing a reference eliminates most redundant work.

---

Minor

• unify_with_occurs_check/2 is implemented (occurs_in in unify.rs:164) but not registered in is_builtin/exec_builtin. The #[allow(dead_code)] attribute should explain why it is intentionally omitted.
• call/N (N > 1) is unsupported and undocumented. A test capturing the current limit would prevent silent regressions.
• In arith_div (builtins.rs:572), the guard (_, ArithVal::Float(b)) if *b == 0.0 correctly catches -0.0 because -0.0 == 0.0 in IEEE 754. Correct but non-obvious; a comment helps.

[claude]

Code Review - see details below

[claude]

REVIEW PART 1 of 3 -- index.rs line 101 None => vec![]: Correct and an improvement. The old fallback to all_clause_indices was unnecessary when var_clause_indices is empty and a ground query key misses arg_index, no clause can possibly unify. Float and List first-arg clause heads return None from first_arg_key() and are absent from both arg_index and var_clause_indices. Their corresponding query paths (float/list/variable first arg in goal) also produce None in lookup_clauses lines 91-94, falling through to the None => all_clause_indices branch at line 104, never reaching line 101. Ground atom/integer/compound queries against float-headed clauses would fail unification regardless, so vec![] is correct.

[claude]

REVIEW PART 2 of 3 -- parser.rs line 308 negation-as-failure fix: Correct fix for a real bug. With parse_primary(), NAF X = Y at goal level parsed as NAF(X) and left = Y stranded causing a parse error. With parse_term() (= parse_expr_700()), it correctly parses as NAF(X = Y). The comment ISO precedence 900fy, parses argument at 700 is accurate -- ISO says fy 900 but the parser only goes to 700. Since no operators are defined between 701 and 899, this matches ISO for all current operators. Any future operator in that range would need a parse_expr_900() level. One subtle interaction: parse_primary() now calling parse_term() means NAF inside an arithmetic sub-expression greedily consumes a following = ..., e.g. a + NAF b = c parses as plus(a, NAF(equals(b, c))) rather than a syntax error. Pre-existing structural issue, not introduced by this PR.

[claude]

REVIEW PART 3 of 3 -- tokenizer.rs line 560: The val.is_infinite() check is correct. The tokenizer only lexes digit strings so parse f64 can produce Inf from overflow but not NaN. The guard correctly rejects overflowing literals at lex time. Four new integration tests all verify the fixed behaviors correctly. release.yml: publish job uses actions/checkout@v5 while build jobs use @v4 (worth aligning); the 60-second sleep between publishing the two crates is sometimes insufficient for crates.io indexing (consider 90-120 seconds or a retry loop). SUMMARY: No correctness bugs found in the Prolog engine changes. The index optimization is sound, the NAF parse fix is correct, and the float overflow guard is a good safety addition.