Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The grind tactic is generating nondeterministic proofs.

By forcing Lean to re-run grind in the following snippet (by e.g. commenting and un-commenting out the theorem), the hash value that is printed varies, I see: 1643531141, 3675229656, 2808797072 from 5 tries.

Link to live.lean-lang.org

import Lean.Elab.Command

theorem extracted_1_3 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
  ifpnf ≠ 0 →
    pBf + ppB = pB * (1 / ifpnf) + ppB → -- if we remove ppB from both sides, this becomes deterministic again??
      ifpnf / (ppB * ifpnf + pB) = 1 / (ppB + pBf)
  := by grind only [cases Or]

open Lean
run_cmd
  let env ← getEnv
  let some (.thmInfo ci) := env.find? ``extracted_1_3._proof_1_1
    | throwError ""
  println! ci.value.hash

Context

This was discovered by @digama0 while debugging some issues in Mathlib CI: #mathlib4 > Failing CI @ 💬 (All I did was minimize the example and write this issue.)

Steps to Reproduce

1. Click this link
2. Note the value of the hash printed by the run_cmd
3. comment and uncomment the theorem
4. Note that the value of the hash may now be different

Expected behavior: The hash value for the proof generated by grind should be deterministic.

Actual behavior: The hash value for the proof generated by grind is nondeterministic.

Versions

[Output of #version or #eval Lean.versionString]
[OS version, if not using live.lean-lang.org.]

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.