code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2017 José Miguel Sánchez García <jmi2k@openmailbox.org>
;;; Copyright © 2018 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2019 Alexandru-Sergiu Marton <brown121407@member.fsf.org>
;;; Copyright © 2019 Brett Gilio <brettg@gnu.org>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages compton)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (guix packages)
  #:use-module (guix git-download)
  #:use-module (guix build-system gnu)
  #:use-module (guix build-system meson)
  #:use-module (gnu packages datastructures)
  #:use-module (gnu packages docbook)
  #:use-module (gnu packages documentation)
  #:use-module (gnu packages freedesktop)
  #:use-module (gnu packages gl)
  #:use-module (gnu packages glib)
  #:use-module (gnu packages libevent)
  #:use-module (gnu packages pcre)
  #:use-module (gnu packages pkg-config)
  #:use-module (gnu packages python)
  #:use-module (gnu packages textutils)
  #:use-module (gnu packages xdisorg)
  #:use-module (gnu packages xml)
  #:use-module (gnu packages xorg))

(define-public compton
  (let ((upstream-version "0.1_beta2"))
    (package
      (name "compton")
      (version (string-filter (char-set-complement (char-set #\_))
                              upstream-version))
      (source
       (origin
         (method git-fetch)
         (uri (git-reference
               (url "https://github.com/chjj/compton")
               (commit (string-append "v" upstream-version))))
         (sha256
          (base32
           "0v65viilhnd2xgvmdpzc1srxszcg8kj1vhi5gy9292j48w0s2fx1"))
         (file-name (git-file-name name version))))
      (build-system gnu-build-system)
      (inputs
       `(("dbus" ,dbus)
         ("libconfig" ,libconfig)
         ("libx11" ,libx11)
         ("libxcomposite" ,libxcomposite)
         ("libxdamage" ,libxdamage)
         ("libxext" ,libxext)
         ("libxfixes" ,libxfixes)
         ("libxinerama" ,libxinerama)
         ("libxrandr" ,libxrandr)
         ("libxrender" ,libxrender)
         ("mesa" ,mesa)
         ("xprop" ,xprop)
         ("xwininfo" ,xwininfo)))
      (native-inputs
       `(("asciidoc" ,asciidoc)
         ("libdrm" ,libdrm)
         ("pkg-config" ,pkg-config)
         ("python" ,python)
         ("xorgproto" ,xorgproto)))
      (arguments
       `(#:make-flags (list
                       "CC=gcc"
                       "NO_REGEX_PCRE=1"          ; pcre makes build fail
                       (string-append "PREFIX=" (assoc-ref %outputs "out")))
         #:tests? #f                              ; no tests
         #:phases
         (modify-phases %standard-phases
           (delete 'configure))))
      (home-page "https://github.com/chjj/compton")
      (synopsis "Compositor for X11")
      (description
       "Compton is a compositor for the Xorg display server and a for of
xcompmgr-dana, which implements some changes like:

@itemize
@item OpenGL backend (@command{--backend glx}), in addition to the old X Render
backend.
@item Inactive window transparency (@command{-i}) and dimming
(@command{--inactive-dim}).
@item Menu transparency (@command{-m}, thanks to Dana).
@item Shadows are now enabled for argb windows, e.g terminals with transparency
@item Removed serverside shadows (and simple compositing) to clean the code,
the only option that remains is clientside shadows.
@item Configuration files (see the man page for more details).
@item Colored shadows (@command{--shadow-[red/green/blue]}).
@item A new fade system.
@item VSync support (not always working).
@item Blur of background of transparent windows, window color inversion (bad in
performance).
@item Some more options...
@end itemize\n")
      (license license:expat))))

(define-public picom
  (package
    (name "picom")
    (version "8.2")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/yshui/picom")
             (commit (string-append "v" version))))
       (sha256
        (base32
         "0gjksayz2xpmgglvw17ppsan2imrd1fijs579kbf27xwp503xgfl"))
       (file-name (string-append "picom-" version))))
    (build-system meson-build-system)
    (inputs
     `(("dbus" ,dbus)
       ("libconfig" ,libconfig)
       ("libx11" ,libx11)
       ("libxext" ,libxext)
       ("libev" ,libev)
       ("mesa" ,mesa)
       ("xprop" ,xprop)
       ("xcb-util-renderutil" ,xcb-util-renderutil)
       ("xcb-util-image" ,xcb-util-image)
       ("pixman" ,pixman)
       ("uthash" ,uthash)
       ("libxdg-basedir" ,libxdg-basedir)
       ("pcre" ,pcre)))
    (native-inputs
     `(("asciidoc" ,asciidoc)
       ("pkg-config" ,pkg-config)
       ("xorgproto" ,xorgproto)))
    (arguments
     `(#:build-type "release"
       #:configure-flags '("-Dwith_docs=true")))
    (home-page "https://github.com/yshui/picom")
    (synopsis "Compositor for X11, forked from Compton")
    (description
     "Picom is a standalone compositor for Xorg, suitable for use
with window managers that do not provide compositing.

Picom is a fork of compton, which is a fork of xcompmgr-dana,
which in turn is a fork of xcompmgr.")
    (license (list license:expat      ; The original compton license.
                   license:mpl2.0)))) ; License used by new picom files.


code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2020 Oleg Pykhalov <go.wigust@gmail.com>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages configuration-management)
  #:use-module (gnu packages)
  #:use-module (guix build-system go)
  #:use-module (guix git-download)
  #:use-module (gnu packages golang)
  #:use-module (gnu packages version-control)
  #:use-module (gnu packages textutils)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (guix packages)
  #:use-module (guix utils))

(define-public chezmoi
  (package
    (name "chezmoi")
    ;; XXX: Make sure 7f238faa61e46d79b54d4d0ea8f0b5fc27db84b2 applied before
    ;; version update, which should fix @code{password-store} integration.
    (version "1.8.1")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/twpayne/chezmoi")
                    (commit (string-append "v" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "1b8y0wq3myhvjdnwl0i4x85iil7i7kmsjajvbw1a47afm83jkbaw"))))
    (build-system go-build-system)
    (arguments
     `(#:import-path "github.com/twpayne/chezmoi"
       ;; We don't need to install the source code for end-user applications.
       #:install-source? #f))
    (native-inputs
     `(("go-github-com-masterminds-sprig" ,go-github-com-masterminds-sprig)
       ("go-github-com-masterminds-goutils" ,go-github-com-masterminds-goutils)
       ("go-github-com-masterminds-semver" ,go-github-com-masterminds-semver)
       ("go-github-com-google-uuid" ,go-github-com-google-uuid)
       ("go-github-com-huandu-xstrings" ,go-github-com-huandu-xstrings)
       ("go-github-com-imdario-mergo" ,go-github-com-imdario-mergo)
       ("go-github-com-mitchellh-reflectwalk" ,go-github-com-mitchellh-reflectwalk)
       ("go-github-com-mitchellh-copystructure" ,go-github-com-mitchellh-copystructure)
       ("go-github-com-bmatcuk-doublestar" ,go-github-com-bmatcuk-doublestar)
       ("go-github-com-charmbracelet-glamour" ,go-github-com-charmbracelet-glamour)
       ("go-github-com-alecthomas-chroma" ,go-github-com-alecthomas-chroma)
       ("go-github-com-coreos-go-semver" ,go-github-com-coreos-go-semver)
       ("go-github-com-danwakefield-fnmatch" ,go-github-com-danwakefield-fnmatch)
       ("go-github-com-dlclark-regexp2" ,go-github-com-dlclark-regexp2)
       ("go-github-go-git" ,go-github-go-git)
       ("go-github-com-google-go-github" ,go-github-com-google-go-github)
       ("go-github-com-google-go-querystring" ,go-github-com-google-go-querystring)
       ("go-github-com-google-renameio" ,go-github-com-google-renameio)
       ("go-github-com-microcosm-cc-bluemonday",go-github-com-microcosm-cc-bluemonday)
       ("go-github-com-aymerick-douceur" ,go-github-com-aymerick-douceur)
       ("go-github-com-chris-ramon-douceur" ,go-github-com-chris-ramon-douceur)
       ("go-github-com-gorilla-css" ,go-github-com-gorilla-css)
       ("go-github-com-muesli-reflow-ansi" ,go-github-com-muesli-reflow-ansi)
       ("go-github-com-muesli-reflow-wordwrap" ,go-github-com-muesli-reflow-wordwrap)
       ("go-github-com-muesli-reflow-indent" ,go-github-com-muesli-reflow-indent)
       ("go-github-com-muesli-reflow-padding" ,go-github-com-muesli-reflow-padding)
       ("go-github-com-muesli-termenv" ,go-github-com-muesli-termenv)
       ("go-github-com-google-goterm" ,go-github-com-google-goterm)
       ("go-golang-org-colorful" ,go-golang-org-colorful)
       ("go-github-com-mattn-go-isatty" ,go-github-com-mattn-go-isatty)
       ("go-github.com-mattn-go-runewidth" ,go-github.com-mattn-go-runewidth)
       ("go-github-com-olekukonko-tablewriter" ,go-github-com-olekukonko-tablewriter)
       ("go-github-com-pelletier-go-toml" ,go-github-com-pelletier-go-toml)
       ("go-github-com-pkg-diff" ,go-github-com-pkg-diff)
       ("go-github-com-sergi-go-diff" ,go-github-com-sergi-go-diff)
       ("go-github-com-spf13-cobra" ,go-github-com-spf13-cobra)
       ("go-github-com-spf13-viper" ,go-github-com-spf13-viper)
       ("go-github-com-twpayne-go-shell" ,go-github-com-twpayne-go-shell)
       ("go-github-com-twpayne-go-vfs" ,go-github-com-twpayne-go-vfs)
       ("go-github-com-twpayne-go-vfsafero" ,go-github-com-twpayne-go-vfsafero)
       ("go-github-com-twpayne-go-xdg" ,go-github-com-twpayne-go-xdg)
       ("go-github-com-yuin-goldmark" ,go-github-com-yuin-goldmark)
       ("go-github-com-zalando-go-keyring" ,go-github-com-zalando-go-keyring)
       ("go-github-com-godbus-dbus" ,go-github-com-godbus-dbus)
       ("go-etcd-io-bbolt" ,go-etcd-io-bbolt)
       ("go-golang-org-x-crypto" ,go-golang-org-x-crypto)
       ("go-golang-org-x-net" ,go-golang-org-x-net)
       ("go-golang-org-x-oauth2" ,go-golang-org-x-oauth2)
       ("go-github-com-rogpeppe-go-internal" ,go-github-com-rogpeppe-go-internal)
       ("gopkg-in-errgo-fmt-errors" ,gopkg-in-errgo-fmt-errors)))
    (home-page "https://www.chezmoi.io/")
    (synopsis "Personal configuration files manager")
    (description "This package helps to manage personal configuration files
across multiple machines.")
    (license license:expat)))

repo_name: maximed/guix

license: mit


code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2015 Siniša Biđin <sinisa@bidin.eu>
;;; Copyright © 2018, 2019, 2020 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2019 Pierre Neidhardt <mail@ambrevar.xyz>
;;; Copyright © 2019 Vasile Dumitrascu <va511e@yahoo.com>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages conky)
  #:use-module (guix packages)
  #:use-module (guix utils)
  #:use-module (guix download)
  #:use-module (guix git-download)
  #:use-module (guix build-system cmake)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (gnu packages curl)
  #:use-module (gnu packages fontutils)
  #:use-module (gnu packages image)
  #:use-module (gnu packages linux)
  #:use-module (gnu packages lua)
  #:use-module (gnu packages ncurses)
  #:use-module (gnu packages pkg-config)
  #:use-module (gnu packages pulseaudio)
  #:use-module (gnu packages xorg))

(define-public conky
  (package
    (name "conky")
    (home-page "https://github.com/brndnmtthws/conky")
    (version "1.12.2")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url home-page)
             (commit (string-append "v" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32 "1grxapl4q37fzk2rsijwz2rrl0aj520y8daki6bg48jb9vjd39n7"))))
    (build-system cmake-build-system)
    (arguments
     `(#:configure-flags
       (list "-DRELEASE=true"
             "-DBUILD_PULSEAUDIO=ON"
             "-DBUILD_WLAN=ON"
             "-DBUILD_TESTS=ON")
       #:phases
       (modify-phases %standard-phases
         (add-after 'unpack 'add-freetype-to-search-path
           (lambda* (#:key inputs #:allow-other-keys)
             (substitute* "cmake/ConkyPlatformChecks.cmake"
               (("set\\(INCLUDE_SEARCH_PATH")
                (string-append
                 "set(INCLUDE_SEARCH_PATH "
                 (assoc-ref inputs "freetype") "/include/freetype2 ")))
             #t))
         (replace 'install
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (bin (string-append out "/bin")))
               (install-file "src/conky" bin))
             #t)))))
    (inputs
     `(("freetype" ,freetype)
       ("imlib2" ,imlib2)
       ("libx11" ,libx11)
       ("libxdamage" ,libxdamage)
       ("libxext" ,libxext)
       ("libxft" ,libxft)
       ("libxinerama" ,libxinerama)
       ("pulseaudio" ,pulseaudio)
       ("lua" ,lua)
       ("ncurses" ,ncurses)
       ("curl" ,curl)
       ("wireless-tools" ,wireless-tools)))
    (native-inputs
     `(("pkg-config" ,pkg-config)))
    (synopsis "Lightweight system monitor for X")
    (description
     "Conky is a lightweight system monitor for X that displays operating
system statistics (CPU, disk, and memory usage, etc.) and more on the
desktop.")
    (license license:gpl3+)))


code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2016, 2017, 2019, 2021 Efraim Flashner <efraim@flashner.co.il>
;;; Copyright © 2017 Mathieu Othacehe <m.othacehe@gmail.com>
;;; Copyright © 2017 Clément Lassieur <clement@lassieur.org>
;;; Copyright © 2017 Ricardo Wurmus <rekado@elephly.net>
;;; Copyright © 2017, 2018, 2019, 2020 Tobias Geerinckx-Rice <me@tobias.gr>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages connman)
  #:use-module (guix packages)
  #:use-module (guix download)
  #:use-module (guix build-system gnu)
  #:use-module (guix licenses)
  #:use-module (guix utils)
  #:use-module (gnu packages)
  #:use-module (gnu packages admin)
  #:use-module (gnu packages compression)
  #:use-module (gnu packages enlightenment)
  #:use-module (gnu packages glib)
  #:use-module (gnu packages linux)
  #:use-module (gnu packages pkg-config)
  #:use-module (gnu packages polkit)
  #:use-module (gnu packages python)
  #:use-module (gnu packages python-xyz)
  #:use-module (gnu packages qt)
  #:use-module (gnu packages readline)
  #:use-module (gnu packages samba)
  #:use-module (gnu packages tls)
  #:use-module (gnu packages vpn))

(define-public connman
  (package
    (name "connman")
    (version "1.40")
    (source
      (origin
        (method url-fetch)
        (uri (string-append "mirror://kernel.org/linux/network/connman/"
                            "connman-" version ".tar.xz"))
        (sha256
         (base32 "04nbxpaxykncp65fyh4lk778vn9145fbxhxa8hbkmailw9yawmqs"))))
    (build-system gnu-build-system)
    (arguments
     `(#:configure-flags
       (list "--enable-nmcompat"
             "--enable-polkit" ; Polkit doesn't need to be present at build time.
             "--enable-openconnect"
             "--enable-openvpn"
             "--enable-vpnc"
             "--enable-l2tp"
             "--localstatedir=/var"
             (string-append
              "--with-dbusconfdir=" (assoc-ref %outputs "out") "/etc")
             (string-append
              "--with-dbusdatadir=" (assoc-ref %outputs "out") "/share"))))
    (native-inputs
     `(("pkg-config" ,pkg-config)
       ("python" ,python-wrapper)))
    (inputs
     `(("dbus" ,dbus)
       ("glib" ,glib)
       ("gnutls" ,gnutls)
       ("iptables" ,iptables)
       ("libmnl" ,libmnl)
       ("lz4" ,lz4)                     ; required by openconnect.pc
       ("readline" ,readline)
       ;; These inputs are needed for connman to include the interface to
       ;; these technologies so IF they are installed they can be used.
       ;; TODO: add neard, ofono
       ("openconnect" ,openconnect)
       ("openvpn" ,openvpn)
       ("ppp" ,ppp)
       ("vpnc" ,vpnc)
       ("wpa-supplicant" ,wpa-supplicant)
       ("xl2tpd" ,xl2tpd)))
    (home-page "https://01.org/connman")
    (synopsis "Connection management daemon")
    (description "Connman provides a daemon for managing Internet connections.
The Connection Manager is designed to be slim and to use as few resources as
possible. It is fully modular system that can be extended through plug-ins.
The plug-in approach allows for easy adaption and modification for various use
cases.  Connman implements DNS resolving and caching, DHCP clients for both
IPv4 and IPv6, link-local IPv4 address handling and tethering (IP connection
sharing) to clients via USB, ethernet, WiFi, cellular and Bluetooth.")
    (license gpl2)))

(define-public econnman
  (package
    (name "econnman")
    (version "1.1")
    (source
      (origin
        (method url-fetch)
        (uri (string-append "https://download.enlightenment.org/rel/apps/"
                            "econnman/econnman-" version ".tar.gz"))
        (sha256
         (base32
          "057pwwavlvrrq26bncqnfrf449zzaim0zq717xv86av4n940gwv0"))))
    (build-system gnu-build-system)
    (arguments
     `(#:configure-flags '("--localstatedir=/var")
       #:phases
       (modify-phases %standard-phases
         (add-after 'unpack 'set-home-directory
           ;; FATAL: Cannot create run dir '/homeless-shelter/.run' - errno=2
           (lambda _ (setenv "HOME" "/tmp") #t))
         (add-after 'install 'wrap-binary
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (bin (string-append out "/bin/econnman-bin")))
               (wrap-program bin
                 `("PYTHONPATH" ":" prefix (,(getenv "PYTHONPATH"))))
               #t))))))
    (native-inputs `(("pkg-config" ,pkg-config)))
    (inputs
     `(("efl" ,efl)
       ("python" ,python-wrapper)
       ("python-dbus" ,python-dbus)
       ("python-efl" ,python-efl)))
    (home-page "https://www.enlightenment.org")
    (synopsis "Connman User Interface written using the EFL")
    (description
     "An EFL user interface for the @code{connman} connection manager.")
    (license lgpl3)))

(define-public cmst
  (package
    (name "cmst")
    (version "2020.11.01")
    (source
     (origin
       (method url-fetch)
       (uri (string-append
             "https://github.com/andrew-bibb/cmst/releases/download/"
             version "/cmst-" version ".tar.xz"))
       (sha256
        (base32 "0jn12wxwjznady6aniwmvahg1dj25p902sdwj0070biv6vx5c7dq"))))
    (inputs
     `(("qtbase" ,qtbase-5)))
    (native-inputs
     `(("qttools" ,qttools)))
    (build-system gnu-build-system)
    (arguments
     '(#:phases
       (modify-phases %standard-phases
         (replace 'configure
           (lambda* (#:key outputs #:allow-other-keys)
             (invoke "qmake"
                     (string-append "PREFIX="
                                    (assoc-ref outputs "out")))))
         (add-before 'build 'fix-Makefiles
           (lambda* (#:key inputs outputs #:allow-other-keys)
             (let ((out (assoc-ref outputs "out")))
               (substitute* (find-files "." "Makefile")
                 (("INSTALL_ROOT)")
                  (string-append "INSTALL_ROOT)" out))
                 (("/usr") ""))
               (substitute* '("apps/cmstapp/cmstapp.pro"
                              "apps/cmstapp/code/control_box/controlbox.cpp"
                              "apps/rootapp/rootapp.pro"
                              "apps/rootapp/system/org.cmst.roothelper.service"
                              "cmst.pri"
                              "cmst.pro")
                 (("/usr") out)
                 (("/etc") (string-append out "/etc")))
               #t))))))
    (home-page "https://github.com/andrew-bibb/cmst")
    (synopsis "Qt frontend for Connman")
    (description
     "Cmst is a Qt based frontend for the @code{connman} connection manager.
This package also provides a systemtray icon.")
    (license x11)))


code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2020 Leo Prikler <leo.prikler@student.tugraz.at>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages convmv)
  #:use-module (gnu packages)
  #:use-module (gnu packages perl)
  #:use-module (guix licenses)
  #:use-module (guix packages)
  #:use-module (guix download)
  #:use-module (guix build-system gnu))

(define-public convmv
  (package
    (name "convmv")
    (version "2.05")
    (source (origin
              (method url-fetch)
              (uri (string-append "https://www.j3e.de/linux/convmv/convmv-"
                                  version ".tar.gz"))
              (sha256
               (base32
                "19hwv197p7c23f43vvav5bs19z9b72jzca2npkjsxgprwj5ardjk"))))
    (build-system gnu-build-system)
    (arguments
     `(#:test-target "test"
       #:make-flags `(,(string-append "PREFIX=" (assoc-ref %outputs "out")))
       #:phases
       (modify-phases %standard-phases
         (delete 'bootstrap)
         (delete 'configure)
         (add-before 'check 'unpack-testsuite
           (lambda _
             (invoke "tar" "xf" "testsuite.tar")
             (patch-shebang "suite/dotests.sh")
             (patch-shebang "suite/parsable_tester.pl")
             #t)))))
    (inputs
     `(("perl" ,perl)))
    (synopsis "Convert filenames between character sets")
    (description
     "convmv is a file renamer, that converts between different encodings,
e.g. from ISO-8859-1 to UTF-8.  It is particularly usefuls for files with
names, that display incorrectly.")
    (license (list gpl2 gpl3))
    (home-page "https://www.j3e.de/")))


code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2014 John Darrington <jmd@gnu.org>
;;; Copyright © 2018 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2020 Marius Bakke <mbakke@fastmail.com>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages cook)
  #:use-module (guix packages)
  #:use-module (guix licenses)
  #:use-module (guix download)
  #:use-module (gnu packages ed)
  #:use-module (gnu packages bison)
  #:use-module (gnu packages groff)
  #:use-module (gnu packages compression)
  #:use-module (guix build-system gnu))

(define-public cook
  (package
    (name "cook")
    (version "2.34")
    (source
     (origin
       (method url-fetch)
       (uri "http://fossies.org/linux/misc/old/cook-2.34.tar.gz")
       (sha256
        (base32
         "104saqnqql1l7zr2pm3f718fdky3ds8j07c6xvwrs1rfkhrw58yw"))))
    (build-system gnu-build-system)
    (arguments
     `(#:parallel-build? #f ; There are some nasty racy rules in the Makefile.
       #:phases
       (modify-phases %standard-phases
         (add-before 'configure 'pre-conf
           (lambda _
             (substitute* (append '("common/env.c")
                                  (find-files "test" "\\.sh"))
               (("/bin/sh") (which "sh")))

             ;; Guix's binutils (because it wants bit-reproducable builds) is
             ;; is configured with the  --enable-deterministic-archives flag.
             ;; This means the timestamp of files appended to an ar archive
             ;; are automatically and silently mutated to 00:00 1 Jan 1970
             ;; which plays havoc with this test, for which correct timestamps
             ;; are very important. Adding the U flag undoes the effect of
             ;; --enable-deterministic-archives and allows this test to work
             ;; again.
             (substitute* "test/00/t0077a.sh"
               (("ar qc") "ar qcU"))

             ;; Guix builds have LC_ALL set to "en_US.utf8", which causes
             ;; `date` to use a 12-hour clock instead of 24h, which in turn
             ;; makes t0217a.sh fail because of unexpected date output.
             (substitute* "test/02/t0217a.sh"
               (("export TZ")
                "export TZ\nLC_ALL=POSIX\nexport LC_ALL"))

             (setenv "SH" (which "sh"))
             #t)))))
    (native-inputs `(("bison" ,bison)
                     ;; For building the documentation:
                     ("groff" ,groff)
                     ;; For the tests:
                     ("sharutils" ,sharutils)
                     ;; One test wants rsh.  However there is no rsh server
                     ;; running in the build environment and so far as I'm
                     ;; aware, it cannot be started without root.
                     ;; This test is therefore just skipped.
                     ;; ("inetutils" ,inetutils)
                     ("ed" ,ed)))
    (home-page (string-append "https://web.archive.org/web/20140727122520/"
                              "http://miller.emu.id.au/pmiller/software/cook/"))
    (synopsis "Tool for constructing files")
    (description "Cook is a tool for constructing files.  It is given a set of
files to create, and recipes of how to create them.  In any non-trivial program
there will be prerequisites to performing the actions necessary to creating
any file, such as include files.  Cook provides a mechanism to define these.")
    (license gpl3+)))


code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2019 Dan Frumin <dfrumin@cs.ru.nl>
;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
;;; Copyright © 2020 Björn Höfling <bjoern.hoefling@bjoernhoefling.de>
;;; Copyright © 2020 raingloom <raingloom@riseup.net>
;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages coq)
  #:use-module (gnu packages)
  #:use-module (gnu packages autotools)
  #:use-module (gnu packages base)
  #:use-module (gnu packages bison)
  #:use-module (gnu packages boost)
  #:use-module (gnu packages emacs)
  #:use-module (gnu packages flex)
  #:use-module (gnu packages gawk)
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages ocaml)
  #:use-module (gnu packages perl)
  #:use-module (gnu packages python)
  #:use-module (gnu packages rsync)
  #:use-module (gnu packages texinfo)
  #:use-module (guix build-system gnu)
  #:use-module (guix build-system ocaml)
  #:use-module (guix download)
  #:use-module (guix git-download)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (guix packages)
  #:use-module (guix utils)
  #:use-module ((srfi srfi-1) #:hide (zip)))

(define-public coq
  (package
    (name "coq")
    (version "8.11.2")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/coq/coq")
             (commit (string-append "V" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32
         "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz"))))
    (native-search-paths
     (list (search-path-specification
            (variable "COQPATH")
            (files (list "lib/coq/user-contrib")))))
    (build-system ocaml-build-system)
    (outputs '("out" "ide"))
    (inputs
     `(("lablgtk" ,lablgtk3)
       ("python" ,python-2)
       ("camlp5" ,camlp5)
       ("ocaml-num" ,ocaml-num)))
    (native-inputs
     `(("ocaml-ounit" ,ocaml-ounit)
       ("rsync" ,rsync)
       ("which" ,which)))
    (arguments
     `(#:phases
       (modify-phases %standard-phases
         (add-after 'unpack 'make-git-checkout-writable
           (lambda _
             (for-each make-file-writable (find-files "."))
             #t))
         (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 'remove-duplicate
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (bin (string-append out "/bin"))
                    (coqtop (string-append bin "/coqtop"))
                    (coqidetop (string-append bin "/coqidetop"))
                    (coqtop.opt (string-append coqtop ".opt"))
                    (coqidetop.opt (string-append coqidetop ".opt")))
               ;; These files are exact copies without `.opt` extension.
               ;; Removing these saves 35 MiB in the resulting package.
               ;; Unfortunately, completely deleting them breaks coqide.
               (delete-file coqtop.opt)
               (delete-file coqidetop.opt)
               (symlink coqtop coqtop.opt)
               (symlink coqidetop coqidetop.opt))
             #t))
         (add-after 'install 'install-ide
           (lambda* (#:key outputs #:allow-other-keys)
             (let ((out (assoc-ref outputs "out"))
                   (ide (assoc-ref outputs "ide")))
               (mkdir-p (string-append ide "/bin"))
               (rename-file (string-append out "/bin/coqide")
                            (string-append ide "/bin/coqide")))
             #t))
         (add-after 'install 'check
           (lambda _
             (with-directory-excursion "test-suite"
               ;; These two tests fail.
               ;; Fails because the output is not formatted as expected.
               (delete-file-recursively "coq-makefile/timing")
               ;; Fails because we didn't build coqtop.byte.
               (delete-file "misc/printers.sh")
               (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 source 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
  ;; The latest release is from 2016 and there has been more than 450 commits
  ;; since then.
  ;; Commit from 2021-06-07.
  (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a")
        (revision "0"))
    (package
      (name "proof-general")
      (version (git-version "4.4" revision commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/ProofGeneral/PG")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
      (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)
                            (string-append "ELISP_START=" %output
                                           "/share/emacs/site-lisp/ProofGeneral"))
         #: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)"))))
           (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")))
                 (substitute* "Makefile"
                   (("/sbin/install-info") "install-info")))))
           (add-after 'unpack 'clean
             (lambda _
               ;; Delete the pre-compiled elc files for Emacs 23.
               (invoke "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") ""))
               (apply invoke "make" "install-doc" make-flags))))))
      (home-page "https://proofgeneral.github.io/")
      (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 coq-flocq
  (package
    (name "coq-flocq")
    (version "3.3.1")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://gitlab.inria.fr/flocq/flocq.git")
             (commit (string-append "flocq-" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32
         "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("autoconf" ,autoconf)
       ("automake" ,automake)
       ("ocaml" ,ocaml)
       ("which" ,which)
       ("coq" ,coq)))
    (arguments
     `(#:configure-flags
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
                            "/lib/coq/user-contrib/Flocq"))
       #:phases
       (modify-phases %standard-phases
         (add-after 'unpack 'remove-failing-examples
           (lambda _
             (substitute* "Remakefile.in"
               ;; Fails on a union error.
               (("Double_rounding_odd_radix.v") ""))
             #t))
         (add-before 'configure 'fix-remake
           (lambda _
             (substitute* "remake.cpp"
               (("/bin/sh") (which "sh")))
             #t))
         (replace 'build
           (lambda _
             (invoke "./remake")))
         (replace 'check
           (lambda _
             (invoke "./remake" "check")))
             ;; TODO: requires coq-gappa and coq-interval.
             ;(invoke "./remake" "check-more")
         (replace 'install
           (lambda _
             (invoke "./remake" "install"))))))
    (home-page "https://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+)))

(define-public coq-gappa
  (package
    (name "coq-gappa")
    (version "1.4.4")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://gitlab.inria.fr/gappa/coq.git")
             (commit (string-append "gappalib-coq-" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32
         "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("autoconf" ,autoconf)
       ("automake" ,automake)
       ("ocaml" ,ocaml)
       ("which" ,which)
       ("coq" ,coq)
       ("camlp5" ,camlp5)
       ("bison" ,bison)
       ("flex" ,flex)))
    (inputs
     `(("gmp" ,gmp)
       ("mpfr" ,mpfr)
       ("boost" ,boost)))
    (propagated-inputs
     `(("coq-flocq" ,coq-flocq)))
    (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")))
             #t))
         (replace 'build
           (lambda _ (invoke "./remake")))
         ;; FIXME: Figure out why failures occur, and re-enable check phase.
         (delete 'check)
         ;; (replace 'check
         ;;   (lambda _ (invoke "./remake" "check")))
         (replace 'install
           (lambda _ (invoke "./remake" "install"))))))
    (home-page "https://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.11.0")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/math-comp/math-comp")
             (commit (string-append "mathcomp-" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("ocaml" ,ocaml)
       ("which" ,which)
       ("coq" ,coq)))
    (arguments
     `(#:tests? #f ; No tests.
       #:phases
       (modify-phases %standard-phases
         (delete 'configure)
         (add-before 'build 'chdir
           (lambda _ (chdir "mathcomp") #t))
         (replace 'install
           (lambda* (#:key outputs #:allow-other-keys)
             (invoke "make" "-f" "Makefile.coq"
                     (string-append "COQLIB=" (assoc-ref outputs "out")
                                    "/lib/coq/")
                     "install"))))))
    (home-page "https://math-comp.github.io/")
    (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.1.0")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://gitlab.inria.fr/coquelicot/coquelicot.git")
             (commit (string-append "coquelicot-" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32
         "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("autoconf" ,autoconf)
       ("automake" ,automake)
       ("ocaml" ,ocaml)
       ("which" ,which)
       ("coq" ,coq)))
    (propagated-inputs
     `(("mathcomp" ,coq-mathcomp)))
    (arguments
     `(#:configure-flags
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
                            "/lib/coq/user-contrib/Coquelicot"))
       #:phases
       (modify-phases %standard-phases
         (add-before 'configure 'fix-remake
           (lambda _
             (substitute* "remake.cpp"
               (("/bin/sh") (which "sh")))
             #t))
         (replace 'build
           (lambda _ (invoke "./remake")))
         (replace 'check
           (lambda _ (invoke "./remake" "check")))
         (replace 'install
           (lambda _ (invoke "./remake" "install"))))))
    (home-page "http://coquelicot.saclay.inria.fr")
    (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+)))

(define-public coq-bignums
  (package
    (name "coq-bignums")
    (version "8.11.0")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                     (url "https://github.com/coq/bignums")
                     (commit (string-append "V" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("ocaml" ,ocaml)
       ("coq" ,coq)))
    (inputs
     `(("camlp5" ,camlp5)))
    (arguments
     `(#:tests? #f ; No test target.
       #:make-flags
       (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
                            "/lib/coq/user-contrib"))
       #: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+)))

(define-public coq-interval
  (package
    (name "coq-interval")
    (version "4.0.0")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://gitlab.inria.fr/coqinterval/interval.git")
             (commit (string-append "interval-" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32
         "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("autoconf" ,autoconf)
       ("automake" ,automake)
       ("ocaml" ,ocaml)
       ("which" ,which)
       ("coq" ,coq)))
    (propagated-inputs
     `(("flocq" ,coq-flocq)
       ("bignums" ,coq-bignums)
       ("coquelicot" ,coq-coquelicot)
       ("mathcomp" ,coq-mathcomp)))
    (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")))
             #t))
         (replace 'build
           (lambda _ (invoke "./remake")))
         (replace 'check
           (lambda _ (invoke "./remake" "check")))
         (replace 'install
           (lambda _ (invoke "./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)))

(define-public coq-autosubst
  ;; Latest commit on that branch, where work on supporting coq 8.6 and
  ;; more recent versions of coq happen.
  (let ((branch "coq86-devel")
        (commit "fa6ef30664511ffa659cbcf3c962715cbee03572"))
    (package
      (name "coq-autosubst")
      (version (git-version "1" branch commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "git://github.com/uds-psl/autosubst")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32 "1cl0bp96bk6lplbl7n5c703vd3gvbs5mvf2qrf8q333kkqd7jqq4"))))
      (build-system gnu-build-system)
      (arguments
       `(#:tests? #f
         #:phases
         (modify-phases %standard-phases
           (delete 'configure)
           (replace 'install
             (lambda* (#:key outputs #:allow-other-keys)
               (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
               (invoke "make"
                       (string-append "COQLIB=" (assoc-ref outputs "out")
                                      "/lib/coq/")
                       "install"))))))
      (native-inputs
       `(("coq" ,coq)))
      (home-page "https://www.ps.uni-saarland.de/autosubst/")
      (synopsis "Coq library for parallel de Bruijn substitutions")
      (description "Formalizing syntactic theories with variable binders is
not easy.  Autosubst is a library for the Coq proof assistant to
automate this process.  Given an inductive definition of syntactic objects in
de Bruijn representation augmented with binding annotations, Autosubst
synthesizes the parallel substitution operation and automatically proves the
basic lemmas about substitutions.  This library contains an automation
tactic that solves equations involving terms and substitutions.  This makes the
usage of substitution lemmas unnecessary.  The tactic is based on our current
work on a decision procedure for the equational theory of an extension of the
sigma-calculus by Abadi et al.  The library is completely written in Coq and
uses Ltac to synthesize the substitution operation.")
      (license license:bsd-3))))

(define-public coq-equations
  (package
    (name "coq-equations")
    (version "1.2.3")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/mattam82/Coq-Equations")
                    (commit (string-append "v" version "-8.11"))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("ocaml"  ,ocaml)
       ("coq"    ,coq)
       ("camlp5" ,camlp5)))
    (arguments
     `(#:test-target "test-suite"
       #:phases
       (modify-phases %standard-phases
         (replace 'configure
           (lambda* (#:key outputs #:allow-other-keys)
             (invoke "sh" "./configure.sh")))
         (replace 'install
           (lambda* (#:key outputs #:allow-other-keys)
             (invoke "make"
                     (string-append "COQLIB=" (assoc-ref outputs "out")
                                    "/lib/coq/")
                     "install"))))))
    (home-page "https://mattam82.github.io/Coq-Equations/")
    (synopsis "Function definition plugin for Coq")
    (description "Equations provides a notation for writing programs
by dependent pattern-matching and (well-founded) recursion in Coq.  It
compiles everything down to eliminators for inductive types, equality
and accessibility, providing a definitional extension to the Coq
kernel.")
    (license license:lgpl2.1)))

(define-public coq-stdpp
  (package
    (name "coq-stdpp")
    (version "1.4.0")
    (synopsis "Alternative Coq standard library std++")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://gitlab.mpi-sws.org/iris/stdpp.git")
                    (commit (string-append "coq-stdpp-" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"))))
    (build-system gnu-build-system)
    (inputs
     `(("coq" ,coq)))
    (arguments
     `(#:tests? #f ; Tests are executed during build phase.
       #:phases
       (modify-phases %standard-phases
         (delete 'configure)
         (replace 'install
           (lambda* (#:key outputs #:allow-other-keys)
             (invoke "make"
                     (string-append "COQLIB=" (assoc-ref outputs "out")
                                    "/lib/coq/")
                     "install"))))))
    (description "This project contains an extended \"Standard Library\" for
Coq called coq-std++.  The key features are:
@itemize
@item Great number of definitions and lemmas for common data structures such
as lists, finite maps, finite sets, and finite multisets.

@item Type classes for common notations (like ∅, ∪, and Haskell-style monad
notations) so that these can be overloaded for different data structures.

@item It uses type classes to keep track of common properties of types, like
it having decidable equality or being countable or finite.

@item Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have m1 =
m2 iff ∀ i, m1 !! i = m2 !! i).  On top of that, the library provides setoid
instances for most types and operations.

@item Various tactics for common tasks, like an ssreflect inspired done tactic
for finishing trivial goals, a simple breadth-first solver naive_solver, an
equality simplifier simplify_eq, a solver solve_proper for proving
compatibility of functions with respect to relations, and a solver set_solver
for goals involving set operations.

@item The library is dependency- and axiom-free.
@end itemize")
    (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
    (license license:bsd-3)))


code:
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2012 Nikita Karetnikov <nikita@karetnikov.org>
;;; Copyright © 2014 Mark H Weaver <mhw@netris.org>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages cpio)
  #:use-module (guix licenses)
  #:use-module (gnu packages)
  #:use-module (gnu packages autotools)
  #:use-module (guix packages)
  #:use-module (guix download)
  #:use-module (guix build-system gnu))

(define-public cpio
  (package
    (name "cpio")
    (version "2.13")
    (source (origin
             (method url-fetch)
             (uri (string-append "mirror://gnu/cpio/cpio-"
                                 version ".tar.bz2"))
             (sha256
              (base32
               "0vbgnhkawdllgnkdn6zn1f56fczwk0518krakz2qbwhxmv2vvdga"))))
    (build-system gnu-build-system)
    (home-page "https://www.gnu.org/software/cpio/")
    (synopsis "Manage cpio and tar file archives")
    (description
     "GNU cpio copies files into or out of cpio or tar archives.  Indeed,
many formats are supported, including legacy formats.  The format is
determined automatically by the program and is handled appropriately.
Furthermore, the location of the archive is not important.  It can be another
file on the drive, a tape, or data on a pipe.")
    (license gpl3+)))