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> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sat, 02 Jul 2022 11:43:02 +0000
Resent-Message-ID: <handler.56356.B.16567621416368 <at> debbugs.gnu.org>
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> debbugs.gnu.org
Cc: Gabriel Hondet <gabrielhondet@HIDDEN>
X-Debbugs-Original-To: guix-patches@HIDDEN
Received: via spool by submit <at> debbugs.gnu.org id=B.16567621416368
          (code B ref -1); Sat, 02 Jul 2022 11:43:02 +0000
Received: (at submit) by debbugs.gnu.org; 2 Jul 2022 11:42:21 +0000
Received: from localhost ([127.0.0.1]:40010 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1o7bW1-0001ee-DE
	for submit <at> debbugs.gnu.org; Sat, 02 Jul 2022 07:42:21 -0400
Received: from lists.gnu.org ([209.51.188.17]:43224)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1o7bVz-0001eW-9g
 for submit <at> debbugs.gnu.org; Sat, 02 Jul 2022 07:42:20 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:53294)
 by lists.gnu.org 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 lepiller.eu ([2a00:5884:8208::1]:60026)
 by eggs.gnu.org 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 lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id 168d0d08;
 Sat, 2 Jul 2022 11:42:05 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from
 :to:cc:subject:message-id:mime-version:content-type; s=dkim; bh=
 GG4vTJiuIim1+5CrN3DJAxkq4csVWNgtxBYMeDTqwnk=; b=Mdoi1yY2by1scMe2
 fJpdCDHY3AQeD/ENP7qopRg6n64l+IG2u9Jt60F5K6n1cdpPk6j9j2vTDRAtllYP
 mHrDiNizJsQRgVHuqCbKQgFnj0fylISxqZkYWIFUEPH+0ixwFa6OtPv3NgA3MAA9
 pnd8LjLqFoYArVUaSOv2RD2//EUKB4WbYu91FItZfskArtRwxUYfxl+st7kUmx4O
 g8bStHTBrtE3rQOn0/wSiD7Pc8pqwYXw2p6wvQBpaINcGarq4OFs9OMOU5uJHv4n
 lmXIU9460gD7dEMrs/cGYudsgHiaUZJCb/tme5tyQZsJajTXZrRxqHShh8ZixsCJ
 sbr1Xw==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id a366ab95
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); 
 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;
 envelope-from=julien@HIDDEN; helo=lepiller.eu
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,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001,
 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> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.3 (--)

--MP_/lxQYYl5gP8w003p7O312bpE
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 :)

--MP_/lxQYYl5gP8w003p7O312bpE
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
   (package
     (name "dedukti")
-    (version "2.6.0")
+    (version "2.7")
     (home-page "https://deducteam.github.io/")
     (source
      (origin
@@ -4517,31 +4517,12 @@ (define-public dedukti
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0frl3diff033i4fmq304b8wbsdnc9mvlhmwd7a3zd699ng2lzbxb"))))
-    (inputs
-     `(("menhir" ,ocaml-menhir)))
-    (native-inputs
-     (list ocamlbuild))
-    (build-system ocaml-build-system)
+         "1dsr3s88kgmcg3najhc29cwfvsxa2plvjws1127fz75kmn15np28"))))
+    (build-system dune-build-system)
     (arguments
-     `(#: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=
 modulo
--=20
2.36.1


--MP_/lxQYYl5gP8w003p7O312bpE--




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> debbugs.gnu.org>
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> debbugs.gnu.org
Date: Sat, 02 Jul 2022 11:43:02 +0000

Thank you for filing a new bug report with debbugs.gnu.org.

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):
 guix-patches@HIDDEN

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

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

--=20
56356: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D56356
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.