add why3

LEPILLER JulienFri Jun 30 09:25:06+0200 2017

af9e443

add why3

more/packages/smt.scm

2323 
  #:use-module (guix build-system python)
2424 
  #:use-module ((guix licenses) #:prefix license:)
2525 
  #:use-module (gnu packages)
26+
  #:use-module (gnu packages ocaml)
2627 
  #:use-module (gnu packages python)
2728 
  #:use-module (more packages python))
2829 
…
108109 
    (synopsis "Claripy is a abstracted constraint-solving wrapper")
109110 
    (description "Claripy is a abstracted constraint-solving wrapper.")
110111 
    (license license:bsd-2)))
112+
113+
(define-public why3
114+
  (package
115+
    (name "why3")
116+
    (version "0.87.3")
117+
    (source (origin
118+
              (method url-fetch)
119+
              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36398/why3-"
120+
                                  version ".tar.gz"))
121+
              (sha256
122+
               (base32
123+
                "1fn9v6w1ilkrm2n4rz31w8qvjnchyvwxiqs67z3f59b5k99wb2ka"))))
124+
    (build-system gnu-build-system)
125+
    (native-inputs
126+
     `(("ocaml" ,ocaml)))
127+
    (propagated-inputs
128+
     `(("menhir" ,ocaml-menhir)))
129+
    (arguments
130+
     `(#:tests? #f))
131+
       ;#:phases
132+
       ;(modify-phases %standard-phases
133+
       ;  (replace 'check
134+
       ;    (lambda _
135+
       ;      (zero? (system* "make" ;"test-ocaml-extraction"
136+
       ;                      "test-runstrat" "test-coq-tactic.opt"
137+
       ;                      "test-coq-tactic.byte" "test-session.opt"
138+
       ;                      "test-session.byte" "test-api-mlw.opt"
139+
       ;                      "test-api-mlw.byte" "test-api-mlw-tree.opt"
140+
       ;                      "test-mlw-tree.byte" "test-api-logic.opt"
141+
       ;                      "test-api-logic.byte")))))))
142+
    (home-page "http://why3.lri.fr")
143+
    (synopsis "")
144+
    (description "")
145+
    (license license:lgpl2.1)))