Permalink
Browse files

Add a formula for Ssreflect.

Ssreflect is an extension of Coq. It provides convenient notations,
several mathematical components, and other general purpose features.
The famous Four Colour Theorem was proved in Coq with the Ssreflect
extension.
  • Loading branch information...
1 parent 419857b commit 9e132182c38fbf35a07bcf489376a63b5776f5cb @mht208 committed Sep 10, 2012
Showing with 32 additions and 0 deletions.
  1. +32 −0 Library/Formula/ssreflect.rb
View
32 Library/Formula/ssreflect.rb
@@ -0,0 +1,32 @@
+require 'formula'
+
+class Ssreflect < Formula
+ homepage 'http://www.msr-inria.inria.fr/Projects/math-components'
+ url 'http://www.msr-inria.inria.fr/Projects/math-components/ssreflect-1.4-coq8.4.tar.gz'
+ version '1.4'
+ sha1 'c9e678a362973b202a5d90d2abf6436fa1ab4dcf'
+
+ depends_on 'objective-caml'
+ depends_on 'coq'
+
+ def install
+ ENV.j1
+
+ # Enable static linking.
+ inreplace 'Make' do |s|
+ s.gsub! /#\-custom/, '-custom'
+ s.gsub! /#SSRCOQ/, 'SSRCOQ'
+ end
+
+ args = ["COQBIN=#{HOMEBREW_PREFIX}/bin/",
+ "COQLIBINSTALL=lib/coq/user-contrib",
+ "COQDOCINSTALL=doc/coq",
+ "DSTROOT=#{prefix}/"]
+ system "make", *args
+ system "make", "install", *args
+ bin.install 'bin/ssrcoq.byte', 'bin/ssrcoq'
+ mkdir_p "#{share}/ssreflect"
+ cp "pg-ssr.el", "#{share}/ssreflect"
@adamv
adamv added a line comment Sep 10, 2012

These two lines can be:

(share/'ssreflect').install "pg-ssr.el"

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
+ end
+
+end

0 comments on commit 9e13218

Please sign in to comment.