update coq and compcert

Julien LepillerFri May 04 13:37:49+0200 2018

b434301

update coq and compcert

more/packages/ocaml.scm

434434 
(define-public compcert
435435 
  (package
436436 
    (name "compcert")
437-
    (version "3.1")
437+
    (version "3.2")
438438 
    (source (origin
439439 
              (method url-fetch)
440440 
              (uri (string-append "http://compcert.inria.fr/release/compcert-"
441441 
                                  version ".tgz"))
442442 
              (sha256
443443 
               (base32
444-
                "0irfwlw2chalp0g2gw0makc699hn3z37sha1a239p9d90mzx03cx"))))
444+
                "11q4121s0rxva63njjwya7syfx9w0p4hzr6avh8s57vfbrcakc93"))))
445445 
    (build-system gnu-build-system)
446446 
    (arguments
447447 
     `(#:phases
448448 
       (modify-phases %standard-phases
449-
         (add-before 'configure 'fix-newer-coq
450-
           (lambda _
451-
             (substitute* "configure"
452-
               (("8.6|8.6.1") "8.6|8.6.1|8.7.0"))
453-
             ;; functional induction is now defined in FunInd rather than in the
454-
             ;; toplevel.
455-
             (substitute* '("common/Globalenvs.v" "backend/ValueDomain.v")
456-
               (("Require Import Zwf")
457-
                "Require Import Zwf FunInd."))
458-
             (substitute* '("lib/Intv.v" "lib/Heaps.v" "lib/Parmov.v"
459-
                            "backend/Selectionproof.v" "backend/ValueAnalysis.v"
460-
                            "x86/CombineOpproof.v" "backend/Deadcodeproof.v")
461-
               (("Require Import Coqlib")
462-
                "Require Import Coqlib FunInd"))))
463449 
         (replace 'configure
464450 
           (lambda* (#:key outputs #:allow-other-keys)
465451 
             (zero? (system* "./configure" "x86_64-linux" "-prefix"

…

683669 
    (synopsis "")
684670 
    (description "")
685671 
    (license license:lgpl2.1+)))
672+
673+
(define-public coq-8.8
674+
  (package
675+
    (inherit coq)
676+
    (name "coq")
677+
    (version "8.8.0")
678+
    (source (origin
679+
              (method url-fetch)
680+
              (uri (string-append "https://github.com/coq/coq/archive/V"
681+
                                  version ".tar.gz"))
682+
              (file-name (string-append name "-" version ".tar.gz"))
683+
              (sha256
684+
               (base32
685+
                "0g96k2x6lbddlmkmdaczvcpb2gwqi1ydbq9bv4gf9q38kv9w3xya"))))))