Search results

probe-lean may skip lake build after lake clean (stale cache hit)

Status: Open.

#15 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Apr 1, 2026

Audit: are dependency arrays generated in deterministic order? (P14)

Status: Open.

#13 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Mar 22, 2026

Bug: multi-library projects get 0 declarations when Aeneas code is not in defaultTargets

Status: Open.

#12 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Mar 19, 2026

Design: Atom.FromJson/ToJson asymmetry (name field)

Status: Open.

#9 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Mar 6, 2026

Bug: loadFilteredAtoms hardcodes Aeneas-specific 'Funs.lean' filter

Status: Open.

#8 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Mar 6, 2026

Bug: pathsMatch can produce false positives (no directory boundary check)

Status: Open.

#7 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Mar 6, 2026

Design: isAlwaysSpecified returns true for all declaration kinds

Status: Open.

#6 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Mar 6, 2026

Soundness: sorryInDeclaration returns false when codeText is none

Status: Open.

#5 In Beneficial-AI-Foundation/probe-lean;

· astefano opened on Mar 6, 2026