Function main

scripts/rubi/translate.ts:52–172

()

}

function main(): void {
  const argv = process.argv;
  let rubi =
    process.env.RUBI_HOME ??
    path.join(os.homedir(), `dev/rubi/Rubi-${RUBI_VERSION}`);
  // `--section` may be repeated to translate several chapters into one corpus
  // (e.g. ch1 + ch4); the combined file list keeps each chapter's rules in
  // their own files, so per-file rule order — Rubi's match priority — is
  // preserved. No `--section` means the whole corpus.
  const sections: string[] = [];
  let out = 'data/rubi';
  for (let i = 2; i < argv.length; i++) {
    switch (argv[i]) {
      case '--rubi':
        rubi = argv[++i];
        break;
      case '--section':
        sections.push(argv[++i]);
        break;
      case '--out':
        out = argv[++i];
        break;
      default:
        console.error(`unknown option ${argv[i]}`);
        process.exit(2);
    }
  }

  const rulesRoot = path.join(rubi, 'Rubi/IntegrationRules');
  const files = (sections.length ? sections : [''])
    .flatMap((s) => listRuleFiles(rulesRoot, s))
    .sort();
  console.log(`translating ${files.length} rule files from ${rulesRoot}`);

  let totalRules = 0;
  let totalErrors = 0;
  const skipped: {
    file: string;
    index: number;
    error: string;
    source: string;
  }[] = [];
  const perFile: { file: string; rules: number; errors: number }[] = [];

  for (const file of files) {
    const { rules, errors } = extractRules(path.join(rulesRoot, file));
    totalRules += rules.length;
    totalErrors += errors.length;
    for (const e of errors) skipped.push({ file, ...e });
    perFile.push({ file, rules: rules.length, errors: errors.length });

    const target = path.join(out, 'corpus', file.replace(/\.m$/, '.json'));
    fs.mkdirSync(path.dirname(target), { recursive: true });
    // Compact, one rule per line: diffable per-rule, small on disk.
    fs.writeFileSync(
      target,
      `{"schemaVersion":1,"file":${JSON.stringify(file)},"rules":[\n` +
        rules.map((r) => JSON.stringify(r)).join(',\n') +