🍺 BREW Explorer

← all formulae

proof-general

brew install proof-general v4.5 GPL-3.0-or-later

Emacs-based generic interface for theorem provers

3
30-day installs · #12004
11
90-day · #11541
88
365-day · #9542

Runtime dependencies

Build dependencies

Links

Caveats

HTML documentation is available in: $HOMEBREW_PREFIX/share/doc/proof-general
Raw metadata
{
  "aliases": [],
  "alternatives": [],
  "build_dependencies": [
    "texi2html",
    "texinfo"
  ],
  "categories": [],
  "caveats": "HTML documentation is available in: $HOMEBREW_PREFIX/share/doc/proof-general\n",
  "conflicts_with": [],
  "dependencies": [
    "emacs"
  ],
  "deprecated": 0,
  "deprecation_reason": null,
  "desc": "Emacs-based generic interface for theorem provers",
  "disable_reason": null,
  "disabled": 0,
  "enrichment_fetched_at": null,
  "first_seen": "2026-06-20T23:34:18+00:00",
  "full_name": "proof-general",
  "github_default_branch": null,
  "github_last_commit_at": null,
  "github_readme_excerpt": null,
  "github_repo": null,
  "github_stars": null,
  "github_topics": [],
  "homepage": "https://proofgeneral.github.io",
  "homepage_og_description": null,
  "homepage_og_image": null,
  "homepage_title": null,
  "installs_30d": 3,
  "installs_365d": 88,
  "installs_90d": 11,
  "keg_only": 0,
  "keg_only_reason": null,
  "last_seen": "2026-06-20T23:34:18+00:00",
  "license": "GPL-3.0-or-later",
  "llm_generated_at": null,
  "llm_model": null,
  "name": "proof-general",
  "oldnames": [],
  "one_liner": null,
  "optional_dependencies": [],
  "rank_30d": 12004,
  "rank_365d": 9542,
  "rank_90d": 11541,
  "raw_hash": "0352af6a011ca69e",
  "recommended_dependencies": [],
  "revision": 0,
  "ruby_source_path": "Formula/p/proof-general.rb",
  "tap": "homebrew/core",
  "test_dependencies": [],
  "uses_from_macos": [],
  "version_head": "HEAD",
  "version_stable": "4.5",
  "versioned_formulae": [],
  "why_use_this": null
}