GNU logs - #56356, boring messages

Message sent to guix-patches@HIDDEN:

X-Loop: help-debbugs@HIDDEN
Subject: [bug#56356] [WIP PATCH] gnu: dedukti: Update to 1.7.
Resent-From: Julien Lepiller <julien@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at>>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sat, 02 Jul 2022 11:43:02 +0000
Resent-Message-ID: <handler.56356.B.16567621416368 <at>>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: report 56356
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 56356 <at>
Cc: Gabriel Hondet <gabrielhondet@HIDDEN>
X-Debbugs-Original-To: guix-patches@HIDDEN
Received: via spool by submit <at> id=B.16567621416368
          (code B ref -1); Sat, 02 Jul 2022 11:43:02 +0000
Received: (at submit) by; 2 Jul 2022 11:42:21 +0000
Received: from localhost ([]:40010
	by with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at>>)
	id 1o7bW1-0001ee-DE
	for submit <at>; Sat, 02 Jul 2022 07:42:21 -0400
Received: from ([]:43224)
 by with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1o7bVz-0001eW-9g
 for submit <at>; Sat, 02 Jul 2022 07:42:20 -0400
Received: from ([2001:470:142:3::10]:53294)
 by with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <julien@HIDDEN>)
 id 1o7bVx-0004vA-Gb
 for guix-patches@HIDDEN; Sat, 02 Jul 2022 07:42:18 -0400
Received: from ([2a00:5884:8208::1]:60026)
 by with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <julien@HIDDEN>)
 id 1o7bVq-0000os-MC
 for guix-patches@HIDDEN; Sat, 02 Jul 2022 07:42:15 -0400
Received: from (localhost [])
 by (OpenSMTPD) with ESMTP id 168d0d08;
 Sat, 2 Jul 2022 11:42:05 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed;; h=date:from
 :to:cc:subject:message-id:mime-version:content-type; s=dkim; bh=
 GG4vTJiuIim1+5CrN3DJAxkq4csVWNgtxBYMeDTqwnk=; b=Mdoi1yY2by1scMe2
Received: by (OpenSMTPD) with ESMTPSA id a366ab95
 Sat, 2 Jul 2022 11:42:04 +0000 (UTC)
Date: Sat, 2 Jul 2022 13:42:01 +0200
From: Julien Lepiller <julien@HIDDEN>
Message-ID: <20220702134201.3cf338e1@HIDDEN>
X-Mailer: Claws Mail 4.0.0 (GTK+ 3.24.30; x86_64-pc-linux-gnu)
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="MP_/lxQYYl5gP8w003p7O312bpE"
Received-SPF: pass client-ip=2a00:5884:8208::1;
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.3 (-)
X-BeenThere: debbugs-submit <at>
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <>
List-Unsubscribe: <>, 
 <mailto:debbugs-submit-request <at>>
List-Archive: <>
List-Post: <mailto:debbugs-submit <at>>
List-Help: <mailto:debbugs-submit-request <at>>
List-Subscribe: <>, 
 <mailto:debbugs-submit-request <at>>
Errors-To: debbugs-submit-bounces <at>
Sender: "Debbugs-submit" <debbugs-submit-bounces <at>>
X-Spam-Score: -2.3 (--)

Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

Hi Guix and Gabriel,

Gabriel, since you provided the initial patch to add dedukti and the
emacs mode, I thought you might be interested, so I CC'd you. Feel free
to ignore if you've moved to something else :)

Attached is a patch to update dedukti to the latest version, 1.7. The
patch works and dedukti seems to be working, though I don't really know
how to use it, so maybe not :)

The issue is with its dependent emacs-dedukti-mode. It embeds a
reference to the "dkcheck" tool that does not exist in this version of
the package. Instead, you're supposed to call "dk check" (the --help
still mentions dkcheck, so maybe I did something wrong in packaging?)

I noticed that emacs-dedukti-mode is 5 years old and unmaintained
upstream, while there is a dedukti-mode provided in the git repository
of dedukti that is only 2 years old. I don't use emacs and I don't know
how to solve this issue, so I'm not updating the package yet.

I'd appreciate some help, either to find a better substitution pattern
in the current emacs-dedukti-mode package, or to package the one
provided by dedukti, or maybe to figure out another direction I didn't
see :)

Content-Type: text/x-patch
Content-Transfer-Encoding: quoted-printable
Content-Disposition: attachment; filename=0001-gnu-dedukti-Update-to-2.7.patch

=46rom cd89e04ea72c18d59a01baccc9311b5070c845a4 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@HIDDEN>
Date: Sat, 2 Jul 2022 13:36:08 +0200
Subject: [PATCH] gnu: dedukti: Update to 2.7.

* gnu/packages/ocaml.scm (dedukti): Update to 2.7.
 gnu/packages/ocaml.scm | 31 ++++++-------------------------
 1 file changed, 6 insertions(+), 25 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index cd8778231e..e3a4bb15ce 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -4506,7 +4506,7 @@ (define-public ocaml-tsdl
 (define-public dedukti
     (name "dedukti")
-    (version "2.6.0")
+    (version "2.7")
     (home-page "")
@@ -4517,31 +4517,12 @@ (define-public dedukti
        (file-name (git-file-name name version))
-         "0frl3diff033i4fmq304b8wbsdnc9mvlhmwd7a3zd699ng2lzbxb"))))
-    (inputs
-     `(("menhir" ,ocaml-menhir)))
-    (native-inputs
-     (list ocamlbuild))
-    (build-system ocaml-build-system)
+         "1dsr3s88kgmcg3najhc29cwfvsxa2plvjws1127fz75kmn15np28"))))
+    (build-system dune-build-system)
-     `(#:phases
-       ,#~(modify-phases %standard-phases
-            (delete 'configure)
-            (replace 'build
-              (lambda _
-                (invoke "make")))
-            (replace 'check
-              (lambda _
-                (invoke "make" "tests")))
-            (add-before 'install 'set-binpath
-              ;; Change binary path in the makefile
-              (lambda _
-                (substitute* "GNUmakefile"
-                  (("BINDIR =3D (.*)$")
-                   (string-append "BINDIR =3D " #$output "/bin")))))
-            (replace 'install
-              (lambda _
-                (invoke "make" "install"))))))
+     `(#:test-target "tests"))
+    (inputs (list gmp ocaml-cmdliner ocaml-z3 z3))
+    (native-inputs (list ocaml-menhir))
     (synopsis "Proof-checker for the =CE=BB=CE=A0-calculus modulo theory, =
an extension of
 the =CE=BB-calculus")
     (description "Dedukti is a proof-checker for the =CE=BB=CE=A0-calculus=


Message sent:

Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
MIME-Version: 1.0
X-Mailer: MIME-tools 5.505 (Entity 5.505)
Content-Type: text/plain; charset=utf-8
X-Loop: help-debbugs@HIDDEN
From: help-debbugs@HIDDEN (GNU bug Tracking System)
To: Julien Lepiller <julien@HIDDEN>
Subject: bug#56356: Acknowledgement ([WIP PATCH] gnu: dedukti: Update to 1.7.)
Message-ID: <handler.56356.B.16567621416368.ack <at>>
References: <20220702134201.3cf338e1@HIDDEN>
X-Gnu-PR-Message: ack 56356
X-Gnu-PR-Package: guix-patches
X-Gnu-PR-Keywords: patch
Reply-To: 56356 <at>
Date: Sat, 02 Jul 2022 11:43:02 +0000

Thank you for filing a new bug report with

This is an automatically generated reply to let you know your message
has been received.

Your message is being forwarded to the package maintainers and other
interested parties for their attention; they will reply in due course.

Your message has been sent to the package maintainer(s):

If you wish to submit further information on this problem, please
send it to 56356 <at>

Please do not send mail to help-debbugs@HIDDEN unless you wish
to report a problem with the Bug-tracking system.

GNU Bug Tracking System
Contact help-debbugs@HIDDEN with problems

Last modified: Sat, 2 Jul 2022 11:45:02 UTC

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