Major LLM services and UI improvement

[GlebSolovev]

Changes summary

⏳ Estimate time for LLM services to become available via logging proof-generation requests

• Implement GenerationsLogger
  • capable of thoroughly logging all LLM service generation requests in a human-readable way, which can be useful for debugging too;
  • with support of censorship for sensitive data (for example, API keys).
• Implement a default algorithm to estimate the time for LLM service to become available.

🕵️ Support proper logging and error handling inside LLMService-s

• Introduce hierarchy for LLMService errors: LLMServiceError, ConfigurationError, RemoteConnectionError, GenerationFailedError.
• Handle these errors properly inside LLMService implementation:
  • throw different errors for different causes;
  • repack errors where needed.
• Implemented proper logging based on the errors thrown: with both EventsLogger and GenerationsLogger.
• Introduce LLMServiceRequest to make data transfer coherent between different logic modules.
• Design and implement interaction between LLMService-s and UI to report errors.

🏯 Rework LLMService arhcitecture

• Introduce and implement LLMServiceInternal that:
  • separates and hides the actual implementation of the interaction with a model;
  • restricts the visibility of some methods and properties;
  • provides a convenient way to support new services easily via wrapper methods.
• Rework facade classes and methods of LLMService to make them both concise and powerful.
• Design and support complete and powerful typing for LLMService classes based on recursive generics.
  • That makes any further development involving LLMService-s safer and easier.
• Document core LLMService architecture.

✅ Test everything

• Test the LLM services module completely:
  • including facade, core and utility functionality;
  • via both unit and integration tests, with the use of stress testing and asynchronous behaviour;
  • in total, about 150 new tests.
• Improve test infrastructure in general:
  • introduce a lot of utility functions and mocks;
  • structure them properly.
• Fix minor bugs and make minor improvements detected by tests.

🚀 Fix & improve CI

• Fix the issue with building a test Coq project resource.
• Thereby, make previously "non-CI" tests successfully pass on CI.
• Set up CI debugging for future needs.
  • Now it is possible to connect to the running GitHub-Actions worker by SSH and debug the environment. This mode activates only in case any task fails.
• Enable launching CI manually.
• Double the speed of CI by setting up caches for ocaml and opam dependencies.

🤝 Improve LLM services' parameters: their naming, transparency, description

• Introduce modelId to distinguish a model identifier from the name of an OpenAI / Grazie model.
• Rename newMessageMaxTokens to maxTokensToGenerate for greater clarity.
• Add defaultChoices to ModelParams to make its resolution more transparent in the code.
• Update the settings description, and make it more user-friendly.

🕊 Rework and significantly improve settings validation

• Improve Ajv schemas for the parameters.
• Refactor validation errors to one SettingsValidationError,
  • which supports hints for the settings to open.
• Move all input parameters validation to one place and make it coherent.
• Add some general checks:
  • input models have unique modelId-s;
  • there are models to generate proofs with.
• Design and implement a powerful parameters resolver framework that:
  • makes it possible for LLM services to resolve input parameters (with overrides and defaults) and validate them;
  • makes it possible for developers to specify parameters resolution in a declarative way;
  • provides great compile-time type checks for developers;
  • is well-documented.
• Significantly improve messages shown to users:
  • improve existing ones;
  • support messages about parameter resolution: both failures and unexpected overrides.
• Decipher Ajv errors and make them clear both in UI and for debugging.

💚🤖 Improve interaction with OpenAI

• Handle OpenAI runtime errors and repacked them into clear configuration errors, shown to users.
• Specify default token parameters for OpenAIService:
  • gather values for various models from different sources;
  • implement an algorithm to resolve maxTokensToGenerate appropriately.

🌿 Improve code quality

• Split CoqPilot into smaller pieces.
• Make throwing Error coherent.
• Get rid of unnecessary any-s.
• Output values coherently.
• Make an order of LLM services coherent.
• Improve linters' configuration.

[K-dizzled]

Need to add .nvmrc file and fix the node version

[GlebSolovev]

Yup, made it pretty much the same as you did in ai_agents_server and also used it on CI

[K-dizzled]

Why is the textual file format best for the logs?

[GlebSolovev]

It is a good question to be answered indeed, including the docs. I left a note at GenerationsLogger's docs about the possible performance overhead and how to resolve the issue if it arises in practice one day.

No worries for now though, neither tests nor I didn't experience any problems, on the opposite, only +vibes from working with human-readable logs during debugging 🕊