Major LLM services and UI improvement

Changes summary

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.

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.

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 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 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.

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.

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.

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.