From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([208.118.235.92]:41441) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gcAAH-0008BC-K8 for guix-patches@gnu.org; Wed, 26 Dec 2018 09:28:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gcAAE-0006Sr-Bn for guix-patches@gnu.org; Wed, 26 Dec 2018 09:28:05 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:51569) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gcAAE-0006SJ-6X for guix-patches@gnu.org; Wed, 26 Dec 2018 09:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gcAAD-0006kU-PY for guix-patches@gnu.org; Wed, 26 Dec 2018 09:28:01 -0500 Subject: [bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode. Resent-Message-ID: Date: Wed, 26 Dec 2018 15:27:35 +0100 From: Julien Lepiller Message-ID: <20181226152735.5cdb50aa@lepiller.eu> In-Reply-To: <87wonxwimk.fsf@gmail.com> References: <87zhstx41e.fsf@gmail.com> <20181225185155.038cee5b@lepiller.eu> <87wonxwimk.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Gabriel Hondet Cc: 33866@debbugs.gnu.org Le Tue, 25 Dec 2018 19:45:07 +0100, Gabriel Hondet a =C3=A9crit : > * gnu/packages/emacs.scm (emacs-dedukti-mode): New variable. > --- > gnu/packages/emacs.scm | 22 ++++++++++++++++++++++ > 1 file changed, 22 insertions(+) >=20 > 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 =C2=A9 2018 Alex Branham > ;;; Copyright =C2=A9 2018 Thorsten Wilms > ;;; Copyright =C2=A9 2018 Pierre Langlois > +;;; Copyright =C2=A9 2018 Gabriel Hondet > ;;; > ;;; 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.