[bug#33866] [PATCH] gnu: Add emacs-dedukti-mode emacs-flycheck-dedukti.

[bug#33866] [PATCH] gnu: Add emacs-dedukti-mode emacs-flycheck-dedukti.

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 2345 bytes --]

* gnu/packages/emacs.scm (emacs-dedukti-mode emacs-flycheck-dedukti): New variable.
---
 gnu/packages/emacs.scm | 43 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/gnu/packages/emacs.scm b/gnu/packages/emacs.scm
index 7fdcfb1a3..8c8ae6fb9 100644
--- a/gnu/packages/emacs.scm
+++ b/gnu/packages/emacs.scm
@@ -12854,3 +12854,46 @@ functions to ensure they are called with the right arguments during testing.")
 @code{wordnet}.  Features include completion, if the query is not found
 too ambiguous and navigation in the result buffer.")
       (license license:gpl3+))))
+
+(define-public emacs-dedukti-mode
+  (package
+    (name "emacs-dedukti-mode")
+    (version "git")
+    (home-page "https://github.com/rafoo/dedukti-mode")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url home-page)
+                    (commit "d7c3505a1046187de3c3aeb144455078d514594e")))
+              (sha256
+               (base32
+                "1842wikq24c8rg0ac84vb1qby9ng1nssxswyyni4kq85lng5lcrp"))
+              (file-name (git-file-name name version))))
+    (build-system emacs-build-system)
+    (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
+  (package
+    (name "emacs-flycheck-dedukti")
+    (version "git")
+    (home-page "https://github.com/rafoo/flycheck-dedukti")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url home-page)
+                    (commit "3dbff5646355f39d57a3ec514f560a6b0082a1cd")))
+              (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)))
-- 
2.20.1

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#33866] [PATCH] gnu: Add emacs-dedukti-mode emacs-flycheck-dedukti.

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 2837 bytes --]

Le Tue, 25 Dec 2018 11:57:48 +0100,
Gabriel Hondet <gabrielhondet@gmail.com> a écrit :

> * gnu/packages/emacs.scm (emacs-dedukti-mode emacs-flycheck-dedukti):
> New variable. ---
>  gnu/packages/emacs.scm | 43
> ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43
> insertions(+)
> 
> diff --git a/gnu/packages/emacs.scm b/gnu/packages/emacs.scm
> index 7fdcfb1a3..8c8ae6fb9 100644
> --- a/gnu/packages/emacs.scm
> +++ b/gnu/packages/emacs.scm
> @@ -12854,3 +12854,46 @@ functions to ensure they are called with the
> right arguments during testing.") @code{wordnet}.  Features include
> completion, if the query is not found too ambiguous and navigation in
> the result buffer.") (license license:gpl3+))))
> +
> +(define-public emacs-dedukti-mode
> +  (package
> +    (name "emacs-dedukti-mode")
> +    (version "git")
> +    (home-page "https://github.com/rafoo/dedukti-mode")
> +    (source (origin
> +              (method git-fetch)
> +              (uri (git-reference
> +                    (url home-page)
> +                    (commit
> "d7c3505a1046187de3c3aeb144455078d514594e")))
> +              (sha256
> +               (base32
> +
> "1842wikq24c8rg0ac84vb1qby9ng1nssxswyyni4kq85lng5lcrp"))
> +              (file-name (git-file-name name version))))
> +    (build-system emacs-build-system)
> +    (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
> +  (package
> +    (name "emacs-flycheck-dedukti")
> +    (version "git")
> +    (home-page "https://github.com/rafoo/flycheck-dedukti")
> +    (source (origin
> +              (method git-fetch)
> +              (uri (git-reference
> +                    (url home-page)
> +                    (commit
> "3dbff5646355f39d57a3ec514f560a6b0082a1cd")))
> +              (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)))

Thank you! I'm not an emacs-package expert, but they look fine, except:

please add a copyright line for yourself at the beginning of the file
the version numbers don't follow what can be found elsewhere. I've
never used it, but it seems that you can use git-version instead of
"git". Can you try that?

Thank you! 

[-- Attachment #2: Signature digitale OpenPGP --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

[bug#33866] [PATCH] gnu: Add emacs-dedukti-mode emacs-flycheck-dedukti.

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 2573 bytes --]

Le Tue, 25 Dec 2018 11:57:48 +0100,
Gabriel Hondet <gabrielhondet@gmail.com> a écrit :

> * gnu/packages/emacs.scm (emacs-dedukti-mode emacs-flycheck-dedukti):
> New variable. ---
>  gnu/packages/emacs.scm | 43
> ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43
> insertions(+)
> 
> diff --git a/gnu/packages/emacs.scm b/gnu/packages/emacs.scm
> index 7fdcfb1a3..8c8ae6fb9 100644
> --- a/gnu/packages/emacs.scm
> +++ b/gnu/packages/emacs.scm
> @@ -12854,3 +12854,46 @@ functions to ensure they are called with the
> right arguments during testing.") @code{wordnet}.  Features include
> completion, if the query is not found too ambiguous and navigation in
> the result buffer.") (license license:gpl3+))))
> +
> +(define-public emacs-dedukti-mode
> +  (package
> +    (name "emacs-dedukti-mode")
> +    (version "git")
> +    (home-page "https://github.com/rafoo/dedukti-mode")
> +    (source (origin
> +              (method git-fetch)
> +              (uri (git-reference
> +                    (url home-page)
> +                    (commit
> "d7c3505a1046187de3c3aeb144455078d514594e")))
> +              (sha256
> +               (base32
> +
> "1842wikq24c8rg0ac84vb1qby9ng1nssxswyyni4kq85lng5lcrp"))
> +              (file-name (git-file-name name version))))
> +    (build-system emacs-build-system)
> +    (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
> +  (package
> +    (name "emacs-flycheck-dedukti")
> +    (version "git")
> +    (home-page "https://github.com/rafoo/flycheck-dedukti")
> +    (source (origin
> +              (method git-fetch)
> +              (uri (git-reference
> +                    (url home-page)
> +                    (commit
> "3dbff5646355f39d57a3ec514f560a6b0082a1cd")))
> +              (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)))

Also, please send two separate patches, one per package :)

[-- Attachment #2: Signature digitale OpenPGP --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

[bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode.

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 1955 bytes --]

* gnu/packages/emacs.scm (emacs-dedukti-mode): New variable.
---
 gnu/packages/emacs.scm | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/gnu/packages/emacs.scm b/gnu/packages/emacs.scm
index 7fdcfb1a3..02fd25fef 100644
--- a/gnu/packages/emacs.scm
+++ b/gnu/packages/emacs.scm
@@ -41,6 +41,7 @@
 ;;; Copyright © 2018 Alex Branham <alex.branham@gmail.com>
 ;;; Copyright © 2018 Thorsten Wilms <t_w_@freenet.de>
 ;;; Copyright © 2018 Pierre Langlois <pierre.langlois@gmx.com>
+;;; Copyright © 2018 Gabriel Hondet <gabrielhondet@gmail.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -12854,3 +12855,24 @@ functions to ensure they are called with the right arguments during testing.")
 @code{wordnet}.  Features include completion, if the query is not found
 too ambiguous and navigation in the result buffer.")
       (license license:gpl3+))))
+
+(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))))
+      (build-system emacs-build-system)
+      (synopsis "Emacs major mode for Dedukti files")
+      (description "This package provides an Emacs major mode for editing
+Dedukti files.")
+      (license license:cecill-b))))
-- 
2.20.1

On Tue 25 Dec 2018 at 18:51 Julien Lepiller wrote:

> Also, please send two separate patches, one per package :)
Fine, so this is the first one, the other is on its way.


[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#33866] [PATCH 2/2] gnu: Add emacs-flycheck-dedukti.

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 1706 bytes --]

* gnu/packages/emacs.scm (emacs-flycheck-dedukti): New variable.
---
 gnu/packages/emacs.scm | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/gnu/packages/emacs.scm b/gnu/packages/emacs.scm
index 02fd25fef..70cf96614 100644
--- a/gnu/packages/emacs.scm
+++ b/gnu/packages/emacs.scm
@@ -12876,3 +12876,27 @@ too ambiguous and navigation in the result buffer.")
       (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))))
-- 
2.20.1

On Tue 25 Dec 2018 at 18:51 Julien Lepiller wrote:

> Also, please send two separate patches, one per package :)
And here is the 2nd!


[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode.

[Julien Lepiller]

Le Tue, 25 Dec 2018 19:45:07 +0100,
Gabriel Hondet <gabrielhondet@gmail.com> a écrit :

> * gnu/packages/emacs.scm (emacs-dedukti-mode): New variable.
> ---
>  gnu/packages/emacs.scm | 22 ++++++++++++++++++++++
>  1 file changed, 22 insertions(+)
> 
> diff --git a/gnu/packages/emacs.scm b/gnu/packages/emacs.scm
> index 7fdcfb1a3..02fd25fef 100644
> --- a/gnu/packages/emacs.scm
> +++ b/gnu/packages/emacs.scm
> @@ -41,6 +41,7 @@
>  ;;; Copyright © 2018 Alex Branham <alex.branham@gmail.com>
>  ;;; Copyright © 2018 Thorsten Wilms <t_w_@freenet.de>
>  ;;; Copyright © 2018 Pierre Langlois <pierre.langlois@gmx.com>
> +;;; Copyright © 2018 Gabriel Hondet <gabrielhondet@gmail.com>
>  ;;;
>  ;;; This file is part of GNU Guix.
>  ;;;
> @@ -12854,3 +12855,24 @@ functions to ensure they are called with the
> right arguments during testing.") @code{wordnet}.  Features include
> completion, if the query is not found too ambiguous and navigation in
> the result buffer.") (license license:gpl3+))))
> +
> +(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))))
> +      (build-system emacs-build-system)
> +      (synopsis "Emacs major mode for Dedukti files")
> +      (description "This package provides an Emacs major mode for
> editing +Dedukti files.")
> +      (license license:cecill-b))))

I'm not an emacs user, so I'm a bit worried that this package won't be
able to find dedukti (it's not an input at all!). I see this in the
code:

(defcustom dedukti-path "/usr/bin/dkcheck" ...)

I would say that it means that dedukti-mode will not find dkcheck at
all... What do you think? If that's the case, could you add dedukti as
an input and substitute* that path in a custom phase? Or make sure it
loads dedukti from the path at least.

[bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode.

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 3108 bytes --]


On Wed 26 Dec 2018 at 15:27 Julien Lepiller wrote:

> I'm not an emacs user, so I'm a bit worried that this package won't be
> able to find dedukti (it's not an input at all!). I see this in the
> code:
>
> (defcustom dedukti-path "/usr/bin/dkcheck" ...)
>
> I would say that it means that dedukti-mode will not find dkcheck at
> all... What do you think? If that's the case, could you add dedukti as
> an input and substitute* that path in a custom phase? Or make sure it
> loads dedukti from the path at least.

Well seen indeed, here is the new version, which should hopefully be ok!

* gnu/packages/emacs.scm (emacs-dedukti-mode): New variable.
---
 gnu/packages/emacs.scm | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/gnu/packages/emacs.scm b/gnu/packages/emacs.scm
index 7fdcfb1a3..2cc6ca438 100644
--- a/gnu/packages/emacs.scm
+++ b/gnu/packages/emacs.scm
@@ -41,6 +41,7 @@
 ;;; Copyright © 2018 Alex Branham <alex.branham@gmail.com>
 ;;; Copyright © 2018 Thorsten Wilms <t_w_@freenet.de>
 ;;; Copyright © 2018 Pierre Langlois <pierre.langlois@gmx.com>
+;;; Copyright © 2018 Gabriel Hondet <gabrielhondet@gmail.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -122,6 +123,7 @@
   #:use-module (gnu packages video)
   #:use-module (gnu packages haskell)
   #:use-module (gnu packages wordnet)
+  #:use-module (gnu packages ocaml)
   #:use-module (guix utils)
   #:use-module (srfi srfi-1)
   #:use-module (ice-9 match))
@@ -12854,3 +12856,35 @@ functions to ensure they are called with the right arguments during testing.")
 @code{wordnet}.  Features include completion, if the query is not found
 too ambiguous and navigation in the result buffer.")
       (license license:gpl3+))))
+
+(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))))
-- 
2.20.1


[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

bug#33866: [PATCH] gnu: Add emacs-dedukti-mode emacs-flycheck-dedukti.

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 110 bytes --]

Pushed as 4a2e1e72806fd62e54201a4aacde213d419d04bd and
ad536c98f9125f47dd948be7dd42d5c34e84bdfd, thank you!

[-- Attachment #2: Signature digitale OpenPGP --]
[-- Type: application/pgp-signature, Size: 833 bytes --]