Message ID | 20220702134201.3cf338e1@sybil.lepiller.eu |
---|---|
State | New |
Headers | show |
Series | [bug#56356,WIP] gnu: dedukti: Update to 1.7. | expand |
Context | Check | Description |
---|---|---|
cbaines/comparison | success | View comparision |
cbaines/git branch | success | View Git branch |
cbaines/applying patch | fail | View Laminar job |
cbaines/issue | success | View issue |
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
Saluton! :-) Julien Lepiller <julien@lepiller.eu> skribis: > From cd89e04ea72c18d59a01baccc9311b5070c845a4 Mon Sep 17 00:00:00 2001 > From: Julien Lepiller <julien@lepiller.eu> > 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’d say go for it! Ludo’.
Pushed to master as e2802132e36ea8157da1c1c06217e4561b6cd79f, thanks! Le Sun, 17 Jul 2022 20:30:38 +0200, Ludovic Courtès <ludo@gnu.org> a écrit : > Saluton! :-) > > Julien Lepiller <julien@lepiller.eu> skribis: > > > From cd89e04ea72c18d59a01baccc9311b5070c845a4 Mon Sep 17 00:00:00 > > 2001 From: Julien Lepiller <julien@lepiller.eu> > > 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’d say go for it! > > Ludo’.
From cd89e04ea72c18d59a01baccc9311b5070c845a4 Mon Sep 17 00:00:00 2001 From: Julien Lepiller <julien@lepiller.eu> 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 = (.*)$") - (string-append "BINDIR = " #$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 λΠ-calculus modulo theory, an extension of the λ-calculus") (description "Dedukti is a proof-checker for the λΠ-calculus modulo -- 2.36.1