A helper whose value depends on a hole is emitted into `ChallengeDeps`, so the workspace cannot build

[rammalahmad]

Summary

generate splits a problem's same-module dependencies into holes and helpers,
and emits every helper into ChallengeDeps.lean. But ChallengeDeps is
imported beneath the hole layer, so holes are not in scope there. A helper
whose value mentions a hole ends up calling an identifier that is not in the
module it lands in, and the workspace does not compile.

The shape that triggers it

/-- hole -/
@[eval_problem]
theorem exists_pos : ∃ n : Nat, 0 < n := by
  sorry

/-- NOT a hole; its value consumes the hole's proof -/
noncomputable def witness : Nat :=
  Classical.choose exists_pos

/-- hole; its statement mentions `witness` -/
@[eval_problem]
theorem witness_pos : 0 < witness := by
  sorry

with both theorems in the manifest's holes. generate classifies witness as
a helper, so the emitted ChallengeDeps.lean is:

import Mathlib

namespace ToyHoleDep

noncomputable def witness : Nat :=
  Classical.choose exists_pos

end ToyHoleDep

error: ChallengeDeps.lean:9:19: Unknown identifier `exists_pos`

This shape is not avoidable by authors: Classical.choose : (∃ x, p x) → α
turns a proof into data, which is how the mathematics is usually written --
prove existence, then define the object it produces.

Where it happens

EvalTools/Generate.lean, building helperNames:

let holeNames : Std.HashSet String :=
  extracteds.foldl (init := {}) fun acc e => acc.insert e.declarationName
let helperNames : Std.HashSet String :=
  extracteds.foldl (init := {}) fun acc e =>
    e.sameModuleDependencies.foldl
      (fun a n => if holeNames.contains n then a else a.insert n) acc

The filter drops dependencies that are holes, but keeps dependencies that
depend on holes.

Why the manifest cannot work around it

• non-hole — stays in ChallengeDeps, cannot compile;
• definition hole — type pinned, body free, so a solver supplies any Nat
  and the author's construction is lost;
• theorem hole — same loss, and it is not Prop.

The declaration needs its data frozen and a position below the hole layer.

Suggested fix

Make hole-dependence transitive when partitioning, and emit anything at or below
the cut into the hole layer instead of ChallengeDeps:

ChallengeDeps.lean     no transitive dependency on a hole
Challenge/Submission/Solution.lean     the holes, plus everything downstream

The moved declarations are not turned into holes -- they stay out of
theorem_names and definition_names, so the comparator still compares them by
full ConstantInfo and the data stays frozen.

[rammalahmad]

Happy to put up a PR if that's useful, I've prototyped the transitive cut as a post-processing pass over generate's output, so I'm familiar with some edge cases.

[alreadydone]

This is also blocking #191, since the eval_problem finite_setOf_place_notMem is used in some instance definition below. Probably easier solution:

Each toml file in manifests/problems designates a module name, and I propose that different problems should lie in different modules (Lean files). Once this is enforced, then the module for a problem could just turn into its Challenge.lean as a whole, while the necessary pieces of the imported files go into ChallengeDeps.lean.

Currently, e.g. NumberTheory/SmallHouse.lean contains two problems. In case multiple problems in a file depend on some common development, these can be extracted to another preliminary file, and we create multiple files, each for one problem, which all import the same preliminary file.