Skip to content

Dev #39

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
JOSHCLUNE merged 2 commits into from
May 27, 2026
Merged

Dev #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7efb656
hammer.singleTacticParallel
JOSHCLUNE May 27, 2026
9d05c58
Update grindPremisesDefault to match "grind +suggestion"'s ordinary m…
JOSHCLUNE May 27, 2026
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
2 changes: 1 addition & 1 deletion Hammer/Options.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ register_option hammer.aesopPremisesDefault : Nat := {
}

register_option hammer.grindPremisesDefault : Nat := {
defValue := 32
defValue := 100
descr := "The default number of premises sent to grind"
}

Expand Down
14 changes: 11 additions & 3 deletions Hammer/ParallelismUtil.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,12 +103,20 @@ def wrapTactic {α : Type} (tactic : α → TacticM Unit) (cancelTk? : Option IO
Term.withoutModifyingElabMetaStateWithInfo do
let preCount := (← Core.getMessageLog).reportedPlusUnreported.size
let ngoals ← Term.withSynthesize (postpone := .no) do
Tactic.run mvar.mvarId! (tactic x)
Tactic.run mvar.mvarId! $ do
taskEventsRef.modify (·.push s!"Task {taskIdx} Tactic.run call started at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
tactic x
taskEventsRef.modify (·.push s!"Task {taskIdx} Tactic.run call ending at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
let tryThisDelta := coreMessageLogDelta preCount (← Core.getMessageLog)
if ngoals.isEmpty then
taskEventsRef.modify (·.push s!"Task {taskIdx} confirmed that all goals were resolved at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
let result ← instantiateMVars mvar
let result ← try inlineFreshProofs env0 result catch _ => return (none, tryThisDelta)
let result ←
try
inlineFreshProofs env0 result
catch _ =>
taskEventsRef.modify (·.push s!"Task {taskIdx} yielded a proof that couldn't be inlined at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
return (none, tryThisDelta)
if (← proofExprIncomplete result) then
taskEventsRef.modify (·.push s!"Task {taskIdx} confirmed to yield an incomplete proof at +{(← IO.monoMsNow) - buildParallelTacticsStart}ms")
return (none, tryThisDelta)
Expand Down Expand Up @@ -165,7 +173,7 @@ def tryAllTacsOnGoal (stxRef : Syntax) (outputAllSuggestions : Bool) (wallclockT
let mut taskIdx := 0
for tac in tacs do
let wrappedTac := (← wrapTactic (fun () => tac) cancelTk stxRef taskIdx buildParallelTacticsStart taskEventsRef) ()
let t ← BaseIO.asTask do
let t ← BaseIO.asTask (prio := Task.Priority.max) do
let startMs ← IO.monoMsNow
taskEventsRef.modify (·.push s!"Task {taskIdx} started at +{startMs - buildParallelTacticsStart}ms")
let r ← wrappedTac
Expand Down
53 changes: 47 additions & 6 deletions Hammer/Tactic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,11 @@ initialize
Lean.registerTraceClass `hammer.premises
Lean.registerTraceClass `hammer.profiling

register_option hammer.singleTacticParallel : Bool := {
defValue := false
descr := "A temporary option to test the impact of using tryAllTacsOnGoal"
}

namespace Hammer

open Lean Meta Elab Tactic HammerCore Syntax LibrarySuggestions Duper Aesop Qq Util
Expand Down Expand Up @@ -159,9 +164,27 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
trace[hammer.profiling] "Premise filtering took {(← IO.monoMsNow) - premiseFilteringStart}ms"
if configOptions.parallelism then
match configOptions.disableAesop, configOptions.disableAuto, configOptions.disableGrind with
| true, true, false => runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
| true, false, true => runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
| false, true, true => runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
| true, true, false =>
if hammer.singleTacticParallel.get (← getOptions) then
tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
evalTactic (← `(tactic| grind? [$grindParamStxs,*]))
]
else
runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
| true, false, true =>
if hammer.singleTacticParallel.get (← getOptions) then
tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions
]
else
runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
| false, true, true =>
if hammer.singleTacticParallel.get (← getOptions) then
tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions
]
else
runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
| false, false, true =>
tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions,
Expand Down Expand Up @@ -189,9 +212,27 @@ def runHammer (stxRef : Syntax) (simpLemmas : Syntax.TSepArray [`Lean.Parser.Tac
| true, true, true => throwError "Erroneous invocation of hammer: At least one of Aesop, Auto, and Grind must be enabled."
else
match configOptions.disableAesop, configOptions.disableAuto, configOptions.disableGrind with
| true, true, false => runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
| true, false, true => runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
| false, _, _ => runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
| true, true, false =>
if hammer.singleTacticParallel.get (← getOptions) then
tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
evalTactic (← `(tactic| grind? [$grindParamStxs,*]))
]
else
runSingularTactic (evalTactic (← `(tactic| grind? [$grindParamStxs,*])))
| true, false, true =>
if hammer.singleTacticParallel.get (← getOptions) then
tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions
]
else
runSingularTactic (runHammerCore stxRef simpLemmas autoPremises includeLCtx configOptions)
| false, _, _ =>
if hammer.singleTacticParallel.get (← getOptions) then
tryAllTacsOnGoal stxRef configOptions.outputAllSuggestions configOptions.wallclockTimeout [
runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions
]
else
runSingularTactic (runAesopWithSubprocedures autoPremises addIdentStxs grindPremiseNames includeLCtx configOptions)
| true, false, false => throwError "Erroneous invocation of hammer: Aesop or parallelism is needed to enable both Auto and Grind."
| true, true, true => throwError "Erroneous invocation of hammer: At least one of Aesop, Auto, and Grind must be enabled."

Expand Down
Loading