Skip to content

Fix tactic suggestion formatting bug#64

Merged
Peiyang-Song merged 1 commit intolean-dojo:mainfrom
Peiyang-Song:main
Apr 3, 2024
Merged

Fix tactic suggestion formatting bug#64
Peiyang-Song merged 1 commit intolean-dojo:mainfrom
Peiyang-Song:main

Conversation

@Peiyang-Song
Copy link
Member

Fix tactic suggestion formatting bug

  • Remove extra spacing issue for suggest_tactics.
  • Respond to issue Proof Suggestion Format Issue #63 .
  • Add an extra logging to print raw tactics returned by LLMs when in verbose mode.

@Peiyang-Song Peiyang-Song added the bug Something isn't working label Apr 3, 2024
@Peiyang-Song Peiyang-Song self-assigned this Apr 3, 2024
@Peiyang-Song Peiyang-Song merged commit d99af09 into lean-dojo:main Apr 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant