7 files changed, 50 insertions, 0 deletions
diff --git a/homebrew/proofgeneral/.beer b/homebrew/proofgeneral/.beer
new file mode 100644
index 000000000..83027c2a5
--- /dev/null
+++ b/homebrew/proofgeneral/.beer
@@ -0,0 +1,39 @@
+{
+    "name": "ProofGeneral",
+    "description": "Emacs-based generic interface for theorem provers",
+    "url": "https://github.com/ProofGeneral/PG/archive/v4.4.tar.gz",
+    "mirror": null,
+    "homepage": "https://proofgeneral.github.io",
+    "depends": [
+        {
+            "depend": "texi2html",
+            "build-depend": true
+        },
+        {
+            "depend": "texinfo",
+            "build-depend": true
+        },
+        {
+            "depend": "emacs",
+            "build-depend": false
+        }
+    ],
+    "resource": [],
+    "conflicts": [],
+    "patches": [],
+    "install": [
+        "ENV.deparallelize ",
+        "args = %W[",
+        "PREFIX=#{prefix}",
+        "DEST_PREFIX=#{prefix}",
+        "ELISPP=share/emacs/site-lisp/proof-general",
+        "ELISP_START=#{elisp}/site-start.d",
+        "EMACS=#{which \"emacs\"}",
+        "]",
+        "system \"make\", \"install\", *args",
+        "cd \"doc\" do",
+        "system \"make\", \"info\", \"html\""
+    ],
+    "version": "4.4",
+    "file": "proof-general.rb"
+}
+\ No newline at end of file
diff --git a/homebrew/proofgeneral/.make.sh-auto b/homebrew/proofgeneral/.make.sh-auto
new file mode 100644
index 000000000..7d39b6ee1
--- /dev/null
+++ b/homebrew/proofgeneral/.make.sh-auto
@@ -0,0 +1,6 @@
+pkg:setup
+ENV.deparallelize 
+args = %W[PREFIX=#{prefix} DEST_PREFIX=#{prefix} ELISPP=share/emacs/site-lisp/proof-general ELISP_START=#{elisp}/site-start.d EMACS=#{which "emacs"} ]
+make DESTDIR=${PKG_DEST} install *args
+cd "doc" 
+make info html
diff --git a/homebrew/proofgeneral/_metadata/description b/homebrew/proofgeneral/_metadata/description
new file mode 100644
index 000000000..5514c790c
--- /dev/null
+++ b/homebrew/proofgeneral/_metadata/description
@@ -0,0 +1 @@
+Emacs-based generic interface for theorem provers
diff --git a/homebrew/proofgeneral/_metadata/homepage b/homebrew/proofgeneral/_metadata/homepage
new file mode 100644
index 000000000..fc1d48c31
--- /dev/null
+++ b/homebrew/proofgeneral/_metadata/homepage
@@ -0,0 +1 @@
+https://proofgeneral.github.io
diff --git a/homebrew/proofgeneral/_metadata/name b/homebrew/proofgeneral/_metadata/name
new file mode 100644
index 000000000..d6e10bc1f
--- /dev/null
+++ b/homebrew/proofgeneral/_metadata/name
@@ -0,0 +1 @@
+ProofGeneral
diff --git a/homebrew/proofgeneral/_metadata/version b/homebrew/proofgeneral/_metadata/version
new file mode 100644
index 000000000..515be8f91
--- /dev/null
+++ b/homebrew/proofgeneral/_metadata/version
@@ -0,0 +1 @@
+4.4
diff --git a/homebrew/proofgeneral/download.sh b/homebrew/proofgeneral/download.sh
new file mode 100755
index 000000000..4066ecd25
--- /dev/null
+++ b/homebrew/proofgeneral/download.sh
@@ -0,0 +1 @@
+wget https://github.com/ProofGeneral/PG/archive/v4.4.tar.gz
+\ No newline at end of file