From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([208.118.235.92]:58209) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gcDdC-0007ze-9r for guix-patches@gnu.org; Wed, 26 Dec 2018 13:10:11 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gcDd6-0006AY-3l for guix-patches@gnu.org; Wed, 26 Dec 2018 13:10:09 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:42649) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gcDd4-00069Q-0z for guix-patches@gnu.org; Wed, 26 Dec 2018 13:10:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gcDd3-00068c-R5 for guix-patches@gnu.org; Wed, 26 Dec 2018 13:10:01 -0500 Subject: [bug#33866] [PATCH 1/2] gnu: Add emacs-dedukti-mode. Resent-Message-ID: References: <87zhstx41e.fsf@gmail.com> <20181225185155.038cee5b@lepiller.eu> <87wonxwimk.fsf@gmail.com> <20181226152735.5cdb50aa@lepiller.eu> From: Gabriel Hondet In-reply-to: <20181226152735.5cdb50aa@lepiller.eu> Date: Wed, 26 Dec 2018 19:09:00 +0100 Message-ID: <87sgykw477.fsf@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" 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: Julien Lepiller Cc: 33866@debbugs.gnu.org --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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. =2D-- 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 =2D-- 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. ;;; @@ -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)))) =2D-=20 2.20.1 --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlwjw7wACgkQMbyBBfZZ 1CXs7BAAkxwCKeLkXP4H7VAPrQAb7ziYeOobz4/87wDCXC5Ps+6RkFff/RiNXEp/ XOEu+b2AvXJ+2UGYJcs5J4veTU8PX20P1TgO/gUPOJddEk4ds3+RnizVuxsIX1ns 6ACwwY2A+q8On50z309F4EFGUym6EVaT4dHDqBw6+mfshzq+HjcsufClwrmGYqlP iZcT78KaW1GhpFMn6Vppn8bk2EqUWeYXYvoIB7YLGv5hL52dfOQfDTdLVRPvSqBz 5cWdCkQzUCDWGI3h4JnvB1VHB+quluAYOFHuSiKgZiwjls+ExbhgrZbbqHWb3W9c W4GDfLwPi33GZwGlnbD5sUbhUnIH36DImCL0LaCq0V17/hWveywYz7QoKzUxONQV 4yzsPHFDZZlLkDutSBXQWeMljwnoQNbzl9//ZUzg4GcOpXyaKxPlrrJMqRkKZ8pf n/8ReyEcr7osxHIH4vaG3LT9T86LEnwrWo3exZWv12/WqiYLqLFZg5cXDv9Me/Ej vuKsp2Sox8uwxOo//anTl0N7z9DC5OTBfe9XkoVq22HFr80r/vOCpQoNqZwU7OVn 2OKP1N1fgbUMSZeaZ2e4H7Enc6rwJxEW1xR4BRsdGiwfHHhAfRJiGtFXo478FQHh 20bchv3vHkN+/OGEsFohACmF0JCiMuKimG1ZcnMkRk6Xq0DzUgo= =chWb -----END PGP SIGNATURE----- --=-=-=--