Issues

• proofStep discards the message log on failure, so elaboration errors surface only as internal exception #N

  leanprover-community/repl#164 · Filter by author haeliotang opened on Aug 8, 2026

• Uncompatible lean version for different libraries

  leanprover-community/repl#125 · Filter by author MarkJYC001 opened on Aug 11, 2025
  1

• [proposal]Make request parsing more robust

  leanprover-community/repl#122 · Filter by author Qiu233 opened on Jul 15, 2025

• Want to parse ast even in invalid proof.

  leanprover-community/repl#118 · Filter by author shanjiaming opened on Jul 6, 2025

• Lean Repl unable to run with canonical

  leanprover-community/repl#115 · Filter by author FrederickPu opened on Jul 1, 2025
  16

• Local instances not captured correctly in term sorries

  leanprover-community/repl#107 · Filter by author augustepoiroux opened on Jun 27, 2025

• [feature request] Option for pickling imported environment completely, not just diff from imports - so that they can be recovered fast in one command without re-doing the fully-fledged imports

  leanprover-community/repl#95 · Filter by author vadimkantorov opened on Apr 29, 2025

• [feature request] Built-in command timeout support

  leanprover-community/repl#94 · Filter by author vadimkantorov opened on Apr 29, 2025
  1

• CPU usage

  leanprover-community/repl#91 · Filter by author vadimkantorov opened on Apr 22, 2025
  1

• Fork safety

  leanprover-community/repl#87 · Filter by author vadimkantorov opened on Apr 18, 2025
  2

• How to solve the input issue of the v4.8 repl server?

  leanprover-community/repl#86 · Filter by author Kouer-www opened on Apr 17, 2025
  1

• Server mode

  leanprover-community/repl#84 · Filter by author vadimkantorov opened on Apr 15, 2025
  12

• INTERNAL PANIC: Error when Pickling Proof State

  leanprover-community/repl#81 · Filter by author RexWzh opened on Apr 7, 2025

• LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

  leanprover-community/repl#77 · Filter by author FrederickPu opened on Mar 29, 2025
  29

• information returned by repl is inconsistent with the information returned by lean info.

  leanprover-community/repl#76 · Filter by author tsuki8 opened on Mar 4, 2025
  4

• pattern-matching in theorem signature causes unknown constant 'foo.match_1'

  leanprover-community/repl#66 · Filter by author llllvvuu opened on Jan 8, 2025
  1

• Pickling-unpickling an environment makes definitions noncomputable?

  leanprover-community/repl#62 · Filter by author augustepoiroux opened on Dec 15, 2024

• Goals of tactics often lose line breaks

  leanprover-community/repl#58 · Filter by author caochenrui opened on Oct 12, 2024

• [Question] (automatically) Including imports

  leanprover-community/repl#53 · Filter by author Manuscrit opened on Aug 9, 2024

• [BUG] REPL accepts incorrect proofs

  leanprover-community/repl#44 · Filter by author amit9oct opened on May 29, 2024
  36

• Issues while executing tactics with ; in them.

  leanprover-community/repl#43 · Filter by author amit9oct opened on May 27, 2024
  2

• Bugs for metavariable '?[anonymous]' when setting "allTactics" as true

  leanprover-community/repl#42 · Filter by author xinhjBrant opened on May 26, 2024
  2

• Failed to input the tactics step-by-step within a case block

  leanprover-community/repl#25 · Filter by author ohyeat opened on Dec 18, 2023
  3

• Repl doesn't return any output?

  leanprover-community/repl#16 · Filter by author Kreijstal opened on Oct 30, 2023
  7

• Iterative execution of proofs

  leanprover-community/repl#6 · Filter by author zhangir-azerbayev opened on May 2, 2023
  2