From unknown Sun Aug 10 16:47:03 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#56356] [WIP PATCH] gnu: dedukti: Update to 1.7. Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 02 Jul 2022 11:43:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 56356 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 56356@debbugs.gnu.org Cc: Gabriel Hondet X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@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 ) id 1o7bW1-0001ee-DE for submit@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 ) id 1o7bVz-0001eW-9g for submit@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 ) id 1o7bVx-0004vA-Gb for guix-patches@gnu.org; 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 ) id 1o7bVq-0000os-MC for guix-patches@gnu.org; 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 Message-ID: <20220702134201.3cf338e1@sybil.lepiller.eu> 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@lepiller.eu; 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@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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 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-- From unknown Sun Aug 10 16:47:03 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#56356] [WIP PATCH] gnu: dedukti: Update to 1.7. Resent-From: Gabriel Hondet Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 10 Jul 2022 09:56:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 56356 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Julien Lepiller Cc: 56356@debbugs.gnu.org X-Debbugs-Original-Cc: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.165744692617148 (code B ref -1); Sun, 10 Jul 2022 09:56:02 +0000 Received: (at submit) by debbugs.gnu.org; 10 Jul 2022 09:55:26 +0000 Received: from localhost ([127.0.0.1]:36260 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oATev-0004SV-Qn for submit@debbugs.gnu.org; Sun, 10 Jul 2022 05:55:26 -0400 Received: from lists.gnu.org ([209.51.188.17]:49458) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oATet-0004SN-ME for submit@debbugs.gnu.org; Sun, 10 Jul 2022 05:55:23 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:47296) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oATet-0005By-E0 for guix-patches@gnu.org; Sun, 10 Jul 2022 05:55:23 -0400 Received: from mail-wr1-x434.google.com ([2a00:1450:4864:20::434]:36532) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oATer-0002cE-Ux for guix-patches@gnu.org; Sun, 10 Jul 2022 05:55:23 -0400 Received: by mail-wr1-x434.google.com with SMTP id o4so3593716wrh.3 for ; Sun, 10 Jul 2022 02:55:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to; bh=3rdIGjRV7ksOi7aX6Jldl0fWZ6BM82EifwY6M77HpfM=; b=ZR3O0aTVv6vYvIIEpi6/si12O4TVmQpsznh4uiYhAERm5+k60MfN2aNuqobKaGSrkN 0W0mh5JqZz2DTrlVG9fNHKtnyEbguq8YPdWzfsrNY6lb+rfSMw9327VTCZ0MPPNeSnbB SM7CPNVimU/HVnO2z4N8e4n3ybjEAKIHzpD/4jKCCBjvrvysYkCG/BrPHWf3vqQmH9+S 1AsJ8I7z639lqmXkBJprHPaPEu+g4Huogn1m+w5Hx5Gm0rIAXsP7SBaYZ37k5tZQYqfU GsqXU4Gg98vwCtTLVmyDja/7VWFGoTZAqlgQGj8VUoMAqvhRAe80Np86LjjteaKibD+k 4BEg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:references :mime-version:content-disposition:in-reply-to; bh=3rdIGjRV7ksOi7aX6Jldl0fWZ6BM82EifwY6M77HpfM=; b=U/RHrTyF7GOFSvuZ6NFYjjWzqkl9GZY71Sx6JLoop2DuLuhyGMLSAZ8Re+ohnPqqnd lvndzX5bgU98gh72ev6k/lBU6da1u3waw762HkcU+nau7oxVUAA9MeCkB62gKRW3u/ii opqS8vN/ss6t+YvjXh8Gi4sCgzVm134fx3Vz1y5/xYgIDRXKscyL+WXslVuf56nVRpT9 nymasKU5D5c7JFuqj/ralUojgCTjgTR1lpw5ijrVbhjhr4M49nUDS2fF2ca0ZjQ4mp8F eASEByejeSOwmUg3eJ4YQQBpcKupDR40sRhyIOP1iFwnI5goQ60y1Nvrv3JUAFNaXhAv Eexw== X-Gm-Message-State: AJIora/dEof1chVOo9H7jfJS04YvLWfF+WFSumS7HJSv7nWPTh4divTu txLTsgkfYNIH3bD7BPf4doGwO50bbu0= X-Google-Smtp-Source: AGRyM1uk9D8pwfiMy5k2Ev3F8VzckdybycI3915cL9Qf+/CrpIJ1rtTBlOzwwiQln3TvnOIke4ctAQ== X-Received: by 2002:a5d:47cd:0:b0:21d:30ea:a0d5 with SMTP id o13-20020a5d47cd000000b0021d30eaa0d5mr12423764wrc.74.1657446919843; Sun, 10 Jul 2022 02:55:19 -0700 (PDT) Received: from localhost (2a01cb0400145b00ae675dfffe707cef.ipv6.abo.wanadoo.fr. [2a01:cb04:14:5b00:ae67:5dff:fe70:7cef]) by smtp.gmail.com with ESMTPSA id v18-20020a5d6792000000b0021d4155cd6fsm3256387wru.53.2022.07.10.02.55.19 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 10 Jul 2022 02:55:19 -0700 (PDT) Date: Sun, 10 Jul 2022 11:55:18 +0200 From: Gabriel Hondet Message-ID: References: <20220702134201.3cf338e1@sybil.lepiller.eu> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline In-Reply-To: <20220702134201.3cf338e1@sybil.lepiller.eu> Received-SPF: pass client-ip=2a00:1450:4864:20::434; envelope-from=gabrielhondet@gmail.com; helo=mail-wr1-x434.google.com 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, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=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@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.3 (--) Hi Julien and Guix, On Sat, Jul 02, 2022 at 01:42:01PM +0200, Julien Lepiller wrote: > 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 :) Sorry for the late reply, and thanks a lot for the update, the patch seems perfect. > 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 :) Indeed, the emacs-dedukti-mode is deprecated, it would be better to just remove it from guix recipes. Cheers, Gabriel From unknown Sun Aug 10 16:47:03 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#56356] [WIP PATCH] gnu: dedukti: Update to 1.7. Resent-From: Ludovic =?UTF-8?Q?Court=C3=A8s?= Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 17 Jul 2022 18:31:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 56356 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Julien Lepiller Cc: Gabriel Hondet , 56356@debbugs.gnu.org Received: via spool by 56356-submit@debbugs.gnu.org id=B56356.165808265919946 (code B ref 56356); Sun, 17 Jul 2022 18:31:02 +0000 Received: (at 56356) by debbugs.gnu.org; 17 Jul 2022 18:30:59 +0000 Received: from localhost ([127.0.0.1]:48549 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oD92h-0005Be-4p for submit@debbugs.gnu.org; Sun, 17 Jul 2022 14:30:59 -0400 Received: from eggs.gnu.org ([209.51.188.92]:37944) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oD92b-0005BH-W2 for 56356@debbugs.gnu.org; Sun, 17 Jul 2022 14:30:57 -0400 Received: from fencepost.gnu.org ([2001:470:142:3::e]:49286) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oD92T-00085g-HU; Sun, 17 Jul 2022 14:30:45 -0400 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=gnu.org; s=fencepost-gnu-org; h=MIME-Version:In-Reply-To:Date:References:Subject:To: From; bh=GufLofDoOgHy+A36IonNx6pN1TIIRbBcUkfslF4JqE4=; b=qE9Vi6WVRTyGgHVg24uZ 2+TH9hKAZwuYMQ0jqKtOSwpUM5Siicc+TWDqZ5f6HmZA4biP+3a6nj+/z8gzmdTLygQGwDvZqHGEe P8l98fBCAXb2MC0QXc7LaKrPGoI/UbwlezY5yJWIZY3XErc8szt0AF8Wj+/nw7pZvJneMeVJUK4Ui Nw5lSFamsas6lvV+edprHgcCSE0yclEqT/M/8BwF/N9schPkdFw7E2PFaAnEYkqWe0XUZ5b04KbBe nvw5L5U0kaYKwuY//3R5nxzgvAOBoaKuThoaGYTBzyThC5uvCQrcjPoVCQRoG8iQNNhe1gVb/xnfW PqDeynMUZnshHA==; Received: from 91-160-117-201.subs.proxad.net ([91.160.117.201]:59330 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oD92O-0002CS-Iw; Sun, 17 Jul 2022 14:30:45 -0400 From: Ludovic =?UTF-8?Q?Court=C3=A8s?= References: <20220702134201.3cf338e1@sybil.lepiller.eu> Date: Sun, 17 Jul 2022 20:30:38 +0200 In-Reply-To: <20220702134201.3cf338e1@sybil.lepiller.eu> (Julien Lepiller's message of "Sat, 2 Jul 2022 13:42:01 +0200") Message-ID: <87lesr4mnl.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.1 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -2.3 (--) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Saluton! :-) Julien Lepiller skribis: > From cd89e04ea72c18d59a01baccc9311b5070c845a4 Mon Sep 17 00:00:00 2001 > From: Julien Lepiller > 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. If it works for both of you, I=E2=80=99d say go for it! Ludo=E2=80=99. From unknown Sun Aug 10 16:47:03 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Julien Lepiller Subject: bug#56356: closed (Re: bug#56356: [WIP PATCH] gnu: dedukti: Update to 1.7.) Message-ID: References: <20221103140739.0b38781e@sybil.lepiller.eu> <20220702134201.3cf338e1@sybil.lepiller.eu> X-Gnu-PR-Message: they-closed 56356 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 56356@debbugs.gnu.org Date: Thu, 03 Nov 2022 13:08:03 +0000 Content-Type: multipart/mixed; boundary="----------=_1667480883-20939-1" This is a multi-part message in MIME format... ------------=_1667480883-20939-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #56356: [WIP PATCH] gnu: dedukti: Update to 1.7. which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 56356@debbugs.gnu.org. --=20 56356: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D56356 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1667480883-20939-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 56356-done) by debbugs.gnu.org; 3 Nov 2022 13:07:50 +0000 Received: from localhost ([127.0.0.1]:48335 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oqZwk-0005Qw-9d for submit@debbugs.gnu.org; Thu, 03 Nov 2022 09:07:50 -0400 Received: from lepiller.eu ([89.234.186.109]:54668) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oqZwg-0005Qj-CA for 56356-done@debbugs.gnu.org; Thu, 03 Nov 2022 09:07:49 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 640ed379; Thu, 3 Nov 2022 13:07:42 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:message-id:in-reply-to:references:mime-version :content-type:content-transfer-encoding; s=dkim; bh=kmJ6V4N4Rf3e xWIq4pzGpTg/bR0n/nxGnKVjIZx+pM8=; b=Xs1ymRsTi7b7qQ57a8T6C63HllGQ +hwqceSiwe5S7bXduNdXLd//xBASnOTVppT4NebWnkvAHgIvySGI60XbNYGJf9iY Gc+LTA8GHgKqdZMemqTGFIoE7w4thcfauNfPJTSkoagoVSwItaB4aMY6ySyYiCMS xovKOQmPW54b+cOjbwPMUCojmNXr8Q6ponSRB0NgGq2l/XD61mAivuf1M1+H4/LK Y/P/cKA0sXn2mvtYEMmrHKTBCrJ3vJnbkUt+k3Amw4p5SIXNv6lSTTZ4YbaEH0nu PYkkoSdqGtIi9m5E6n30IVmfEoQ+rfmzjEn+Yh331x+CYjnDRgojA0jZsg== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 31d5298a (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); Thu, 3 Nov 2022 13:07:42 +0000 (UTC) Date: Thu, 3 Nov 2022 14:07:39 +0100 From: Julien Lepiller To: Ludovic =?UTF-8?B?Q291cnTDqHM=?= Subject: Re: bug#56356: [WIP PATCH] gnu: dedukti: Update to 1.7. Message-ID: <20221103140739.0b38781e@sybil.lepiller.eu> In-Reply-To: <87lesr4mnl.fsf@gnu.org> References: <20220702134201.3cf338e1@sybil.lepiller.eu> <87lesr4mnl.fsf@gnu.org> X-Mailer: Claws Mail 4.1.0 (GTK 3.24.30; x86_64-pc-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 56356-done Cc: Gabriel Hondet , 56356-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Pushed to master as e2802132e36ea8157da1c1c06217e4561b6cd79f, thanks! Le Sun, 17 Jul 2022 20:30:38 +0200, Ludovic Court=C3=A8s a =C3=A9crit : > Saluton! :-) >=20 > Julien Lepiller skribis: >=20 > > From cd89e04ea72c18d59a01baccc9311b5070c845a4 Mon Sep 17 00:00:00 > > 2001 From: Julien Lepiller > > 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. =20 >=20 > If it works for both of you, I=E2=80=99d say go for it! >=20 > Ludo=E2=80=99. ------------=_1667480883-20939-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit 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 ) id 1o7bW1-0001ee-DE for submit@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 ) id 1o7bVz-0001eW-9g for submit@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 ) id 1o7bVx-0004vA-Gb for guix-patches@gnu.org; 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 ) id 1o7bVq-0000os-MC for guix-patches@gnu.org; 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 To: guix-patches@gnu.org Subject: [WIP PATCH] gnu: dedukti: Update to 1.7. Message-ID: <20220702134201.3cf338e1@sybil.lepiller.eu> 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@lepiller.eu; 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-Debbugs-Envelope-To: submit Cc: Gabriel Hondet X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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 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-- ------------=_1667480883-20939-1--