GNU bug report logs - #51896
[PATCH] gnu: Add coq-semantics.

Previous Next

Package: guix-patches;

Reported by: zimoun <zimon.toutoune <at> gmail.com>

Date: Tue, 16 Nov 2021 18:00:02 UTC

Severity: normal

Tags: patch

Done: Julien Lepiller <julien <at> lepiller.eu>

Bug is archived. No further changes may be made.

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 51896 in the body.
You can then email your comments to 51896 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to julien <at> lepiller.eu, guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:00:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to zimoun <zimon.toutoune <at> gmail.com>:
New bug report received and forwarded. Copy sent to julien <at> lepiller.eu, guix-patches <at> gnu.org. (Tue, 16 Nov 2021 18:00:02 GMT) Full text and rfc822 format available.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: guix-patches <at> gnu.org
Cc: zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH] gnu: Add coq-semantics.
Date: Tue, 16 Nov 2021 18:59:36 +0100
* gnu/packages/coq.scm (coq-semantics): New variable.
---
 gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index dccb9bea4c..ca9335302f 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -7,6 +7,7 @@
 ;;; Copyright © 2020 raingloom <raingloom <at> riseup.net>
 ;;; Copyright © 2020 Robin Green <greenrd <at> greenrd.org>
 ;;; Copyright © 2021 Xinglu Chen <public <at> yoctocell.xyz>
+;;; Copyright © 2021 Simon Tournier <zimon.toutoune <at> gmail.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -573,6 +574,59 @@ (define-public coq-equations
 kernel.")
     (license license:lgpl2.1)))
 
+(define-public coq-semantics
+  (package
+    (name "coq-semantics")
+    (version "8.13.0")
+    (source
+      (origin
+        (method git-fetch)
+        (uri (git-reference
+              (url "https://github.com/coq-community/semantics")
+              (commit (string-append "v" version))))
+        (file-name (git-file-name name version))
+        (sha256
+         (base32
+          "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("coq" ,coq)
+       ("ocaml" ,ocaml)
+       ("ocamlbuild" ,ocamlbuild)
+       ("ocaml-findlib" ,ocaml-findlib)))
+    (inputs
+     `(("ocaml-num" ,ocaml-num)))
+    (arguments
+     `(#:tests? #f                      ;included in Makefile
+       #:phases
+       (modify-phases %standard-phases
+         (add-after 'unpack 'fix-ocaml-Big_int
+           (lambda _
+             (substitute* "Makefile.coq.local"
+               ;; Num has part of OCaml and now external
+               (("-libs nums") "-use-ocamlfind -pkg num -libs num"))))
+         (delete 'configure)
+         (replace 'install
+           (lambda* (#:key outputs #:allow-other-keys)
+             (invoke "make"
+                     (string-append "COQLIB=" (assoc-ref outputs "out")
+                                    "/lib/coq/")
+                     "install"))))))
+    (home-page "https://github.com/coq-community/semantics")
+    (synopsis "Survey of semantics styles")
+    (description
+     "This package provides a survey of programming language semantics styles,
+from natural semantics through structural operational, axiomatic, and
+denotational semantics, for a miniature example of an imperative programming
+language.  Their encoding, the proofs of equivalence of different styles,
+abstract interpretation, and the proof of soundess obtained from axiomatic
+semantics or abstract interpretation is done in Coq.  The tools can be run
+inside Coq, thus making them available for proof by reflection.  Code can also
+be extracted and connected to a yacc-based parser, thanks to the use of a
+functor parameterized by a module type of strings.  A hand-written parser is
+also provided in Coq, without associated proofs.")
+    (license license:expat)))
+
 (define-public coq-stdpp
   (package
     (name "coq-stdpp")

base-commit: 122396075f12b013b6bde56dafb895587b95bc9d
-- 
2.32.0





Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:08:02 GMT) Full text and rfc822 format available.

Message #8 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: debbugs-submit <at> debbugs.gnu.org, zimoun <zimon.toutoune <at> gmail.com>,
 51896 <at> debbugs.gnu.org
Subject: Re: [bug#51896] [PATCH] gnu: Add coq-semantics.
Date: Tue, 16 Nov 2021 13:07:14 -0500
 

Le 16 novembre 2021 12:59:36 GMT-05:00, zimoun <zimon.toutoune <at> gmail.com> a écrit :
>* gnu/packages/coq.scm (coq-semantics): New variable.
>---
> gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 54 insertions(+)
>
>diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>index dccb9bea4c..ca9335302f 100644
>--- a/gnu/packages/coq.scm
>+++ b/gnu/packages/coq.scm
>@@ -7,6 +7,7 @@
> ;;; Copyright © 2020 raingloom <raingloom <at> riseup.net>
> ;;; Copyright © 2020 Robin Green <greenrd <at> greenrd.org>
> ;;; Copyright © 2021 Xinglu Chen <public <at> yoctocell.xyz>
>+;;; Copyright © 2021 Simon Tournier <zimon.toutoune <at> gmail.com>
> ;;;
> ;;; This file is part of GNU Guix.
> ;;;
>@@ -573,6 +574,59 @@ (define-public coq-equations
> kernel.")
>     (license license:lgpl2.1)))
> 
>+(define-public coq-semantics
>+  (package
>+    (name "coq-semantics")
>+    (version "8.13.0")
>+    (source
>+      (origin
>+        (method git-fetch)
>+        (uri (git-reference
>+              (url "https://github.com/coq-community/semantics")
>+              (commit (string-append "v" version))))
>+        (file-name (git-file-name name version))
>+        (sha256
>+         (base32
>+          "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
>+    (build-system gnu-build-system)
>+    (native-inputs
>+     `(("coq" ,coq)
>+       ("ocaml" ,ocaml)
>+       ("ocamlbuild" ,ocamlbuild)
>+       ("ocaml-findlib" ,ocaml-findlib)))
>+    (inputs
>+     `(("ocaml-num" ,ocaml-num)))
>+    (arguments
>+     `(#:tests? #f                      ;included in Makefile

You mean it's run at the same time as "make"?

>+       #:phases
>+       (modify-phases %standard-phases
>+         (add-after 'unpack 'fix-ocaml-Big_int
>+           (lambda _
>+             (substitute* "Makefile.coq.local"
>+               ;; Num has part of OCaml and now external

was?

>+               (("-libs nums") "-use-ocamlfind -pkg num -libs num"))))

Should this instead be in a snippet in the origin record?

>+         (delete 'configure)
>+         (replace 'install
>+           (lambda* (#:key outputs #:allow-other-keys)
>+             (invoke "make"
>+                     (string-append "COQLIB=" (assoc-ref outputs "out")
>+                                    "/lib/coq/")
>+                     "install"))))))

Would it make sense to have it in #:make-flags?

>+    (home-page "https://github.com/coq-community/semantics")
>+    (synopsis "Survey of semantics styles")
>+    (description
>+     "This package provides a survey of programming language semantics styles,
>+from natural semantics through structural operational, axiomatic, and
>+denotational semantics, for a miniature example of an imperative programming
>+language.  Their encoding, the proofs of equivalence of different styles,
>+abstract interpretation, and the proof of soundess obtained from axiomatic
>+semantics or abstract interpretation is done in Coq.  The tools can be run
>+inside Coq, thus making them available for proof by reflection.  Code can also
>+be extracted and connected to a yacc-based parser, thanks to the use of a
>+functor parameterized by a module type of strings.  A hand-written parser is
>+also provided in Coq, without associated proofs.")
>+    (license license:expat)))
>+
> (define-public coq-stdpp
>   (package
>     (name "coq-stdpp")
>
>base-commit: 122396075f12b013b6bde56dafb895587b95bc9d




Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:15:02 GMT) Full text and rfc822 format available.

Message #11 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 51896 <at> debbugs.gnu.org, debbugs-submit <at> debbugs.gnu.org
Subject: Re: [bug#51896] [PATCH] gnu: Add coq-semantics.
Date: Tue, 16 Nov 2021 19:13:56 +0100
Re,

On Tue, 16 Nov 2021 at 19:07, Julien Lepiller <julien <at> lepiller.eu> wrote:

> >+         (replace 'install
> >+           (lambda* (#:key outputs #:allow-other-keys)
> >+             (invoke "make"
> >+                     (string-append "COQLIB=" (assoc-ref outputs "out")
> >+                                    "/lib/coq/")
> >+                     "install"))))))
>
> Would it make sense to have it in #:make-flags?

I did the same way as other packages.  That's fine to correct all the
others, WDYT?


Cheers,
simon




Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:26:02 GMT) Full text and rfc822 format available.

Message #14 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 51896 <at> debbugs.gnu.org, debbugs-submit <at> debbugs.gnu.org
Subject: Re: [bug#51896] [PATCH] gnu: Add coq-semantics.
Date: Tue, 16 Nov 2021 13:24:56 -0500

Le 16 novembre 2021 13:13:56 GMT-05:00, zimoun <zimon.toutoune <at> gmail.com> a écrit :
>Re,
>
>On Tue, 16 Nov 2021 at 19:07, Julien Lepiller <julien <at> lepiller.eu> wrote:
>
>> >+         (replace 'install
>> >+           (lambda* (#:key outputs #:allow-other-keys)
>> >+             (invoke "make"
>> >+                     (string-append "COQLIB=" (assoc-ref outputs "out")
>> >+                                    "/lib/coq/")
>> >+                     "install"))))))
>>
>> Would it make sense to have it in #:make-flags?
>
>I did the same way as other packages.  That's fine to correct all the
>others, WDYT?

If it works yes, but in a separate patch :)

>
>Cheers,
>simon




Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:53:02 GMT) Full text and rfc822 format available.

Message #17 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51896 <at> debbugs.gnu.org
Cc: julien <at> lepiller.eu, zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH v2 1/5] gnu: Add coq-semantics.
Date: Tue, 16 Nov 2021 19:51:50 +0100
* gnu/packages/coq.scm (coq-semantics): New variable.
---
 gnu/packages/coq.scm | 51 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index dccb9bea4c..322bdb126e 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -7,6 +7,7 @@
 ;;; Copyright © 2020 raingloom <raingloom <at> riseup.net>
 ;;; Copyright © 2020 Robin Green <greenrd <at> greenrd.org>
 ;;; Copyright © 2021 Xinglu Chen <public <at> yoctocell.xyz>
+;;; Copyright © 2021 Simon Tournier <zimon.toutoune <at> gmail.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -573,6 +574,56 @@ (define-public coq-equations
 kernel.")
     (license license:lgpl2.1)))
 
+(define-public coq-semantics
+  (package
+    (name "coq-semantics")
+    (version "8.13.0")
+    (source
+      (origin
+        (method git-fetch)
+        (uri (git-reference
+              (url "https://github.com/coq-community/semantics")
+              (commit (string-append "v" version))))
+        (modules '((guix build utils)))
+        (snippet
+         '(substitute* "Makefile.coq.local"
+            ;; Num was part of OCaml and now external
+            (("-libs nums") "-use-ocamlfind -pkg num -libs num")))
+        (file-name (git-file-name name version))
+        (sha256
+         (base32
+          "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("coq" ,coq)
+       ("ocaml" ,ocaml)
+       ("ocamlbuild" ,ocamlbuild)
+       ("ocaml-findlib" ,ocaml-findlib)))
+    (inputs
+     `(("ocaml-num" ,ocaml-num)))
+    (arguments
+     `(#:tests? #f                      ;included in Makefile
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (assoc-ref %outputs "out")
+                                         "/lib/coq/user-contrib"))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure))))
+    (home-page "https://github.com/coq-community/semantics")
+    (synopsis "Survey of semantics styles")
+    (description
+     "This package provides a survey of programming language semantics styles,
+from natural semantics through structural operational, axiomatic, and
+denotational semantics, for a miniature example of an imperative programming
+language.  Their encoding, the proofs of equivalence of different styles,
+abstract interpretation, and the proof of soundess obtained from axiomatic
+semantics or abstract interpretation is done in Coq.  The tools can be run
+inside Coq, thus making them available for proof by reflection.  Code can also
+be extracted and connected to a yacc-based parser, thanks to the use of a
+functor parameterized by a module type of strings.  A hand-written parser is
+also provided in Coq, without associated proofs.")
+    (license license:expat)))
+
 (define-public coq-stdpp
   (package
     (name "coq-stdpp")

base-commit: 122396075f12b013b6bde56dafb895587b95bc9d
-- 
2.32.0





Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:53:02 GMT) Full text and rfc822 format available.

Message #20 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51896 <at> debbugs.gnu.org
Cc: julien <at> lepiller.eu, zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH v2 2/5] gnu: coq-mathcomp: Adjust '#:make-flags'.
Date: Tue, 16 Nov 2021 19:51:51 +0100
* gnu/packages/coq.scm (coq-mathcomp)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
 gnu/packages/coq.scm | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 322bdb126e..602a2d305d 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -326,17 +326,14 @@ (define-public coq-mathcomp
        ("coq" ,coq)))
     (arguments
      `(#:tests? #f ; No tests.
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (assoc-ref %outputs "out")
+                                         "/lib/coq/user-contrib"))
        #:phases
        (modify-phases %standard-phases
          (delete 'configure)
          (add-before 'build 'chdir
-           (lambda _ (chdir "mathcomp") #t))
-         (replace 'install
-           (lambda* (#:key outputs #:allow-other-keys)
-             (invoke "make" "-f" "Makefile.coq"
-                     (string-append "COQLIB=" (assoc-ref outputs "out")
-                                    "/lib/coq/")
-                     "install"))))))
+           (lambda _ (chdir "mathcomp") #t)))))
     (home-page "https://math-comp.github.io/")
     (synopsis "Mathematical Components for Coq")
     (description "Mathematical Components for Coq has its origins in the formal
-- 
2.32.0





Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:53:03 GMT) Full text and rfc822 format available.

Message #23 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51896 <at> debbugs.gnu.org
Cc: julien <at> lepiller.eu, zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH v2 3/5] gnu: coq-autosubst: Adjust '#:make-flags'.
Date: Tue, 16 Nov 2021 19:51:52 +0100
* gnu/packages/coq.scm (coq-autosubst)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
 gnu/packages/coq.scm | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 602a2d305d..fc739a0475 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -502,16 +502,12 @@ (define-public coq-autosubst
       (build-system gnu-build-system)
       (arguments
        `(#:tests? #f
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (assoc-ref %outputs "out")
+                                         "/lib/coq/user-contrib"))
          #:phases
          (modify-phases %standard-phases
-           (delete 'configure)
-           (replace 'install
-             (lambda* (#:key outputs #:allow-other-keys)
-               (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
-               (invoke "make"
-                       (string-append "COQLIB=" (assoc-ref outputs "out")
-                                      "/lib/coq/")
-                       "install"))))))
+           (delete 'configure))))
       (native-inputs
        `(("coq" ,coq)))
       (home-page "https://www.ps.uni-saarland.de/autosubst/")
-- 
2.32.0





Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:53:03 GMT) Full text and rfc822 format available.

Message #26 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51896 <at> debbugs.gnu.org
Cc: julien <at> lepiller.eu, zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH v2 5/5] gnu: coq-stdpp: Adjust '#:make-flags'.
Date: Tue, 16 Nov 2021 19:51:54 +0100
* gnu/packages/coq.scm (coq-stdpp)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
 gnu/packages/coq.scm | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index aeba0eb5da..a0579f8869 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -633,15 +633,12 @@ (define-public coq-stdpp
      `(("coq" ,coq)))
     (arguments
      `(#:tests? #f ; Tests are executed during build phase.
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (assoc-ref %outputs "out")
+                                         "/lib/coq/user-contrib"))
        #:phases
        (modify-phases %standard-phases
-         (delete 'configure)
-         (replace 'install
-           (lambda* (#:key outputs #:allow-other-keys)
-             (invoke "make"
-                     (string-append "COQLIB=" (assoc-ref outputs "out")
-                                    "/lib/coq/")
-                     "install"))))))
+         (delete 'configure))))
     (description "This project contains an extended \"Standard Library\" for
 Coq called coq-std++.  The key features are:
 @itemize
-- 
2.32.0





Information forwarded to guix-patches <at> gnu.org:
bug#51896; Package guix-patches. (Tue, 16 Nov 2021 18:53:04 GMT) Full text and rfc822 format available.

Message #29 received at 51896 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51896 <at> debbugs.gnu.org
Cc: julien <at> lepiller.eu, zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH v2 4/5] gnu: coq-equations: Adjust '#:make-flags'.
Date: Tue, 16 Nov 2021 19:51:53 +0100
* gnu/packages/coq.scm (coq-equations)[arguments]<#:make-flags>: Set install
destination.
<#:phases>: Remove replace 'install.
---
 gnu/packages/coq.scm | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fc739a0475..aeba0eb5da 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -547,17 +547,14 @@ (define-public coq-equations
      `(("ocaml-zarith" ,ocaml-zarith)))
     (arguments
      `(#:test-target "test-suite"
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (assoc-ref %outputs "out")
+                                         "/lib/coq/user-contrib"))
        #:phases
        (modify-phases %standard-phases
          (replace 'configure
            (lambda* (#:key outputs #:allow-other-keys)
-             (invoke "sh" "./configure.sh")))
-         (replace 'install
-           (lambda* (#:key outputs #:allow-other-keys)
-             (invoke "make"
-                     (string-append "COQLIB=" (assoc-ref outputs "out")
-                                    "/lib/coq/")
-                     "install"))))))
+             (invoke "sh" "./configure.sh"))))))
     (home-page "https://mattam82.github.io/Coq-Equations/")
     (synopsis "Function definition plugin for Coq")
     (description "Equations provides a notation for writing programs
-- 
2.32.0





Reply sent to Julien Lepiller <julien <at> lepiller.eu>:
You have taken responsibility. (Thu, 18 Nov 2021 03:36:02 GMT) Full text and rfc822 format available.

Notification sent to zimoun <zimon.toutoune <at> gmail.com>:
bug acknowledged by developer. (Thu, 18 Nov 2021 03:36:02 GMT) Full text and rfc822 format available.

Message #34 received at 51896-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 51896-done <at> debbugs.gnu.org
Subject: Re: [bug#51896] [PATCH] gnu: Add coq-semantics.
Date: Thu, 18 Nov 2021 04:35:25 +0100
Pushed v2 to master as 2d60af4d6d486591c5a6981659d1771b7c69781a to
7537ec816ffe0aaa6677c53604ac12fe9d9ca250. Thanks!




bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Thu, 16 Dec 2021 12:24:12 GMT) Full text and rfc822 format available.

This bug report was last modified 2 years and 93 days ago.

Previous Next


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