Troubleshooting

Common Issues

Socket Mode Connection Errors

  • Ensure pet-server is running: pet-server -p 8765

  • Verify port availability and network connectivity

  • Check firewall settings if connecting remotely

Subprocess Mode Errors

  • Ensure pet command is available in PATH: which pet

  • Verify coq-lsp installation includes the pet binary

  • Check that the pet process can access your Rocq/Coq files

File Path Issues

  • Use absolute paths or ensure working directory is correct

  • Check file exists and has proper Coq/Rocq syntax

  • Ensure workspace is set correctly with client.set_workspace()

Installation Issues

  • Ensure coq-lsp is properly installed with both pet and pet-server

  • Install lwt and logs before coq-lsp (required for both modes)

  • Verify installation: pet --version and pet-server --version

Performance Considerations

  • Socket mode: Better for multiple clients or long-running sessions

  • Subprocess mode: Better for single-client usage or automation

  • Choose the appropriate mode based on your use case