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

Done

Details

2 participants

Gabriel Hondet
Julien Lepiller

Owner: unassigned

Submitted by: Gabriel Hondet

Severity: normal

Debbugs page

Gabriel Hondet wrote 6 years ago

Recipients:(address . guix-patches@gnu.org)

Message-ID:87zhstx41e.fsf@gmail.com

* gnu/packages/emacs.scm (emacs-dedukti-mode emacs-flycheck-dedukti): New variable.

---

gnu/packages/emacs.scm | 43 ++++++++++++++++++++++++++++++++++++++++++

1 file changed, 43 insertions(+)

Toggle diff (53 lines)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

Julien Lepiller wrote 6 years ago

Recipients:(name . Gabriel Hondet)(address . gabrielhondet@gmail.com)(address . 33866@debbugs.gnu.org)

Message-ID:20181225184654.6ccc561a@lepiller.eu

Le Tue, 25 Dec 2018 11:57:48 +0100,

Gabriel Hondet <gabrielhondet@gmail.com> a écrit :

Toggle quote (62 lines)> * 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!

Julien Lepiller wrote 6 years ago

Recipients:(name . Gabriel Hondet)(address . gabrielhondet@gmail.com)(address . 33866@debbugs.gnu.org)

Message-ID:20181225185155.038cee5b@lepiller.eu

Le Tue, 25 Dec 2018 11:57:48 +0100,

Gabriel Hondet <gabrielhondet@gmail.com> a écrit :

Toggle quote (62 lines)> * 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 :)

Gabriel Hondet wrote 6 years ago

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

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 33866@debbugs.gnu.org)

Message-ID:87wonxwimk.fsf@gmail.com

* gnu/packages/emacs.scm (emacs-dedukti-mode): New variable.

---

gnu/packages/emacs.scm | 22 ++++++++++++++++++++++

1 file changed, 22 insertions(+)

Toggle diff (44 lines)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.

Gabriel Hondet wrote 6 years ago

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

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 33866@debbugs.gnu.org)

Message-ID:87va3hwiij.fsf@gmail.com

* gnu/packages/emacs.scm (emacs-flycheck-dedukti): New variable.

---

gnu/packages/emacs.scm | 24 ++++++++++++++++++++++++

1 file changed, 24 insertions(+)

Toggle diff (39 lines)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!

Julien Lepiller wrote 6 years ago

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

Recipients:(name . Gabriel Hondet)(address . gabrielhondet@gmail.com)(address . 33866@debbugs.gnu.org)

Message-ID:20181226152735.5cdb50aa@lepiller.eu

Le Tue, 25 Dec 2018 19:45:07 +0100,

Gabriel Hondet <gabrielhondet@gmail.com> a écrit :

Toggle quote (44 lines)> * 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.

Gabriel Hondet wrote 6 years ago

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 33866@debbugs.gnu.org)

Message-ID:87sgykw477.fsf@gmail.com

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

Toggle quote (11 lines)> 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(+)

Toggle diff (58 lines)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

Julien Lepiller wrote 6 years ago

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

Recipients:(address . 33866-done@debbugs.gnu.org)

Message-ID:20181227092043.3ba0df88@lepiller.eu

Pushed as 4a2e1e72806fd62e54201a4aacde213d419d04bd and

ad536c98f9125f47dd948be7dd42d5c34e84bdfd, thank you!

Closed

Your comment

This issue is archived.

To comment on this conversation send an email to 33866@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it

mumi current 33866

Then, you may apply the latest patchset in this issue (with sign off)

mumi am -- -s

Or, compose a reply to this issue

mumi compose

Or, send patches to this issue

mumi send-email *.patch

You may also tag this issue. See list of standard tags. For example, to set the confirmed and easy tags

mumi command -t +confirmed -t +easy

Or, remove the moreinfo tag and set the help tag

mumi command -t -moreinfo -t +help

is:open	open issues
is:done	closed issues
submitter:<who>	search issue submitter
author:<who>	search by message author
date:yesterday..now	search by issue date
mdate:3m..2d	search by message date