CoqPilot refinement: Grazie bug fix, new limiting context model parameters, unsafe code refactor

[GlebSolovev]

• 🐞 Fixed GrazieService bug. Resolved an issue where it generated choices + 1 proofs instead of the expected choices. This was caused by an improperly updated loop after a prior refactor.

• 🆕 Added and tested new model parameters. Introduced maxContextTheoremsNumber and multiroundProfile.maxPreviousProofVersionsNumber to better control the context sent to LLMs.

  • Previously, users could only limit the context by adjusting tokensToGenerate, but these new parameters provide a more intuitive and precise way to manage it.
  • These additions are essential for experiments exploring how premises influence CoqPilot's proof generation capabilities.

• 💂‍♂️ Refactored potentially unsafe code:

  • In the project's early stages, we (or at least I) sometimes used misleading as type casts without realizing they only perform compile-time checks and have no effect at runtime. These cases have now been reviewed, and misleading casts were replaced with proper runtime checks or refactored entirely.
  • Updated constructors for all custom errors to ensure consistent and reliable typing in all scenarios, following the approach established in the last benchmarking framework refactor.
  • Revised and refactored error-throwing code: replaced most of the generic Error-s with more specific ones using previously introduced error-utils wrappers.

[GlebSolovev]

Ran CI manually, it passes: https://github.com/JetBrains-Research/coqpilot/actions/runs/13030842228