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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 33866 in the body.
You can then email your comments to 33866 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: guix-patches <at> gnu.org
Subject: [PATCH] gnu: Add emacs-dedukti-mode emacs-flycheck-dedukti.
Date: Tue, 25 Dec 2018 11:57:48 +0100

[Message part 1 (text/plain, inline)]

* 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

[signature.asc (application/pgp-signature, inline)]

Message #8 received at 33866 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: Gabriel Hondet <gabrielhondet <at> gmail.com>
Cc: 33866 <at> debbugs.gnu.org
Subject: Re: [bug#33866] [PATCH] gnu: Add emacs-dedukti-mode
 emacs-flycheck-dedukti.
Date: Tue, 25 Dec 2018 18:46:54 +0100

[Message part 1 (text/plain, inline)]

Le Tue, 25 Dec 2018 11:57:48 +0100,
Gabriel Hondet <gabrielhondet <at> 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! 

[Message part 2 (application/pgp-signature, inline)]

Message #11 received at 33866 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: Gabriel Hondet <gabrielhondet <at> gmail.com>
Cc: 33866 <at> debbugs.gnu.org
Subject: Re: [bug#33866] [PATCH] gnu: Add emacs-dedukti-mode
 emacs-flycheck-dedukti.
Date: Tue, 25 Dec 2018 18:51:55 +0100

[Message part 1 (text/plain, inline)]

Le Tue, 25 Dec 2018 11:57:48 +0100,
Gabriel Hondet <gabrielhondet <at> 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 :)

[Message part 2 (application/pgp-signature, inline)]

Message #14 received at 33866 <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 33866 <at> debbugs.gnu.org
Subject: Re: [bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode.
Date: Tue, 25 Dec 2018 19:45:07 +0100

[Message part 1 (text/plain, inline)]

* 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 <at> gmail.com>
 ;;; Copyright © 2018 Thorsten Wilms <t_w_ <at> freenet.de>
 ;;; Copyright © 2018 Pierre Langlois <pierre.langlois <at> gmx.com>
+;;; Copyright © 2018 Gabriel Hondet <gabrielhondet <at> 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.

[signature.asc (application/pgp-signature, inline)]

Message #17 received at 33866 <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 33866 <at> debbugs.gnu.org
Subject: Re: [bug#33866] [PATCH 2/2] gnu: Add emacs-flycheck-dedukti.
Date: Tue, 25 Dec 2018 19:47:32 +0100

[Message part 1 (text/plain, inline)]

* 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!

[signature.asc (application/pgp-signature, inline)]

Message #20 received at 33866 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: Gabriel Hondet <gabrielhondet <at> gmail.com>
Cc: 33866 <at> debbugs.gnu.org
Subject: Re: [bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode.
Date: Wed, 26 Dec 2018 15:27:35 +0100

Le Tue, 25 Dec 2018 19:45:07 +0100,
Gabriel Hondet <gabrielhondet <at> 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 <at> gmail.com>
>  ;;; Copyright © 2018 Thorsten Wilms <t_w_ <at> freenet.de>
>  ;;; Copyright © 2018 Pierre Langlois <pierre.langlois <at> gmx.com>
> +;;; Copyright © 2018 Gabriel Hondet <gabrielhondet <at> 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.

Message #23 received at 33866 <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 33866 <at> debbugs.gnu.org
Subject: Re: [bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode.
Date: Wed, 26 Dec 2018 19:09:00 +0100

[Message part 1 (text/plain, inline)]

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 <at> gmail.com>
 ;;; Copyright © 2018 Thorsten Wilms <t_w_ <at> freenet.de>
 ;;; Copyright © 2018 Pierre Langlois <pierre.langlois <at> gmx.com>
+;;; Copyright © 2018 Gabriel Hondet <gabrielhondet <at> 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

[signature.asc (application/pgp-signature, inline)]

Message #28 received at 33866-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 33866-done <at> debbugs.gnu.org
Subject: Re: [bug#33866] [PATCH] gnu: Add emacs-dedukti-mode
 emacs-flycheck-dedukti.
Date: Thu, 27 Dec 2018 09:20:43 +0100

[Message part 1 (text/plain, inline)]

Pushed as 4a2e1e72806fd62e54201a4aacde213d419d04bd and
ad536c98f9125f47dd948be7dd42d5c34e84bdfd, thank you!

[Message part 2 (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.