Code

Benchmarking framework hot-fixes#49

Code

Merged

K-dizzled merged 9 commits intov2.4.0-devJetBrains-Research/coqpilot:v2.4.0-devfrom benchmarking-hotfixesJetBrains-Research/coqpilot:benchmarking-hotfixesCopy head branch name to clipboardNov 27, 2024

+87-58

Commits

Commits on Nov 26, 2024

• Clarify abort controller usage at parsing stage of benchmarking

  GlebSolovev

  committed
  0fc8d1d

  Copy full SHA for 0fc8d1d

• Support initial_goal being optional inside benchmarking

  GlebSolovev

  committed
  e867f00

  Copy full SHA for e867f00

• Get initial_goal cached more often

  GlebSolovev

  committed
  7dcd906

  Copy full SHA for 7dcd906

• Make needsTheoremInitialGoals required

  GlebSolovev

  committed
  35130f8

  Copy full SHA for 35130f8

• Fix bug with different o1 class models name in Grazie

  K-dizzled

  committed
  2eb29a1

  Copy full SHA for 2eb29a1

Commits on Nov 27, 2024

• Add TODO for initial-goals flag support inside benchmarking

  GlebSolovev

  committed
  477a0e8

  Copy full SHA for 477a0e8

• Fix multi-workspaces "pre" script

  GlebSolovev

  committed
  b1cd890

  Copy full SHA for b1cd890

• Provide benchmark-test task for faster development

  GlebSolovev

  committed
  86ec217

  Copy full SHA for 86ec217

• Add notes on COQ_LSP_PATH to benchmarking docs

  GlebSolovev

  committed
  d5dda34

  Copy full SHA for d5dda34