Skip to content

Conversation

@lykimq
Copy link
Contributor

@lykimq lykimq commented Nov 13, 2025

Depends on #357. This PR is a bit big but it can be review per commit.

This PR removes all the hardcoded logic (fallback compatibility from the previous PR #357) and makes the bot fully generic.

What changed

Removed all hardcoded repo checks

  • Removed hardcoded checks for "rocq-prover"/"rocq", "math-comp", "rocq-community"
  • All repository-specific behavior now controlled via TOML configuration
  • No fallback compatibility - repos must have explicit config or rely on auto-detection/defaults

3-Tier configuration

How bot is generic

Before (hardcoded):

if owner = "rocq-prover" && repo = "rocq" then 
  (* special rocq logic *)
else 
  (* generic logic *)

Now (generic):

match get_repo_config_opt ~owner ~repo repo_config_table with
  | Some config ->
     (* use config values - works for any repo *)
      if Option.is_some config.github_project_number then 
         (* Backport enabled *)
  | None -> (* no config - skip feature *)

Feature checks

All features are optional and disabled if not configured:

  • github_project_number: enable backport
  • gitlab_domain: enable GitLab mirror
  • minimizer_url: enable minimization
  • jobs.custom_job_status: enable custom job status CI
  • jobs.bench: enable bench detection

Configuration Priority

Explicit TOML > API auto-detection > Generic defaults

Tier 1: Explicit TOML (highest priority)

  • Values explicitly set in coqbot-config.toml

Tier 2: API Auto-Detection (medium priority)

  • Fetched from GitHub/GitLab APIs when missing
  • Cached for 1 hour (hardcoded TTL) to avoid rate limits
  • Timeout configurable via bot.api_timeout (TOML in [bot] section) or API_TIMEOUT env var (default: 5.0 seconds)
  • Example: auto-detect org_name from GitHub API

Tier 3: Generic Defaults (lowest priority)

  • Works for any repository
  • Example: team_name = "maintainers"

Key components

1. src/config

  • repo_config.ml: Parses TOML repo configs
  • default.ml: Provides generic defaults for any repo
  • auto_detection.ml: API-based auto-detection with caching
  • config_resolver.ml: Merges explicit/auto/default with priority
  • cache.ml: 1-hour TTL cache for auto-detection results (hardcoded)

2. src/webhooks/

  • github.ml and gitlab.ml now use repo_config_table (no hardcoded checks)

3. src/actions/

  • backport.ml: Enabled via config.github_project_number
  • job.ml: Uses config.jobs.bench and config.jobs.custom_job_status
  • pr_sync.ml: Uses config.org_name, config.team_name, config.ci_config

4. bot-components

  • Moved init_git_bare_repository from src/utils/helpers.ml (removed) to Git_utils.ml
  • Added in GitHub_queries.ml (used for auto-detection):
    • get_repository_info: Get repository info (owner, default branch)
    • get_organization_teams: Get all teams for an organization
    • get_all_labels: Get all labels for a repository
    • All queries support configurable timeout (defaults to bot_info.api_timeout)
  • Added GitHub_GraphQL:
    • GetRepositoryInfo: GraphQL query for repo info (owner, default branch)
    • GetOrganizationTeams: for organization team
    • GetRepositoryLabels: for repo labels
  • Added in GitLab_queries.ml:
    • search_projects: Search for projects matching a term - detect GitLab domain/owner/repo
    • get_ci_config_file: Get CI config file content
    • All queries support configurable timeout (defaults to bot_info.api_timeout)
  • Added in GitLab_GraphQL:
    • SearchProjects: query to search for GitLab projects
    • GetCIConfigFile: query to get CI config file content (.gitlab-ci.yml or .gitlab-ci.yaml)

Configuration priority examples

  • minimizer_url: TOML [repositories.*] minimizer_url > Env var BOT_MINIMIZER_URL > None
  • api_timeout: TOML [bot] api_timeout > Env var API_TIMEOUT > Default 5.0

Example to set up the bot

Minimal setup

[repositories.my-repo]
github = "my-org/my-repo"

What happens:

  • Bot parses github = "my-org/my-repo"
  • Auto-detection runs (if needed):
    • Detects GitLab domain via API search
    • Detects org/team from GitHub API
    • Caches results for 1 hour
  • Defaults applied:
    • gitlab_domain = "gitlab.com"
    • org_name = "my-org"
    • team_name = "maintainers"
  • Repository works with basic features

Full-featured setup (like Rocq) - see coqbot-config.toml

[repositories.rocq]
github = "rocq-prover/rocq"
github_project_number = "11"          # Enables backport feature
gitlab_domain = "gitlab.inria.fr"     # Custom GitLab instance
gitlab_owner = "coq"
gitlab_repo = "coq"
org_name = "rocq-prover"
team_name = "contributors"
minimizer_url = "https://..."         # Enables minimization

[repositories.rocq.jobs]
bench = "bench"                       # Bench job detection
custom_job_status = true              # Custom CI handling

What this enables:

  • Backport feature via github_project_number
  • GitLab mirroring via gitlab_domain
  • Bug minimization via minimizer_url
  • Bench job detection via jobs.bench
  • Custom job status via jobs.custom_job_status

Test Coverage

  • config_resolver_test: 3-tier priority system
  • auto_detection_test, cache_test: API-based detection with caching
  • default_config_test: Generic defaults for any repo
  • integration_test, repo_config_integration_test: End-to-end workflows
  • config_timeout_test: TOML and env var priority
  • generic_bot_demo_test: Demonstration tests showing how the bot config system works

kim.ly and others added 30 commits November 14, 2025 10:59
…fig,

fallback to the original hardcoded for backward compability
error handling.
- make timeout configurable with bot_info, default is 5.0 if not set
becomes generic functions instead of rocq-specific ones
…rences, add api_timeout, fix run_bench calls
@lykimq lykimq changed the title Generic bot configuration System Draft: Generic bot configuration System Nov 24, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants