Merge branch 'master' into core-updates

1 files changed, 695 insertions, 477 deletions

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 3b1ddcb5b6..28f1c99e4c 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -10,6 +10,9 @@
 ;;; Copyright © 2017 Ben Woodcroft <donttrustben@gmail.com>
 ;;; Copyright © 2017, 2018 Tobias Geerinckx-Rice <me@tobias.gr>
 ;;; Copyright © 2018 Peter Kreye <kreyepr@gmail.com>
+;;; Copyright © 2018, 2019 Gabriel Hondet <gabrielhondet@gmail.com>
+;;; Copyright © 2018 Kei Kebreau <kkebreau@posteo.net>
+;;; Copyright © 2019 Ricardo Wurmus <rekado@elephly.net>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -34,8 +37,8 @@
   #:use-module (gnu packages boost)
   #:use-module (gnu packages compression)
   #:use-module (gnu packages curl)
-  #:use-module (gnu packages databases)
   #:use-module (gnu packages emacs)
+  #:use-module (gnu packages emacs-xyz)
   #:use-module (gnu packages flex)
   #:use-module (gnu packages gcc)
   #:use-module (gnu packages ghostscript)
@@ -46,6 +49,7 @@
   #:use-module (gnu packages libffi)
   #:use-module (gnu packages llvm)
   #:use-module (gnu packages m4)
+  #:use-module (gnu packages maths)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages ncurses)
   #:use-module (gnu packages pcre)
@@ -54,6 +58,7 @@
   #:use-module (gnu packages protobuf)
   #:use-module (gnu packages python)
   #:use-module (gnu packages sdl)
+  #:use-module (gnu packages sqlite)
   #:use-module (gnu packages tex)
   #:use-module (gnu packages texinfo)
   #:use-module (gnu packages time)
@@ -64,6 +69,7 @@
   #:use-module (gnu packages xml)
   #:use-module (gnu packages xorg)
   #:use-module (guix build-system dune)
+  #:use-module (guix build-system emacs)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system ocaml)
   #:use-module (guix download)
@@ -186,19 +192,18 @@ patch-/bin/sh-references: ~a: changing `\"/bin/sh\"' to `~a'~%"
                     (mandir (string-append out "/share/man")))
                ;; Custom configure script doesn't recognize
                ;; --prefix=<PREFIX> syntax (with equals sign).
-               (zero? (system* "./configure"
-                               "--prefix" out
-                               "--mandir" mandir)))))
+               (invoke "./configure"
+                       "--prefix" out
+                       "--mandir" mandir))))
          (replace 'build
            (lambda _
-             (zero? (system* "make" "-j" (number->string
-                                          (parallel-job-count))
-                             "world.opt"))))
+             (invoke "make" "-j" (number->string (parallel-job-count))
+                     "world.opt")))
          (delete 'check)
          (add-after 'install 'check
            (lambda _
              (with-directory-excursion "testsuite"
-               (zero? (system* "make" "all")))))
+               (invoke "make" "all"))))
          (add-before 'check 'prepare-socket-test
            (lambda _
              (format (current-error-port)
@@ -249,7 +254,7 @@ functional, imperative and object-oriented styles of programming.")
            (replace 'build
              (lambda _
                ;; Specifying '-j' at all causes the build to fail.
-               (zero? (system* "make" "world.opt"))))
+               (invoke "make" "world.opt")))
            ,@(if (string=? "aarch64-linux" (%current-system))
                ;; Custom configure script doesn't recongnize aarch64.
                '((replace 'configure
@@ -264,11 +269,9 @@ functional, imperative and object-oriented styles of programming.")
            (replace 'check
              (lambda _
                (with-directory-excursion "testsuite"
-                 (zero? (system*
-                         "make"
-                         "all"
+                 (invoke "make" "all"
                          (string-append
-                          "TOPDIR=" (getcwd) "/.."))))))))))))
+                          "TOPDIR=" (getcwd) "/..")))))))))))
 
 (define-public ocaml-4.07
   (package
@@ -297,46 +300,46 @@ functional, imperative and object-oriented styles of programming.")
 (define-public ocaml ocaml-4.07)
 
 (define-public ocamlbuild
-	  (package
-	    (name "ocamlbuild")
-	    (version "0.13.1")
-	    (source (origin
-	              (method url-fetch)
-	              (uri (string-append "https://github.com/ocaml/ocamlbuild/archive/"
-	                                  version ".tar.gz"))
-	              (file-name (string-append name "-" version ".tar.gz"))
-	              (sha256
-	               (base32
-	                "1320cfkixs1xlng5av04pa5qjb3ynvi2kl3k1ngqzg5fpi29b0vr"))))
-	    (build-system gnu-build-system)
-	    (arguments
-	     `(#:test-target "test"
-	       #:tests? #f; tests require findlib
-	       #:make-flags
-	       (list (string-append "OCAMLBUILD_PREFIX=" (assoc-ref %outputs "out"))
-	             (string-append "OCAMLBUILD_BINDIR=" (assoc-ref %outputs "out")
-                                "/bin")
-	             (string-append "OCAMLBUILD_LIBDIR=" (assoc-ref %outputs "out")
-                                "/lib/ocaml/site-lib")
-	             (string-append "OCAMLBUILD_MANDIR=" (assoc-ref %outputs "out")
-                                "/share/man"))
-	       #:phases
-	       (modify-phases %standard-phases
-	         (delete 'bootstrap)
-	         (delete 'configure)
-	         (add-before 'build 'findlib-environment
-	           (lambda* (#:key outputs #:allow-other-keys)
-	             (let* ((out (assoc-ref outputs "out")))
-	               (setenv "OCAMLFIND_DESTDIR" (string-append out "/lib/ocaml/site-lib"))
-	               (setenv "OCAMLFIND_LDCONF" "ignore")
-	               #t))))))
-	    (native-inputs
-	     `(("ocaml" ,ocaml)))
-	    (home-page "https://github.com/ocaml/ocamlbuild")
-	    (synopsis "OCaml build tool")
-	    (description "OCamlbuild is a generic build tool, that has built-in rules
-	for building OCaml library and programs.")
-	    (license license:lgpl2.1+)))
+  (package
+    (name "ocamlbuild")
+    (version "0.13.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://github.com/ocaml/ocamlbuild/archive/"
+                                  version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "1320cfkixs1xlng5av04pa5qjb3ynvi2kl3k1ngqzg5fpi29b0vr"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "test"
+       #:tests? #f; tests require findlib
+       #:make-flags
+       (list (string-append "OCAMLBUILD_PREFIX=" (assoc-ref %outputs "out"))
+             (string-append "OCAMLBUILD_BINDIR=" (assoc-ref %outputs "out")
+                        "/bin")
+             (string-append "OCAMLBUILD_LIBDIR=" (assoc-ref %outputs "out")
+                        "/lib/ocaml/site-lib")
+             (string-append "OCAMLBUILD_MANDIR=" (assoc-ref %outputs "out")
+                        "/share/man"))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'bootstrap)
+         (delete 'configure)
+         (add-before 'build 'findlib-environment
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let* ((out (assoc-ref outputs "out")))
+               (setenv "OCAMLFIND_DESTDIR" (string-append out "/lib/ocaml/site-lib"))
+               (setenv "OCAMLFIND_LDCONF" "ignore")
+               #t))))))
+    (native-inputs
+     `(("ocaml" ,ocaml)))
+    (home-page "https://github.com/ocaml/ocamlbuild")
+    (synopsis "OCaml build tool")
+    (description "OCamlbuild is a generic build tool, that has built-in rules
+for building OCaml library and programs.")
+    (license license:lgpl2.1+)))
 
 (define-public opam
   (package
@@ -444,26 +447,26 @@ Git-friendly development workflow.")
        ;; which  fails on the second attempt.
        #:parallel-build? #f
        #:make-flags '("all")
-       #:phases (modify-phases %standard-phases
-                  (replace
-                   'configure
-                   (lambda* (#:key outputs #:allow-other-keys)
-                     ;; This is a home-made 'configure' script.
-                     (let ((out (assoc-ref outputs "out")))
-                       (zero? (system* "./configure"
-                                       (string-append "--libdir=" out
-                                                      "/lib/ocaml/site-lib")
-                                       (string-append "--bindir=" out "/bin")
-                                       (string-append "--pkgdir=" out
-                                                      "/lib/ocaml/site-lib"))))))
-                  (add-after 'install 'install-meta
-                    (lambda* (#:key outputs #:allow-other-keys)
-                      (let ((out (assoc-ref outputs "out")))
-                        (substitute* "camlp4/META.in"
-                          (("directory = .*")
-                            (string-append "directory = \"" out
-                                           "/lib/ocaml/site-lib/camlp4\"\n")))
-                        (zero? (system* "make" "install-META"))))))))
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key outputs #:allow-other-keys)
+             ;; This is a home-made 'configure' script.
+             (let ((out (assoc-ref outputs "out")))
+               (invoke "./configure"
+                       (string-append "--libdir=" out
+                                      "/lib/ocaml/site-lib")
+                       (string-append "--bindir=" out "/bin")
+                       (string-append "--pkgdir=" out
+                                      "/lib/ocaml/site-lib")))))
+         (add-after 'install 'install-meta
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out")))
+               (substitute* "camlp4/META.in"
+                 (("directory = .*")
+                  (string-append "directory = \"" out
+                                 "/lib/ocaml/site-lib/camlp4\"\n")))
+               (invoke "make" "install-META")))))))
     (home-page "https://github.com/ocaml/camlp4")
     (synopsis "Write parsers in OCaml")
     (description
@@ -632,144 +635,6 @@ arbitrary-precision integer and rational arithmetic that used to be part of
 the OCaml core distribution.")
     (license license:lgpl2.1+))); with linking exception
 
-(define-public coq
-  (package
-    (name "coq")
-    (version "8.8.2")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://github.com/coq/coq/archive/V"
-                                  version ".tar.gz"))
-              (file-name (string-append name "-" version ".tar.gz"))
-              (sha256
-               (base32
-                "0i2hs0i6rp27cy8zd0mx7jscqw5cx2y0diw0pxgij66s3yr47y7r"))))
-    (native-search-paths
-     (list (search-path-specification
-            (variable "COQPATH")
-            (files (list "lib/coq/user-contrib")))))
-    (build-system ocaml-build-system)
-    (inputs
-     `(("lablgtk" ,lablgtk)
-       ("python" ,python-2)
-       ("camlp5" ,camlp5)
-       ("ocaml-num" ,ocaml-num)))
-    (arguments
-     `(#:phases
-       (modify-phases %standard-phases
-         (replace 'configure
-           (lambda* (#:key outputs #:allow-other-keys)
-             (let* ((out (assoc-ref outputs "out"))
-                    (mandir (string-append out "/share/man"))
-                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
-               (invoke "./configure"
-                       "-prefix" out
-                       "-mandir" mandir
-                       "-browser" browser
-                       "-coqide" "opt"))))
-         (replace 'build
-           (lambda _
-             (invoke "make"
-                     "-j" (number->string (parallel-job-count))
-                     "world")))
-         (delete 'check)
-         (add-after 'install 'check
-           (lambda _
-             (with-directory-excursion "test-suite"
-               ;; These two tests fail.
-               ;; This one fails because the output is not formatted as expected.
-               (delete-file-recursively "coq-makefile/timing")
-               ;; This one fails because we didn't build coqtop.byte.
-               (delete-file-recursively "coq-makefile/findlib-package")
-               (invoke "make")))))))
-    (home-page "https://coq.inria.fr")
-    (synopsis "Proof assistant for higher-order logic")
-    (description
-     "Coq is a proof assistant for higher-order logic, which allows the
-development of computer programs consistent with their formal specification.
-It is developed using Objective Caml and Camlp5.")
-    ;; The code is distributed under lgpl2.1.
-    ;; Some of the documentation is distributed under opl1.0+.
-    (license (list license:lgpl2.1 license:opl1.0+))))
-
-(define-public proof-general
-  (package
-    (name "proof-general")
-    (version "4.2")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append
-                    "http://proofgeneral.inf.ed.ac.uk/releases/"
-                    "ProofGeneral-" version ".tgz"))
-              (sha256
-               (base32
-                "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm"))))
-    (build-system gnu-build-system)
-    (native-inputs
-     `(("which" ,which)
-       ("emacs" ,emacs-minimal)
-       ("texinfo" ,texinfo)))
-    (inputs
-     `(("host-emacs" ,emacs)
-       ("perl" ,perl)
-       ("coq" ,coq)))
-    (arguments
-     `(#:tests? #f  ; no check target
-       #:make-flags (list (string-append "PREFIX=" %output)
-                          (string-append "DEST_PREFIX=" %output))
-       #:modules ((guix build gnu-build-system)
-                  (guix build utils)
-                  (guix build emacs-utils))
-       #:imported-modules (,@%gnu-build-system-modules
-                           (guix build emacs-utils))
-       #:phases
-       (modify-phases %standard-phases
-         (delete 'configure)
-         (add-after 'unpack 'disable-byte-compile-error-on-warn
-                    (lambda _
-                      (substitute* "Makefile"
-                        (("\\(setq byte-compile-error-on-warn t\\)")
-                         "(setq byte-compile-error-on-warn nil)"))
-                      #t))
-         (add-after 'unpack 'patch-hardcoded-paths
-                    (lambda* (#:key inputs outputs #:allow-other-keys)
-                      (let ((out   (assoc-ref outputs "out"))
-                            (coq   (assoc-ref inputs "coq"))
-                            (emacs (assoc-ref inputs "host-emacs")))
-                        (define (coq-prog name)
-                          (string-append coq "/bin/" name))
-                        (emacs-substitute-variables "coq/coq.el"
-                          ("coq-prog-name"           (coq-prog "coqtop"))
-                          ("coq-compiler"            (coq-prog "coqc"))
-                          ("coq-dependency-analyzer" (coq-prog "coqdep")))
-                        (substitute* "Makefile"
-                          (("/sbin/install-info") "install-info"))
-                        (substitute* "bin/proofgeneral"
-                          (("^PGHOMEDEFAULT=.*" all)
-                           (string-append all
-                                          "PGHOME=$PGHOMEDEFAULT\n"
-                                          "EMACS=" emacs "/bin/emacs")))
-                        #t)))
-         (add-after 'unpack 'clean
-                    (lambda _
-                      ;; Delete the pre-compiled elc files for Emacs 23.
-                      (zero? (system* "make" "clean"))))
-         (add-after 'install 'install-doc
-                    (lambda* (#:key make-flags #:allow-other-keys)
-                      ;; XXX FIXME avoid building/installing pdf files,
-                      ;; due to unresolved errors building them.
-                      (substitute* "Makefile"
-                        ((" [^ ]*\\.pdf") ""))
-                      (zero? (apply system* "make" "install-doc"
-                                    make-flags)))))))
-    (home-page "http://proofgeneral.inf.ed.ac.uk/")
-    (synopsis "Generic front-end for proof assistants based on Emacs")
-    (description
-     "Proof General is a major mode to turn Emacs into an interactive proof
-assistant to write formal mathematical proofs using a variety of theorem
-provers.")
-    (license license:gpl2+)))
-
 (define-public emacs-tuareg
   (package
     (name "emacs-tuareg")
@@ -1284,8 +1149,7 @@ files in these formats.")
        #:phases
        (modify-phases %standard-phases
          (replace 'configure
-           (lambda* (#:key #:allow-other-keys)
-             (zero? (system* "./configure")))))))
+           (lambda _ (invoke "./configure"))))))
     (home-page "https://forge.ocamlcore.org/projects/zarith/")
     (synopsis "Implements arbitrary-precision integers")
     (description "Implements arithmetic and logical operations over
@@ -1527,14 +1391,14 @@ coverage information.")
 (define-public dune
   (package
     (name "dune")
-    (version "1.2.1")
+    (version "1.6.3")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://github.com/ocaml/dune/releases/"
                                   "download/" version "/dune-" version ".tbz"))
               (sha256
                (base32
-                "00c5dbm4hkdapc2i7pg07b2lj8sv6ly38qr7zid58cdmbmzq21z9"))))
+                "0dmf0wbfmgdy5plz1bjiisc2hjgblvxsnrqjmw2c8y45v1h23mdz"))))
     (build-system ocaml-build-system)
     (arguments
      `(#:tests? #f; require odoc
@@ -1555,24 +1419,24 @@ following a very simple s-expression syntax.")
 (define-public ocaml-migrate-parsetree
   (package
     (name "ocaml-migrate-parsetree")
-    (version "1.1.0")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://github.com/ocaml-ppx/"
-                                  "ocaml-migrate-parsetree/releases/download/v"
-                                  version "/ocaml-migrate-parsetree-"
-                                  version ".tbz"))
-              (sha256
-               (base32
-                "01zjp1q4hryqaxv4apkjd868fycz2kf887r6lkb6x2a545h1lh7f"))))
+    (version "1.2.0")
+    (home-page "https://github.com/ocaml-ppx/ocaml-migrate-parsetree")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (sha256
+        (base32
+         "16kas19iwm4afijv3yxd250s08absabmdcb4yj57wc8r4fmzv5dm"))))
     (build-system dune-build-system)
     (arguments
-     `(#:tests? #f
-       #:jbuild? #t))
+     `(#:tests? #f))
     (propagated-inputs
-     `(("ocamlbuild" ,ocamlbuild)
+     `(("ocaml-ppx-derivers" ,ocaml-ppx-derivers)
+       ("ocamlbuild" ,ocamlbuild)
        ("ocaml-result" ,ocaml-result)))
-    (home-page "https://github.com/ocaml-ppx/ocaml-migrate-parsetree")
     (synopsis "OCaml parsetree convertor")
     (description "This library converts between parsetrees of different OCaml
 versions.  For each version, there is a snapshot of the parsetree and conversion
@@ -1901,15 +1765,17 @@ spans without being subject to operating system calendar time adjustments.")
 (define-public ocaml-cmdliner
   (package
     (name "ocaml-cmdliner")
-    (version "0.9.8")
+    (version "1.0.2")
     (source (origin
               (method url-fetch)
               (uri (string-append "http://erratique.ch/software/cmdliner/releases/"
                                   "cmdliner-" version ".tbz"))
               (sha256
                (base32
-                "0hdxlkgiwjml9dpaa80282a8350if7mc1m6yz2mrd7gci3fszykx"))))
+                "18jqphjiifljlh9jg8zpl6310p3iwyaqphdkmf89acyaix0s4kj1"))))
     (build-system ocaml-build-system)
+    (inputs
+     `(("ocaml-result" ,ocaml-result)))
     (native-inputs
      `(("ocamlbuild" ,ocamlbuild)
        ("opam" ,opam)))
@@ -1918,6 +1784,12 @@ spans without being subject to operating system calendar time adjustments.")
        #:build-flags '("native=true" "native-dynlink=true")
        #:phases
        (modify-phases %standard-phases
+         (replace 'install
+           ;; The makefile says 'adjust on cli invocation'
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out")))
+               (invoke "make" "install" (string-append "PREFIX=" out))
+               #t)))
          (delete 'configure))))
     (home-page "http://erratique.ch/software/cmdliner")
     (synopsis "Declarative definition of command line interfaces for OCaml")
@@ -1935,14 +1807,14 @@ most of the POSIX and GNU conventions.")
 (define-public ocaml-fmt
   (package
     (name "ocaml-fmt")
-    (version "0.8.0")
+    (version "0.8.5")
     (source
       (origin
         (method url-fetch)
         (uri (string-append "http://erratique.ch/software/fmt/releases/fmt-"
                             version ".tbz"))
         (sha256 (base32
-                  "16y7ibndnairb53j8a6qgipyqwjxncn4pl9jiw5bxjfjm59108px"))))
+                  "1zj9azcxcn6skmb69ykgmi9z8c50yskwg03wqgh87lypgjdcz060"))))
     (build-system ocaml-build-system)
     (native-inputs
      `(("ocamlbuild" ,ocamlbuild)
@@ -1950,6 +1822,7 @@ most of the POSIX and GNU conventions.")
        ("topkg" ,ocaml-topkg)))
     (propagated-inputs
      `(("result" ,ocaml-result)
+       ("ocaml-uchar" ,ocaml-uchar)
        ("cmdliner" ,ocaml-cmdliner)))
     (arguments `(#:tests? #f
                  #:build-flags (list "build" "--with-base-unix" "true"
@@ -2402,14 +2275,14 @@ representation of the data.")
 (define-public ocaml-uchar
   (package
     (name "ocaml-uchar")
-    (version "0.0.1")
+    (version "0.0.2")
     (source
       (origin
         (method url-fetch)
         (uri (string-append "https://github.com/ocaml/uchar/releases/download/v"
                             version "/uchar-" version ".tbz"))
         (sha256 (base32
-                  "0ficw1x7ymbd6m8hqw3w1aycwm1hbwd6bad3c5pspwnzh3qlikhi"))))
+                  "1w2saw7zanf9m9ffvz2lvcxvlm118pws2x1wym526xmydhqpyfa7"))))
     (build-system ocaml-build-system)
     (arguments
      `(#:tests? #f
@@ -4272,6 +4145,7 @@ and 4 (random based) according to RFC 4122.")
              (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
                                                    "/bin/sh")))))))
     (inputs `(("lablgtk" ,lablgtk)))
+    (properties `((upstream-name . "ocamlgraph")))
     (home-page "http://ocamlgraph.lri.fr/")
     (synopsis "Graph library for OCaml")
     (description "OCamlgraph is a generic graph library for OCaml.")
@@ -4474,13 +4348,12 @@ is provide a description of your project and Jbuilder will do the rest.")
        (modify-phases %standard-phases
          (delete 'configure)
          (replace 'build
-           (lambda* (#:key #:allow-other-keys)
-             (zero? (system* "jbuilder" "build"))))
+           (lambda _ (invoke "jbuilder" "build")))
          (delete 'check)
          (replace 'install
            (lambda* (#:key outputs #:allow-other-keys)
              (let ((out (assoc-ref outputs "out")))
-               (zero? (system* "jbuilder" "install" "--prefix" out))))))))
+               (invoke "jbuilder" "install" "--prefix" out)))))))
     (native-inputs
      `(("jbuilder" ,ocaml-jbuilder)))
     (propagated-inputs
@@ -4552,9 +4425,9 @@ instead of bindings to a C library.")
              (let* ((out (assoc-ref outputs "out"))
                     (libdir (string-append out "/lib/ocaml/site-lib")))
                (mkdir-p libdir)
-               (zero? (system* "jbuilder" "install"
-                               "--prefix" out
-                               "--libdir" libdir))))))))
+               (invoke "jbuilder" "install"
+                       "--prefix" out
+                       "--libdir" libdir)))))))
     (native-inputs
      `(("ocaml" ,ocaml)
        ("cppo" ,ocaml-cppo)
@@ -4711,281 +4584,626 @@ OCaml projects that contain C stubs.")
 cross-platform SDL C library.")
     (license license:isc)))
 
-(define-public coq-flocq
+(define-public dedukti
   (package
-    (name "coq-flocq")
-    (version "2.6.1")
-    (source (origin
-              (method url-fetch)
-              ;; Use the ‘Latest version’ link for a stable URI across releases.
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "file/37454/flocq-" version ".tar.gz"))
-              (sha256
-               (base32
-                "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin"))))
-    (build-system gnu-build-system)
+    (name "dedukti")
+    (version "2.6.0")
+    (home-page "https://deducteam.github.io/")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/deducteam/dedukti.git")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "0frl3diff033i4fmq304b8wbsdnc9mvlhmwd7a3zd699ng2lzbxb"))))
+    (inputs
+     `(("menhir" ,ocaml-menhir)))
     (native-inputs
-     `(("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
+     `(("ocamlbuild" ,ocamlbuild)))
+    (build-system ocaml-build-system)
     (arguments
-     `(#:configure-flags
-       (list (string-append "--libdir=" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib/Flocq"))
-       #:phases
+     `(#:phases
        (modify-phases %standard-phases
-         (add-before 'configure 'fix-remake
-           (lambda _
-             (substitute* "remake.cpp"
-               (("/bin/sh") (which "sh")))
-             #t))
+         (delete 'configure)
          (replace 'build
            (lambda _
-             (invoke "./remake")
+             (invoke "make")
              #t))
          (replace 'check
            (lambda _
-             (invoke "./remake" "check")
+             (invoke "make" "tests")
+             #t))
+         (add-before 'install 'set-binpath
+           ;; Change binary path in the makefile
+           (lambda _
+             (let ((out (assoc-ref %outputs "out")))
+               (substitute* "GNUmakefile"
+                 (("BINDIR = (.*)$")
+                  (string-append "BINDIR = " out "/bin"))))
              #t))
-             ;; TODO: requires coq-gappa and coq-interval.
-             ;(invoke "./remake" "check-more")
          (replace 'install
            (lambda _
-             (invoke "./remake" "install")
+             (invoke "make" "install")
              #t)))))
-    (home-page "http://flocq.gforge.inria.fr/")
-    (synopsis "Floating-point formalization for the Coq system")
-    (description "Flocq (Floats for Coq) is a floating-point formalization for
-the Coq system.  It provides a comprehensive library of theorems on a multi-radix
-multi-precision arithmetic.  It also supports efficient numerical computations
-inside Coq.")
-    (license license:lgpl3+)))
+    (synopsis "Proof-checker for the λΠ-calculus modulo theory, an extension of
+the λ-calculus")
+    (description "Dedukti is a proof-checker for the λΠ-calculus modulo
+theory.  The λΠ-calculus is an extension of the simply typed λ-calculus with
+dependent types.  The λΠ-calculus modulo theory is itself an extension of the
+λΠ-calculus where the context contains variable declaration as well as rewrite
+rules.  This system is not designed to develop proofs, but to check proofs
+developed in other systems.  In particular, it enjoys a minimalistic syntax.")
+    (license license:cecill-c)))
 
-(define-public coq-gappa
-  (package
-    (name "coq-gappa")
-    (version "1.3.2")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36397/gappa-"
-                                  version ".tar.gz"))
-              (sha256
-               (base32
-                "19kg2zldaqs4smy7bv9hp650sqg46xbx1ss7jnyagpxdscwn9apd"))))
-    (build-system gnu-build-system)
-    (native-inputs
-     `(("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)
-       ("bison" ,bison)
-       ("flex" ,flex)))
+(define-public emacs-dedukti-mode
+  (let ((commit "d7c3505a1046187de3c3aeb144455078d514594e"))
+    (package
+      (name "emacs-dedukti-mode")
+      (version (git-version "0" "0" commit))
+      (home-page "https://github.com/rafoo/dedukti-mode")
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url home-page)
+                      (commit commit)))
+                (sha256
+                 (base32
+                  "1842wikq24c8rg0ac84vb1qby9ng1nssxswyyni4kq85lng5lcrp"))
+                (file-name (git-file-name name version))))
+      (inputs
+       `(("dedukti" ,dedukti)))
+      (build-system emacs-build-system)
+      (arguments
+       '(#:phases
+         (modify-phases %standard-phases
+           (add-before 'install 'patch-dkpath
+             (lambda _
+               (let ((dkcheck-path (which "dkcheck")))
+                 (substitute* "dedukti-mode.el"
+                   (("dedukti-path \"(.*)\"")
+                    (string-append "dedukti-path \"" dkcheck-path "\"")))))))))
+      (synopsis "Emacs major mode for Dedukti files")
+      (description "This package provides an Emacs major mode for editing
+Dedukti files.")
+      (license license:cecill-b))))
+
+(define-public emacs-flycheck-dedukti
+  (let ((commit "3dbff5646355f39d57a3ec514f560a6b0082a1cd"))
+    (package
+      (name "emacs-flycheck-dedukti")
+      (version (git-version "0" "0" commit))
+      (home-page "https://github.com/rafoo/flycheck-dedukti")
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url home-page)
+                      (commit commit)))
+                (sha256
+                 (base32
+                  "1ffpxnwl3wx244n44mbw81g00nhnykd0lnid29f4aw1av7w6nw8l"))
+                (file-name (git-file-name name version))))
+      (build-system emacs-build-system)
+      (inputs
+       `(("dedukti-mode" ,emacs-dedukti-mode)
+         ("flycheck-mode" ,emacs-flycheck)))
+      (synopsis "Flycheck integration for the dedukti language")
+      (description "This package provides a frontend for Flycheck to perform
+syntax checking on dedukti files.")
+      (license license:cecill-b))))
+
+(define-public ocaml-ppx-inline-test
+  (package
+    (name "ocaml-ppx-inline-test")
+    (version "0.11.0")
+    (home-page "https://github.com/janestreet/ppx_inline_test")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "11n94fz1asjf5vqdgriv0pvsa5lbfpqcyk525c7816w23vskcvq6"))))
+    (build-system dune-build-system)
+    (arguments
+     ;see home page README for further information
+     `(#:tests? #f))
     (inputs
-     `(("gmp" ,gmp)
-       ("mpfr" ,mpfr)
-       ("boost" ,boost)))
+     `(("ocaml-base" ,ocaml-base)
+       ("ocaml-migrate-parsetree" ,ocaml-migrate-parsetree)
+       ("ocaml-compiler-libs" ,ocaml-compiler-libs)
+       ("ocaml-sexplib0" ,ocaml-sexplib0)
+       ("ocaml-stdio" ,ocaml-stdio)
+       ("ocaml-ppxlib" ,ocaml-ppxlib)))
+    (synopsis "Syntax extension for writing in-line tests in ocaml code")
+    (description "This package contains a syntax extension for writing
+in-line tests in ocaml code.  It is part of Jane Street's PPX rewriters
+collection.")
+    (license license:expat)))
+
+(define-public ocaml-biniou
+ (package
+   (name "ocaml-biniou")
+   (version "1.2.0")
+   (home-page "https://github.com/mjambon/biniou")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "0mjpgwyfq2b2izjw0flmlpvdjgqpq8shs89hxj1np2r50csr8dcb"))))
+   (build-system dune-build-system)
+   (inputs
+    `(("ocaml-easy-format" ,ocaml-easy-format)))
+   (native-inputs
+    `(("which" ,which)))
+   (synopsis "Data format designed for speed, safety, ease of use and backward
+compatibility")
+   (description "Biniou (pronounced \"be new\" is a binary data format
+designed for speed, safety, ease of use and backward compatibility as
+protocols evolve.  Biniou is vastly equivalent to JSON in terms of
+functionality but allows implementations several times faster (4 times faster
+than yojson), with 25-35% space savings.")
+   (license license:bsd-3)))
+
+(define-public ocaml-yojson
+  (package
+    (name "ocaml-yojson")
+    (version "1.4.1")
+    (home-page "https://github.com/ocaml-community/yojson")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "0nwsfkmqpyfab4rxq76q8ff7giyanghw08094jyrp275v99zdjr9"))))
+    (build-system dune-build-system)
     (arguments
-     `(#:configure-flags
-       (list (string-append "--libdir=" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib/Gappa"))
-       #:phases
-       (modify-phases %standard-phases
-         (add-before 'configure 'fix-remake
-           (lambda _
-             (substitute* "remake.cpp"
-               (("/bin/sh") (which "sh")))))
-         (replace 'build
-           (lambda _
-             (zero? (system* "./remake"))))
-         (replace 'check
-           (lambda _
-             (zero? (system* "./remake" "check"))))
-         (replace 'install
-           (lambda _
-             (zero? (system* "./remake" "install")))))))
-    (home-page "http://gappa.gforge.inria.fr/")
-    (synopsis "Verify and formally prove properties on numerical programs")
-    (description "Gappa is a tool intended to help verifying and formally proving
-properties on numerical programs dealing with floating-point or fixed-point
-arithmetic.  It has been used to write robust floating-point filters for CGAL
-and it is used to certify elementary functions in CRlibm.  While Gappa is
-intended to be used directly, it can also act as a backend prover for the Why3
-software verification plateform or as an automatic tactic for the Coq proof
-assistant.")
-    (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
-
-(define-public coq-mathcomp
-  (package
-    (name "coq-mathcomp")
-    (version "1.7.0")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
-                                  version ".tar.gz"))
-              (sha256
-               (base32
-                "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39"))))
-    (build-system gnu-build-system)
+     `(#:test-target "."))
+    (inputs
+     `(("ocaml-biniou" ,ocaml-biniou)
+       ("ocaml-easy-format" ,ocaml-easy-format)))
     (native-inputs
-     `(("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
+     `(("ocaml-cppo" ,ocaml-cppo)))
+    (synopsis "Low-level JSON library for OCaml")
+    (description "Yojson is an optimized parsing and printing library for the
+JSON format.  It addresses a few shortcomings of json-wheel including 2x
+speedup, polymorphic variants and optional syntax for tuples and variants.
+@code{ydump} is a pretty printing command-line program provided with the
+yojson package.  The program @code{atdgen} can be used to derive OCaml-JSON
+serializers and deserializers from type definitions.")
+    (license license:bsd-3)))
+ 
+(define-public ocaml-craml
+  (package
+    (name "ocaml-craml")
+    (version "1.0.0")
+    (home-page "https://github.com/realworldocaml/craml")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit version)))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "197xjp4vmzdymf2ndinw271ihpf45h04mx8gqj8ypspxdr5fj1a5"))))
+    (build-system dune-build-system)
+    (inputs
+     `(("ocaml-fmt" ,ocaml-fmt)
+       ("ocaml-astring" ,ocaml-astring)
+       ("ocaml-logs" ,ocaml-logs)
+       ("ocaml-cmdliner" ,ocaml-cmdliner)))
+    (synopsis
+     "CRAM-testing framework for testing command line applications")
+    (description "CRAM is a is functional testing framework for command line
+applications.  @code{craml} is freely inspired by the
+Mercurial's @code{https://www.selenic.com/blog/?p=663, unified test
+format}.  @code{craml} is released as a single binary (called @code{craml}).")
+    (license license:isc)))
+
+(define-public ocaml-merlin
+  (package
+    (name "ocaml-merlin")
+    (version "3.2.2")
+    (home-page "https://ocaml.github.io/merlin/")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/ocaml/merlin.git")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "15ssgmwdxylbwhld9p1cq8x6kadxyhll5bfyf11dddj6cldna3hb"))))
+    (build-system dune-build-system)
+    (inputs
+     `(("ocaml-biniou" ,ocaml-biniou)
+       ("ocaml-yojson" ,ocaml-yojson)
+       ("ocaml-easy-format" ,ocaml-easy-format)))
+    (native-inputs
+     `(("ocaml-findlib" ,ocaml-findlib)))
     (arguments
-     `(#:tests? #f; No need to test formally-verified programs :)
-       #:phases
-       (modify-phases %standard-phases
-         (delete 'configure)
-         (add-before 'build 'chdir
-           (lambda _
-             (chdir "mathcomp")))
-         (replace 'install
-           (lambda* (#:key outputs #:allow-other-keys)
-             (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
-             (zero? (system* "make" "-f" "Makefile.coq"
-                             (string-append "COQLIB=" (assoc-ref outputs "out")
-                                            "/lib/coq/")
-                             "install")))))))
-    (home-page "https://math-comp.github.io/math-comp/")
-    (synopsis "Mathematical Components for Coq")
-    (description "Mathematical Components for Coq has its origins in the formal
-proof of the Four Colour Theorem.  Since then it has grown to cover many areas
-of mathematics and has been used for large scale projects like the formal proof
-of the Odd Order Theorem.
-
-The library is written using the Ssreflect proof language that is an integral
-part of the distribution.")
-    (license license:cecill-b)))
-
-(define-public coq-coquelicot
-  (package
-    (name "coq-coquelicot")
-    (version "3.0.1")
+     '(#:tests? #f)) ;; Errors in tests in version 3.2.2
+    (synopsis "Context sensitive completion for OCaml in Vim and Emacs")
+    (description "Merlin is an editor service that provides modern IDE
+features for OCaml.  Emacs and Vim support is provided out-of-the-box.
+External contributors added support for Visual Studio Code, Sublime Text and
+Atom.")
+    (license license:expat)))
+
+(define-public ocaml-gsl
+  (package
+    (name "ocaml-gsl")
+    (version "1.22.0")
+    (source
+     (origin
+       (method url-fetch)
+       (uri
+        (string-append
+         "https://github.com/mmottl/gsl-ocaml/releases/download/"
+         version "/gsl-" version ".tbz"))
+       (sha256
+        (base32
+         "17vcswipliq1b2idbzx1z95kskn1a4q4s5v04igilg0f7lnkaarb"))))
+    (build-system ocaml-build-system)
+    (inputs
+     `(("gsl" ,gsl)))
+    (home-page "https://mmottl.github.io/gsl-ocaml")
+    (synopsis "Bindings to the GNU Scientific Library")
+    (description
+     "GSL-OCaml is an interface to the @dfn{GNU scientific library} (GSL) for
+the OCaml language.")
+    (license license:gpl3+)))
+
+(define-public ocaml4.01-gsl
+  (package-with-ocaml4.01 ocaml-gsl))
+
+(define-public cubicle
+  (package
+    (name "cubicle")
+    (version "1.1.2")
     (source (origin
               (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "file/37045/coquelicot-" version ".tar.gz"))
+              (uri (string-append "http://cubicle.lri.fr/cubicle-"
+                                  version ".tar.gz"))
               (sha256
                (base32
-                "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r"))))
+                "10kk80jdmpdvql88sdjsh7vqzlpaphd8vip2lp47aarxjkwjlz1q"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
+     `(("automake" ,automake)
+       ("ocaml" ,ocaml)
+       ("which" ,(@@ (gnu packages base) which))))
     (propagated-inputs
-     `(("mathcomp" ,coq-mathcomp)))
+     `(("ocaml-num" ,ocaml-num)
+       ("z3" ,z3)))
     (arguments
-     `(#:configure-flags
-       (list (string-append "--libdir=" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib/Coquelicot"))
+     `(#:configure-flags (list "--with-z3")
+       #:make-flags (list "QUIET=")
+       #:tests? #f
        #:phases
        (modify-phases %standard-phases
-         (add-before 'configure 'fix-coq8.8
+         (add-before 'configure 'configure-for-release
            (lambda _
-             ; appcontext has been removed from coq 8.8
-             (substitute* "theories/AutoDerive.v"
-               (("appcontext") "context"))
+             (substitute* "Makefile.in"
+               (("SVNREV=") "#SVNREV="))
              #t))
-         (add-before 'configure 'fix-remake
-           (lambda _
-             (substitute* "remake.cpp"
-               (("/bin/sh") (which "sh")))))
-         (replace 'build
-           (lambda _
-             (zero? (system* "./remake"))))
-         (replace 'check
+         (add-before 'configure 'fix-/bin/sh
            (lambda _
-             (zero? (system* "./remake" "check"))))
-         (replace 'install
+             (substitute* "configure"
+               (("-/bin/sh") (string-append "-" (which "sh"))))
+             #t))
+         (add-before 'configure 'fix-smt-z3wrapper.ml
            (lambda _
-             (zero? (system* "./remake" "install")))))))
-    (home-page "http://coquelicot.saclay.inria.fr/index.html")
-    (synopsis "Coq library for Reals")
-    (description "Coquelicot is an easier way of writing formulas and theorem
-statements, achieved by relying on total functions in place of dependent types
-for limits, derivatives, integrals, power series, and so on.  To help with the
-proof process, the library comes with a comprehensive set of theorems that cover
-not only these notions, but also some extensions such as parametric integrals,
-two-dimensional differentiability, asymptotic behaviors.  It also offers some
-automations for performing differentiability proofs.  Moreover, Coquelicot is a
-conservative extension of Coq's standard library and provides correspondence
-theorems between the two libraries.")
-    (license license:lgpl3+)))
+             (substitute* "Makefile.in"
+               (("\\\\n") ""))
+             #t))
+         (add-before 'configure 'fix-ocaml-num
+           (lambda* (#:key inputs #:allow-other-keys)
+             (substitute* "Makefile.in"
+               (("= \\$\\(FUNCTORYLIB\\)")
+                (string-append "= -I "
+                               (assoc-ref inputs "ocaml-num")
+                               "/lib/ocaml/site-lib"
+                               " $(FUNCTORYLIB)")))
+             #t)))))
+    (home-page "http://cubicle.lri.fr/")
+    (synopsis "Model checker for array-based systems")
+    (description "Cubicle is a model checker for verifying safety properties
+of array-based systems.  This is a syntactically restricted class of
+parametrized transition systems with states represented as arrays indexed by
+an arbitrary number of processes.  Cache coherence protocols and mutual
+exclusion algorithms are typical examples of such systems.")
+    (license license:asl2.0)))
 
-(define-public coq-bignums
+(define-public ocaml-sexplib0
   (package
-    (name "coq-bignums")
-    (version "8.8.0")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://github.com/coq/bignums/archive/V"
-                                  version ".tar.gz"))
-              (file-name (string-append name "-" version ".tar.gz"))
-              (sha256
-               (base32
-                "08m1cmq4hkaf4sb0vy978c11rgzvds71cphyadmr2iirpr5815r0"))))
-    (build-system gnu-build-system)
-    (native-inputs
-     `(("ocaml" ,ocaml)
-       ("coq" ,coq)))
+    (name "ocaml-sexplib0")
+    (version "0.11.0")
+    (home-page "https://github.com/janestreet/sexplib0")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "07v3ggyss7xhfv14bjk1n87sr42iqwj4cgjiv2lcdfkqk49i2bmi"))))
+    (build-system dune-build-system)
+    (arguments
+     '(#:tests? #f)) ;no tests
+    (synopsis "Library containing the definition of S-expressions and some
+base converters")
+    (description "Part of Jane Street's Core library The Core suite of
+libraries is an industrial strength alternative to OCaml's standard library
+that was developed by Jane Street, the largest industrial user of OCaml.")
+(license license:expat)))
+
+(define-public ocaml-parsexp
+  (package
+    (name "ocaml-parsexp")
+    (version "0.11.0")
+    (home-page "https://github.com/janestreet/parsexp")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "1nyq23s5igd8cf3n4qxprjvhbmb6ighb3fy5mw7hxl0mdgsw5fvz"))))
+    (build-system dune-build-system)
+    (inputs
+     `(("ocaml-sexplib0" ,ocaml-sexplib0)))
+    (synopsis "S-expression parsing library")
+    (description
+     "This library provides generic parsers for parsing S-expressions from
+strings or other medium.
+
+The library is focused on performances but still provide full generic
+parsers that can be used with strings, bigstrings, lexing buffers,
+character streams or any other sources effortlessly.
+
+It provides three different class of parsers:
+@itemize
+@item
+the normal parsers, producing [Sexp.t] or [Sexp.t list] values
+@item
+the parsers with positions, building compact position sequences so
+that one can recover original positions in order to report properly
+located errors at little cost
+@item
+the Concrete Syntax Tree parsers, produce values of type
+@code{Parsexp.Cst.t} which record the concrete layout of the s-expression
+syntax, including comments
+@end itemize
+
+This library is portable and doesn't provide IO functions.  To read
+s-expressions from files or other external sources, you should use
+parsexp_io.")
+    (license license:expat)))
+
+(define-public ocaml-sexplib
+  (package
+    (name "ocaml-sexplib")
+    (version "0.11.0")
+    (home-page "https://github.com/janestreet/sexplib")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "1qfl0m04rpcjvc4yw1hzh6r16jpwmap0sa9ax6zjji67dz4szpyb"))))
+    (build-system dune-build-system)
+    (inputs
+     `(("ocaml-num" ,ocaml-num)
+       ("ocaml-parsexp" ,ocaml-parsexp)
+       ("ocaml-sexplib0" ,ocaml-sexplib0)))
+    (synopsis
+     "Library for serializing OCaml values to and from S-expressions")
+    (description
+     "This package is part of Jane Street's Core library. Sexplib contains
+functionality for parsing and pretty-printing s-expressions.")
+    (license license:expat)))
+
+(define-public ocaml-base
+  (package
+    (name "ocaml-base")
+    (version "0.11.1")
+    (home-page "https://github.com/janestreet/base")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "0j6xb4265jr41vw4fjzak6yr8s30qrnzapnc6rl1dxy8bjai0nir"))))
+    (build-system dune-build-system)
     (inputs
-     `(("camlp5" ,camlp5)))
+     `(("ocaml-sexplib0" ,ocaml-sexplib0)))
     (arguments
-     `(#:tests? #f; No test target
-       #:make-flags
-       (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib"))
-       #:phases
+     `(#:phases
        (modify-phases %standard-phases
-         (delete 'configure))))
-    (home-page "https://github.com/coq/bignums")
-    (synopsis "Coq library for arbitrary large numbers")
-    (description "Bignums is a coq library of arbitrary large numbers.  It
-provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
-    (license license:lgpl2.1+)))
+         (replace 'build
+           ;; make warnings non fatal (jbuilder behaviour)
+           (lambda _
+             (invoke "dune" "build" "@install" "--profile=release"))))))
+  (synopsis
+    "Full standard library replacement for OCaml")
+  (description
+    "Base is a complete and portable alternative to the OCaml standard
+library.  It provides all standard functionalities one would expect
+from a language standard library.  It uses consistent conventions
+across all of its module.
+
+Base aims to be usable in any context.  As a result system dependent
+features such as I/O are not offered by Base.  They are instead
+provided by companion libraries such as
+@url{https://github.com/janestreet/stdio, ocaml-stdio}.")
+  (license license:expat)))
+
+(define-public ocaml-compiler-libs
+  (package
+    (name "ocaml-compiler-libs")
+    (version "0.11.0")
+    (home-page "https://github.com/janestreet/ocaml-compiler-libs")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "03jds7bszh8wwpfwxb3dg0gyr1j1872wxwx1xqhry5ir0i84bg0s"))))
+    (build-system dune-build-system)
+    (arguments
+     '(#:tests? #f)) ;no tests
+    (synopsis "Compiler libraries repackaged")
+    (description "This packaeg simply repackages the OCaml compiler libraries
+so they don't expose everything at toplevel.  For instance, @code{Ast_helper}
+is now @code{Ocaml_common.Ast_helper}.")
+    (license license:expat)))
 
-(define-public coq-interval
+(define-public ocaml-stdio
   (package
-    (name "coq-interval")
-    (version "3.3.0")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "file/37077/interval-" version ".tar.gz"))
-              (sha256
-               (base32
-                "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903"))))
-    (build-system gnu-build-system)
+    (name "ocaml-stdio")
+    (version "0.11.0")
+    (home-page "https://github.com/janestreet/stdio")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "1facajqhvq34g2wrg368y0ajxd6lrj5b3lyzyj0jhdmraxajjcwn"))))
+    (build-system dune-build-system)
+    (inputs `(("ocaml-base" ,ocaml-base)
+              ("ocaml-sexplib0" ,ocaml-sexplib0)))
+    (arguments
+     '(#:tests? #f)) ;no tests
+    (synopsis "Standard IO library for OCaml")
+    (description
+     "Stdio implements simple input/output functionalities for OCaml.  It
+re-exports the input/output functions of the OCaml standard libraries using
+a more consistent API.")
+    (license license:expat)))
+
+(define-public ocaml-ppx-derivers
+  (package
+    (name "ocaml-ppx-derivers")
+    (version "1.2")
+    (home-page
+     "https://github.com/ocaml-ppx/ppx_derivers")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit version)))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "0bnhihl1w31as5w2czly1v3d6pbir9inmgsjg2cj6aaj9v1dzd85"))))
+    (build-system dune-build-system)
+    (arguments
+     '(#:tests? #f)) ;no tests
+    (synopsis "Shared @code{@@deriving} plugin registry")
+    (description
+     "Ppx_derivers is a tiny package whose sole purpose is to allow
+ppx_deriving and ppx_type_conv to inter-operate gracefully when linked
+as part of the same ocaml-migrate-parsetree driver.")
+    (license license:bsd-3)))
+
+(define-public ocaml-ppxlib
+  (package
+    (name "ocaml-ppxlib")
+    (version "0.4.0")
+    (home-page "https://github.com/ocaml-ppx/ppxlib")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url (string-append home-page ".git"))
+             (commit version)))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "1nr4igf5m4prvigvv470dnhfdhdw0p6hz6zw8gnm5bzcv7s2lg5l"))))
+    (build-system dune-build-system)
+    (inputs
+     `(("ocaml-base" ,ocaml-base)
+       ("ocaml-compiler-libs" ,ocaml-compiler-libs)
+       ("ocaml-migrate-parsetree" ,ocaml-migrate-parsetree)
+       ("ocaml-ppx-derivers" ,ocaml-ppx-derivers)
+       ("ocaml-stdio" ,ocaml-stdio)
+       ("ocaml-result" ,ocaml-result)
+       ("ocaml-sexplib0" ,ocaml-sexplib0)))
     (native-inputs
-     `(("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
-    (propagated-inputs
-     `(("flocq" ,coq-flocq)
-       ("bignums" ,coq-bignums)
-       ("coquelicot" ,coq-coquelicot)
-       ("mathcomp" ,coq-mathcomp)))
+     `(("ocaml-findlib" ,ocaml-findlib)))
     (arguments
-     `(#:configure-flags
-       (list (string-append "--libdir=" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib/Gappa"))
-       #:phases
+     '(#:phases
        (modify-phases %standard-phases
-         (add-before 'configure 'fix-remake
-           (lambda _
-             (substitute* "remake.cpp"
-               (("/bin/sh") (which "sh")))))
-         (replace 'build
-           (lambda _
-             (zero? (system* "./remake"))))
-         (replace 'check
-           (lambda _
-             (zero? (system* "./remake" "check"))))
-         (replace 'install
-           (lambda _
-             (zero? (system* "./remake" "install")))))))
-    (home-page "http://coq-interval.gforge.inria.fr/")
-    (synopsis "Coq tactics to simplify inequality proofs")
-    (description "Interval provides vernacular files containing tactics for
-simplifying the proofs of inequalities on expressions of real numbers for the
-Coq proof assistant.")
-    (license license:cecill-c)))
+         (add-before 'check 'set-topfind
+           (lambda* (#:key inputs #:allow-other-keys)
+             ;; add the line #directory ".." at the top of each file
+             ;; using #use "topfind";; to be able to find topfind
+             (let* ((findlib-path (assoc-ref inputs "ocaml-findlib"))
+                    (findlib-libdir
+                     (string-append findlib-path "/lib/ocaml/site-lib")))
+               (substitute* '("test/base/test.ml"
+                              "test/deriving/test.ml"
+                              "test/driver/attributes/test.ml"
+                              "test/driver/non-compressible-suffix/test.ml"
+                              "test/driver/transformations/test.ml")
+                 (("#use \"topfind\";;" all)
+                  (string-append "#directory \"" findlib-libdir "\"\n"
+                                 all))))
+             #t)))))
+    (synopsis
+     "Base library and tools for ppx rewriters")
+    (description
+     "A comprehensive toolbox for ppx development.  It features:
+@itemize
+@item an OCaml AST / parser / pretty-printer snapshot, to create a full frontend
+independent of the version of OCaml;
+@item a library for library for ppx rewriters in general, and type-driven code
+generators in particular;
+@item
+a feature-full driver for OCaml AST transformers;
+@item a quotation mechanism allowing to write values representing the
+OCaml AST in the OCaml syntax;
+@item a generator of open recursion classes from type definitions.
+@end itemize")
+    (license license:expat)))