[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Jean-Pierre De Jesus DIAZ]

This package updates Frama-C to 28.1 and its dependencies.  An error was
fixed by moving the ocaml-lablgtk3-sourceview3 native-inputs to
propagated-inputs as it was needed by frama-c to properly perform syntax
highlighting on C code.

Also the why3 package was updated and a couple of propagated-inputs
inputs were added to enable extra features and also to enable the
integrated IDE (also using ocaml-lablgtk3-sourceview3).

Jean-Pierre De Jesus DIAZ (7):
  gnu: ocaml-lablgtk3-sourceview3: Fix inputs.
  gnu: coq-flocq: Update to 4.1.4.
  gnu: why3: Update to 1.7.2.
  gnu: why3: Use new style.
  gnu: why3: Enable extra features.
  gnu: Add ocaml-unionfind.
  gnu: frama-c: Update to 28.1.

 gnu/packages/coq.scm   |  5 +--
 gnu/packages/maths.scm | 81 ++++++++++++++++++++++++------------------
 gnu/packages/ocaml.scm | 28 +++++++++++++--
 3 files changed, 75 insertions(+), 39 deletions(-)


base-commit: e5c130c0f90a7dacc8d223eee494a1b1105dd94a
-- 
2.41.0

[bug#70567] [PATCH 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/ocaml.scm (ocaml-lablgtk3-sourceview3): Move gtksourceview-3 from
native-inputs to propagated-inputs.  Remove native-inputs and use
inherited inputs instead.

Change-Id: I2b242343bdace17ee3e992ce71f4e49b3c375e15
---
 gnu/packages/ocaml.scm | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 7fad276b4e..920ccdcf36 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com>
 ;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;; Copyright © 2023 Csepp <raingloom@riseup.net>
-;;; Copyright © 2023 Foundation Devices, Inc. <hello@foundationdevices.com>
+;;; Copyright © 2023,2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;; Copyright © 2023 Arnaud DABY-SEESARAM <ds-ac@nanein.fr>
 ;;; Copyright © 2024 Sören Tempel <soeren@soeren-tempel.net>
 ;;;
@@ -8570,8 +8570,7 @@ (define-public ocaml-lablgtk3-sourceview3
   (package
     (inherit lablgtk3)
     (name "ocaml-lablgtk3-sourceview3")
-    (propagated-inputs (list lablgtk3))
-    (native-inputs (list gtksourceview-3 pkg-config))
+    (propagated-inputs (list gtksourceview-3 lablgtk3))
     (arguments
      `(#:package "lablgtk3-sourceview3"))
     (synopsis "OCaml interface to GTK+ gtksourceview library")
-- 
2.41.0

[bug#70567] [PATCH 2/7] gnu: coq-flocq: Update to 4.1.4.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/coq.scm (coq-flocq): Update to 4.1.4.

Change-Id: Ia2bf4bccad712a7bfa5427ef26ad93d39f1fc6e0
---
 gnu/packages/coq.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 105b942ad3..11d6b034f1 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -9,6 +9,7 @@
 ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
 ;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
 ;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
+;;; Copyright © 2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -217,7 +218,7 @@ (define-public proof-general
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "4.1.1")
+    (version "4.1.4")
     (source
      (origin
        (method git-fetch)
@@ -227,7 +228,7 @@ (define-public coq-flocq
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "01x38w58j95ba9679vpb5wv4bvfnrapd5dzjqlyz8k7i8a9sfqn0"))))
+         "08vrh0h909vmam1b4gfrvcmamnhmr5g0x79zx98hn7cx0vdwysh7"))))
     (build-system gnu-build-system)
     (native-inputs
      (list autoconf automake ocaml which coq))
-- 
2.41.0

[bug#70567] [PATCH 3/7] gnu: why3: Update to 1.7.2.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Update to 1.7.2.

Change-Id: Ie5a40b31c2c418fafbdbba52e875ac25a26fb12b
---
 gnu/packages/maths.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 361f2f7b68..5c7f3102f3 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -63,6 +63,7 @@
 ;;; Copyright © 2023 Jake Leporte <jakeleporte@outlook.com>
 ;;; Copyright © 2023 Camilo Q.S. (Distopico) <distopico@riseup.net>
 ;;; Copyright © 2023 David Elsing <david.elsing@posteo.net>
+;;; Copyright © 2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -9388,7 +9389,7 @@ (define-public numdiff
 (define-public why3
   (package
     (name "why3")
-    (version "1.6.0")
+    (version "1.7.2")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -9397,7 +9398,7 @@ (define-public why3
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0k3y98xzhrl44vwzq2m6k4nrllrwp3ll69lc2gfl8d77w0wg7gkp"))))
+                "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
     (native-inputs
      (list autoconf automake coq ocaml which))
-- 
2.41.0

[bug#70567] [PATCH 4/7] gnu: why3: Use new style.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Use new style and move arguments
above input fields.

Change-Id: Ia9cb04cafe426d7f20c5efb10ca540572dbd3be9
---
 gnu/packages/maths.scm | 63 +++++++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 29 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5c7f3102f3..57f750accc 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9400,36 +9400,41 @@ (define-public why3
                (base32
                 "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
-    (native-inputs
-     (list autoconf automake coq ocaml which))
-    (propagated-inputs
-     (list camlzip ocaml-graph ocaml-menhir ocaml-num ocaml-zarith))
-    (inputs
-     (list coq-flocq emacs-minimal zlib))
     (arguments
-     `(#:phases
-       (modify-phases %standard-phases
-         (add-before 'configure 'bootstrap
-           (lambda _
-             (invoke "./autogen.sh")
-             (setenv "CONFIG_SHELL" (which "sh"))
-             (substitute* "configure"
-               (("#! /bin/sh") (string-append "#!" (which "sh")))
-               ;; find ocaml-num in the correct directory
-               (("\\$DIR/nums.cma") "$DIR/num.cma")
-               (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))
-             #t))
-         (add-after 'configure 'fix-makefile
-           (lambda _
-             (substitute* "Makefile"
-               ;; find ocaml-num in the correct directory
-               (("site-lib/num") "site-lib"))
-             #t))
-        (add-after 'install 'install-lib
-          (lambda _
-            (invoke "make" "byte")
-            (invoke "make" "install-lib")
-            #t)))))
+     (list #:phases
+           #~(modify-phases %standard-phases
+               (add-before 'configure 'bootstrap
+                 (lambda _
+                   (invoke "./autogen.sh")
+                   (setenv "CONFIG_SHELL" (which "sh"))
+                   (substitute* "configure"
+                     (("#! /bin/sh") (string-append "#!" (which "sh")))
+                     ;; find ocaml-num in the correct directory
+                     (("\\$DIR/nums.cma") "$DIR/num.cma")
+                     (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))))
+               (add-after 'configure 'fix-makefile
+                 (lambda _
+                   (substitute* "Makefile"
+                     ;; find ocaml-num in the correct directory
+                     (("site-lib/num") "site-lib"))))
+            (add-after 'install 'install-lib
+              (lambda _
+                (invoke "make" "byte")
+                (invoke "make" "install-lib"))))))
+    (native-inputs (list autoconf
+                         automake
+                         coq
+                         ocaml
+                         ocaml-findlib
+                         which))
+    (propagated-inputs (list camlzip
+                             ocaml-graph
+                             ocaml-menhir
+                             ocaml-num
+                             ocaml-zarith))
+    (inputs (list coq-flocq
+                  emacs-minimal
+                  zlib))
     (home-page "https://why3.lri.fr")
     (synopsis "Deductive program verification")
     (description "Why3 provides a language for specification and programming,
-- 
2.41.0

[bug#70567] [PATCH 5/7] gnu: why3: Enable extra features.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3) <propagated-inputs>: Add
ocaml-ppx-deriving, ocaml-ppx-sexp-conv, ocaml-re and ocaml-sexplib to
enable extra features.

Change-Id: Ia3b66ac08cc25097967c6e18f2193601fb748cac
---
 gnu/packages/maths.scm | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 57f750accc..9bf2f64cbb 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9428,9 +9428,15 @@ (define-public why3
                          ocaml-findlib
                          which))
     (propagated-inputs (list camlzip
+                             lablgtk3
                              ocaml-graph
+                             ocaml-lablgtk3-sourceview3
                              ocaml-menhir
+                             ocaml-ppx-deriving
+                             ocaml-ppx-sexp-conv
                              ocaml-num
+                             ocaml-re
+                             ocaml-sexplib
                              ocaml-zarith))
     (inputs (list coq-flocq
                   emacs-minimal
-- 
2.41.0

[bug#70567] [PATCH 6/7] gnu: Add ocaml-unionfind.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/ocaml.scm (ocaml-unionfind): New variable.

Change-Id: Ib101e67576c000dad1d4a73d008ca0376e7da95a
---
 gnu/packages/ocaml.scm | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 920ccdcf36..921b669a8e 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3186,6 +3186,29 @@ (define ocaml-eio-luv
 (define-public ocaml5.0-eio-luv
   (package-with-ocaml5.0 ocaml-eio-luv))
 
+(define-public ocaml-unionfind
+  (package
+    (name "ocaml-unionfind")
+    (version "20220122")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+              (url "https://gitlab.inria.fr/fpottier/unionfind")
+              (commit version)))
+       (sha256
+        (base32 "0hdh56rbg8vfjd61q09cbmh8l5wmry5ykivg7gsm0v5ckkb3531r"))))
+    (build-system dune-build-system)
+    (home-page "https://gitlab.inria.fr/fpottier/unionFind")
+    (synopsis "Union-find data structure")
+    (description "This package provides two union-find data structure
+implementations for OCaml.  Both implementations are based on disjoint sets
+forests, with path compression and linking-by-rank, so as to guarantee good
+asymptotic complexity: every operation requires a quasi-constant number of
+accesses to the store.")
+    ;; Version 2 only, with linking exception.
+    (license license:lgpl2.0)))
+
 (define-public ocaml-uring
   (package
     (name "ocaml-uring")
-- 
2.41.0

[bug#70567] [PATCH 7/7] gnu: frama-c: Update to 28.1.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (frama-c): Update to 28.1.

Change-Id: I0ce0d0a7db4d017ba1f5028e73c931ceb706fce5
---
 gnu/packages/maths.scm | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 9bf2f64cbb..abbf854f41 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9457,14 +9457,14 @@ (define-public why3
 (define-public frama-c
   (package
     (name "frama-c")
-    (version "27.1")
+    (version "28.1")
     (source (origin
               (method url-fetch)
               (uri (string-append "http://frama-c.com/download/frama-c-"
-                                  version "-Cobalt.tar.gz"))
+                                  version "-Nickel.tar.gz"))
               (sha256
                (base32
-                "1lirkvhf5m53d33l0aw5jzc1fyzkwx5fkgh9g71732d52r55f4sv"))))
+                "14zmwghwhcryvri7k91vc1yampvxvhg36vwjxf64d8kx7dsbq802"))))
     (build-system dune-build-system)
     (arguments
       `(#:phases
@@ -9487,6 +9487,7 @@ (define-public frama-c
                          ocaml-ppx-deriving-yojson
                          ocaml-ppx-deriving-yaml
                          ocaml-ppx-import
+                         ocaml-unionfind
                          why3))
     (native-inputs (list dune-site time ocaml-menhir ocaml-graph))
     (native-search-paths
-- 
2.41.0

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Julien Lepiller]

The whole series LGTM, though untested.

Le 25 avril 2024 15:08:40 GMT+02:00, Jean-Pierre De Jesus DIAZ <jean@foundation.xyz> a écrit :
>This package updates Frama-C to 28.1 and its dependencies.  An error was
>fixed by moving the ocaml-lablgtk3-sourceview3 native-inputs to
>propagated-inputs as it was needed by frama-c to properly perform syntax
>highlighting on C code.
>
>Also the why3 package was updated and a couple of propagated-inputs
>inputs were added to enable extra features and also to enable the
>integrated IDE (also using ocaml-lablgtk3-sourceview3).
>
>Jean-Pierre De Jesus DIAZ (7):
>  gnu: ocaml-lablgtk3-sourceview3: Fix inputs.
>  gnu: coq-flocq: Update to 4.1.4.
>  gnu: why3: Update to 1.7.2.
>  gnu: why3: Use new style.
>  gnu: why3: Enable extra features.
>  gnu: Add ocaml-unionfind.
>  gnu: frama-c: Update to 28.1.
>
> gnu/packages/coq.scm   |  5 +--
> gnu/packages/maths.scm | 81 ++++++++++++++++++++++++------------------
> gnu/packages/ocaml.scm | 28 +++++++++++++--
> 3 files changed, 75 insertions(+), 39 deletions(-)
>
>
>base-commit: e5c130c0f90a7dacc8d223eee494a1b1105dd94a

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Arnaud Daby-Seesaram via Guix-patches via]

[-- Attachment #1: Type: text/plain, Size: 856 bytes --]

Hi,

Thank you for these patches.  I confirm that the patches do apply, and
that packages build.

That said, I still experience an issue when trying to run frama-c.
I can enter a `guix shell frama-c` environment, but then:

- `frama-c --version` outputs "28.1 (Nickel)", as expected.
  
- `frama-c --help` errors out with the following error:
    | Unexpected error (The library "frama-c-alias.core" can't be found
    | in the search paths
    | "/gnu/store/psmc4940aa9bj23dddkglv0p2yhi05kn-ocaml-4.14.1/lib".).
  together with a backtrace.


Note: this issue is also present in Guix for frama-c version
      27.1 (Cobalt).


I am missing additional packages (maybe in another channel) which would
provide frama-c-* packages?


Orthogonal comment: should "http://" be replaced by "https://"?


Best regards,

-- 
Arnaud

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 857 bytes --]

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Jean-Pierre De Jesus Diaz]

Hi,

>That said, I still experience an issue when trying to run frama-c.
>I can enter a `guix shell frama-c` environment, but then:
>- `frama-c --version` outputs "28.1 (Nickel)", as expected.
>
>- `frama-c --help` errors out with the following error:
>    | Unexpected error (The library "frama-c-alias.core" can't be found
>    | in the search paths
>    | "/gnu/store/psmc4940aa9bj23dddkglv0p2yhi05kn-ocaml-4.14.1/lib".).
>  together with a backtrace.

This is due to a problem with OCaml packages and search paths.

See <https://issues.guix.gnu.org/69996>.

So running this should work: `guix shell frama-c ocaml -- frama-c --help'.

>Orthogonal comment: should "http://" be replaced by "https://"?

Shouldn't be an issue per se as Guix checks the hash of the
downloaded files to match but for privacy reasons should be on https
IMO.

Will do and I'll sent a v2.

On Thu, Apr 25, 2024 at 2:54 PM Arnaud Daby-Seesaram <ds-ac@nanein.fr> wrote:
>
> Hi,
>
> Thank you for these patches.  I confirm that the patches do apply, and
> that packages build.
>
> That said, I still experience an issue when trying to run frama-c.
> I can enter a `guix shell frama-c` environment, but then:
>
> - `frama-c --version` outputs "28.1 (Nickel)", as expected.
>
> - `frama-c --help` errors out with the following error:
>     | Unexpected error (The library "frama-c-alias.core" can't be found
>     | in the search paths
>     | "/gnu/store/psmc4940aa9bj23dddkglv0p2yhi05kn-ocaml-4.14.1/lib".).
>   together with a backtrace.
>
>
> Note: this issue is also present in Guix for frama-c version
>       27.1 (Cobalt).
>
>
> I am missing additional packages (maybe in another channel) which would
> provide frama-c-* packages?
>
>
> Orthogonal comment: should "http://" be replaced by "https://"?
>
>
> Best regards,
>
> --
> Arnaud

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Arnaud Daby-Seesaram via Guix-patches via]

[-- Attachment #1: Type: text/plain, Size: 468 bytes --]

> This is due to a problem with OCaml packages and search paths.
>
> See <https://issues.guix.gnu.org/69996>.

Thx for the link, I did not see Julien's answer on this issue.
I confirm than the issue disappears when I add ocaml :).


> Shouldn't be an issue per se as Guix checks the hash of the
> downloaded files to match
Agreed (+ there is a redirection http -> https in place).
> but for privacy reasons should be on https IMO.

Best,

-- 
Arnaud

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 857 bytes --]

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Julien Lepiller]

Le 25 avril 2024 16:54:34 GMT+02:00, Arnaud Daby-Seesaram via Guix-patches via <guix-patches@gnu.org> a écrit :
>Hi,
>
>Thank you for these patches.  I confirm that the patches do apply, and
>that packages build.
>
>That said, I still experience an issue when trying to run frama-c.
>I can enter a `guix shell frama-c` environment, but then:
>
>- `frama-c --version` outputs "28.1 (Nickel)", as expected.
>  
>- `frama-c --help` errors out with the following error:
>    | Unexpected error (The library "frama-c-alias.core" can't be found
>    | in the search paths
>    | "/gnu/store/psmc4940aa9bj23dddkglv0p2yhi05kn-ocaml-4.14.1/lib".).
>  together with a backtrace.
>
>
>Note: this issue is also present in Guix for frama-c version
>      27.1 (Cobalt).
>
>
>I am missing additional packages (maybe in another channel) which would
>provide frama-c-* packages?

Try with guix shell frama-c ocaml

>
>
>Orthogonal comment: should "http://" be replaced by "https://"?

If the website is available at https, yes

>
>
>Best regards,
>

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Jean-Pierre De Jesus Diaz]

Hi,

I've sent a v2 of the patches, it now uses https and fixed
ocaml-unionfind origin that didn't contain the file-name
field.

On Thu, Apr 25, 2024 at 3:24 PM Julien Lepiller <julien@lepiller.eu> wrote:
>
>
>
> Le 25 avril 2024 16:54:34 GMT+02:00, Arnaud Daby-Seesaram via Guix-patches via <guix-patches@gnu.org> a écrit :
> >Hi,
> >
> >Thank you for these patches.  I confirm that the patches do apply, and
> >that packages build.
> >
> >That said, I still experience an issue when trying to run frama-c.
> >I can enter a `guix shell frama-c` environment, but then:
> >
> >- `frama-c --version` outputs "28.1 (Nickel)", as expected.
> >
> >- `frama-c --help` errors out with the following error:
> >    | Unexpected error (The library "frama-c-alias.core" can't be found
> >    | in the search paths
> >    | "/gnu/store/psmc4940aa9bj23dddkglv0p2yhi05kn-ocaml-4.14.1/lib".).
> >  together with a backtrace.
> >
> >
> >Note: this issue is also present in Guix for frama-c version
> >      27.1 (Cobalt).
> >
> >
> >I am missing additional packages (maybe in another channel) which would
> >provide frama-c-* packages?
>
> Try with guix shell frama-c ocaml
>
> >
> >
> >Orthogonal comment: should "http://" be replaced by "https://"?
>
> If the website is available at https, yes
>
> >
> >
> >Best regards,
> >

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Andreas Enge]

Hello,

looking at what frama-c does, I am a bit puzzled: to me it has been put
into the wrong module, together with why3 just above it; unless you consider
informatics as a subset of mathematics, that is. In any case, these packages
do not seem to do computations of interest to an applied mathematician
(which is what most of maths.scm is about) or a pure mathematician (with
packages in algebra.scm).

Could they be moved to coq.scm? Or a more generic, maybe a new module
related to theorem proving and/or source code analysis? Maybe into a
renamed valgrind.scm?

Andreas

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Jean-Pierre De Jesus Diaz]

Hi,

>looking at what frama-c does, I am a bit puzzled: to me it has been put
>into the wrong module, together with why3 just above it; unless you consider
>informatics as a subset of mathematics, that is. In any case, these packages
>do not seem to do computations of interest to an applied mathematician
>(which is what most of maths.scm is about) or a pure mathematician (with
>packages in algebra.scm).

Agreed.

>Could they be moved to coq.scm? Or a more generic, maybe a new module
>related to theorem proving and/or source code analysis? Maybe into a
>renamed valgrind.scm?

I think it should be done but in a separate patch series as it would involve
moving quite a few things, maybe a formal-methods.scm module?

I think the coq.scm should be only for Coq as it contains it's own ecosystem.

On Thu, Apr 25, 2024 at 3:35 PM Andreas Enge <andreas@enge.fr> wrote:
>
> Hello,
>
> looking at what frama-c does, I am a bit puzzled: to me it has been put
> into the wrong module, together with why3 just above it; unless you consider
> informatics as a subset of mathematics, that is. In any case, these packages
> do not seem to do computations of interest to an applied mathematician
> (which is what most of maths.scm is about) or a pure mathematician (with
> packages in algebra.scm).
>
> Could they be moved to coq.scm? Or a more generic, maybe a new module
> related to theorem proving and/or source code analysis? Maybe into a
> renamed valgrind.scm?
>
> Andreas
>

[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Andreas Enge]

Am Fri, Apr 26, 2024 at 01:03:44PM +0000 schrieb Jean-Pierre De Jesus Diaz:
> >Could they be moved to coq.scm? Or a more generic, maybe a new module
> >related to theorem proving and/or source code analysis? Maybe into a
> >renamed valgrind.scm?
> I think it should be done but in a separate patch series as it would involve
> moving quite a few things, maybe a formal-methods.scm module?

Definitely, it should be done in a separate patch.

As to what the module should be called, I will let the specialists discuss
it among themselves :)

Andreas

[bug#70567] [PATCH v2 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/ocaml.scm (ocaml-lablgtk3-sourceview3): Move gtksourceview-3 from
native-inputs to propagated-inputs.  Remove native-inputs and use
inherited inputs instead.

Change-Id: I2b242343bdace17ee3e992ce71f4e49b3c375e15
---
 gnu/packages/ocaml.scm | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 7fad276b4e..920ccdcf36 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com>
 ;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;; Copyright © 2023 Csepp <raingloom@riseup.net>
-;;; Copyright © 2023 Foundation Devices, Inc. <hello@foundationdevices.com>
+;;; Copyright © 2023,2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;; Copyright © 2023 Arnaud DABY-SEESARAM <ds-ac@nanein.fr>
 ;;; Copyright © 2024 Sören Tempel <soeren@soeren-tempel.net>
 ;;;
@@ -8570,8 +8570,7 @@ (define-public ocaml-lablgtk3-sourceview3
   (package
     (inherit lablgtk3)
     (name "ocaml-lablgtk3-sourceview3")
-    (propagated-inputs (list lablgtk3))
-    (native-inputs (list gtksourceview-3 pkg-config))
+    (propagated-inputs (list gtksourceview-3 lablgtk3))
     (arguments
      `(#:package "lablgtk3-sourceview3"))
     (synopsis "OCaml interface to GTK+ gtksourceview library")

base-commit: e5c130c0f90a7dacc8d223eee494a1b1105dd94a
-- 
2.41.0

[bug#70567] [PATCH v2 2/7] gnu: coq-flocq: Update to 4.1.4.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/coq.scm (coq-flocq): Update to 4.1.4.

Change-Id: Ia2bf4bccad712a7bfa5427ef26ad93d39f1fc6e0
---
 gnu/packages/coq.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 105b942ad3..11d6b034f1 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -9,6 +9,7 @@
 ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
 ;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
 ;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
+;;; Copyright © 2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -217,7 +218,7 @@ (define-public proof-general
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "4.1.1")
+    (version "4.1.4")
     (source
      (origin
        (method git-fetch)
@@ -227,7 +228,7 @@ (define-public coq-flocq
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "01x38w58j95ba9679vpb5wv4bvfnrapd5dzjqlyz8k7i8a9sfqn0"))))
+         "08vrh0h909vmam1b4gfrvcmamnhmr5g0x79zx98hn7cx0vdwysh7"))))
     (build-system gnu-build-system)
     (native-inputs
      (list autoconf automake ocaml which coq))
-- 
2.41.0

[bug#70567] [PATCH v2 3/7] gnu: why3: Update to 1.7.2.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Update to 1.7.2.

Change-Id: Ie5a40b31c2c418fafbdbba52e875ac25a26fb12b
---
 gnu/packages/maths.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 361f2f7b68..5c7f3102f3 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -63,6 +63,7 @@
 ;;; Copyright © 2023 Jake Leporte <jakeleporte@outlook.com>
 ;;; Copyright © 2023 Camilo Q.S. (Distopico) <distopico@riseup.net>
 ;;; Copyright © 2023 David Elsing <david.elsing@posteo.net>
+;;; Copyright © 2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -9388,7 +9389,7 @@ (define-public numdiff
 (define-public why3
   (package
     (name "why3")
-    (version "1.6.0")
+    (version "1.7.2")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -9397,7 +9398,7 @@ (define-public why3
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0k3y98xzhrl44vwzq2m6k4nrllrwp3ll69lc2gfl8d77w0wg7gkp"))))
+                "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
     (native-inputs
      (list autoconf automake coq ocaml which))
-- 
2.41.0

[bug#70567] [PATCH v2 4/7] gnu: why3: Use new style.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Use new style and move arguments
above input fields.

Change-Id: Ia9cb04cafe426d7f20c5efb10ca540572dbd3be9
---
 gnu/packages/maths.scm | 63 +++++++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 29 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5c7f3102f3..57f750accc 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9400,36 +9400,41 @@ (define-public why3
                (base32
                 "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
-    (native-inputs
-     (list autoconf automake coq ocaml which))
-    (propagated-inputs
-     (list camlzip ocaml-graph ocaml-menhir ocaml-num ocaml-zarith))
-    (inputs
-     (list coq-flocq emacs-minimal zlib))
     (arguments
-     `(#:phases
-       (modify-phases %standard-phases
-         (add-before 'configure 'bootstrap
-           (lambda _
-             (invoke "./autogen.sh")
-             (setenv "CONFIG_SHELL" (which "sh"))
-             (substitute* "configure"
-               (("#! /bin/sh") (string-append "#!" (which "sh")))
-               ;; find ocaml-num in the correct directory
-               (("\\$DIR/nums.cma") "$DIR/num.cma")
-               (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))
-             #t))
-         (add-after 'configure 'fix-makefile
-           (lambda _
-             (substitute* "Makefile"
-               ;; find ocaml-num in the correct directory
-               (("site-lib/num") "site-lib"))
-             #t))
-        (add-after 'install 'install-lib
-          (lambda _
-            (invoke "make" "byte")
-            (invoke "make" "install-lib")
-            #t)))))
+     (list #:phases
+           #~(modify-phases %standard-phases
+               (add-before 'configure 'bootstrap
+                 (lambda _
+                   (invoke "./autogen.sh")
+                   (setenv "CONFIG_SHELL" (which "sh"))
+                   (substitute* "configure"
+                     (("#! /bin/sh") (string-append "#!" (which "sh")))
+                     ;; find ocaml-num in the correct directory
+                     (("\\$DIR/nums.cma") "$DIR/num.cma")
+                     (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))))
+               (add-after 'configure 'fix-makefile
+                 (lambda _
+                   (substitute* "Makefile"
+                     ;; find ocaml-num in the correct directory
+                     (("site-lib/num") "site-lib"))))
+            (add-after 'install 'install-lib
+              (lambda _
+                (invoke "make" "byte")
+                (invoke "make" "install-lib"))))))
+    (native-inputs (list autoconf
+                         automake
+                         coq
+                         ocaml
+                         ocaml-findlib
+                         which))
+    (propagated-inputs (list camlzip
+                             ocaml-graph
+                             ocaml-menhir
+                             ocaml-num
+                             ocaml-zarith))
+    (inputs (list coq-flocq
+                  emacs-minimal
+                  zlib))
     (home-page "https://why3.lri.fr")
     (synopsis "Deductive program verification")
     (description "Why3 provides a language for specification and programming,
-- 
2.41.0

[bug#70567] [PATCH v2 5/7] gnu: why3: Enable extra features.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3) <propagated-inputs>: Add
ocaml-ppx-deriving, ocaml-ppx-sexp-conv, ocaml-re and ocaml-sexplib to
enable extra features.

Change-Id: Ia3b66ac08cc25097967c6e18f2193601fb748cac
---
 gnu/packages/maths.scm | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 57f750accc..9bf2f64cbb 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9428,9 +9428,15 @@ (define-public why3
                          ocaml-findlib
                          which))
     (propagated-inputs (list camlzip
+                             lablgtk3
                              ocaml-graph
+                             ocaml-lablgtk3-sourceview3
                              ocaml-menhir
+                             ocaml-ppx-deriving
+                             ocaml-ppx-sexp-conv
                              ocaml-num
+                             ocaml-re
+                             ocaml-sexplib
                              ocaml-zarith))
     (inputs (list coq-flocq
                   emacs-minimal
-- 
2.41.0

[bug#70567] [PATCH v2 6/7] gnu: Add ocaml-unionfind.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/ocaml.scm (ocaml-unionfind): New variable.

Change-Id: Ib101e67576c000dad1d4a73d008ca0376e7da95a
---
 gnu/packages/ocaml.scm | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 920ccdcf36..26f5e4a9a9 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3186,6 +3186,30 @@ (define ocaml-eio-luv
 (define-public ocaml5.0-eio-luv
   (package-with-ocaml5.0 ocaml-eio-luv))
 
+(define-public ocaml-unionfind
+  (package
+    (name "ocaml-unionfind")
+    (version "20220122")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+              (url "https://gitlab.inria.fr/fpottier/unionfind")
+              (commit version)))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "0hdh56rbg8vfjd61q09cbmh8l5wmry5ykivg7gsm0v5ckkb3531r"))))
+    (build-system dune-build-system)
+    (home-page "https://gitlab.inria.fr/fpottier/unionFind")
+    (synopsis "Union-find data structure")
+    (description "This package provides two union-find data structure
+implementations for OCaml.  Both implementations are based on disjoint sets
+forests, with path compression and linking-by-rank, so as to guarantee good
+asymptotic complexity: every operation requires a quasi-constant number of
+accesses to the store.")
+    ;; Version 2 only, with linking exception.
+    (license license:lgpl2.0)))
+
 (define-public ocaml-uring
   (package
     (name "ocaml-uring")
-- 
2.41.0

[bug#70567] [PATCH v2 6/7] gnu: Add ocaml-unionfind.

[Ludovic Courtès]

Hi Jean-Pierre,

Jean-Pierre De Jesus DIAZ <jean@foundation.xyz> skribis:

> * gnu/packages/ocaml.scm (ocaml-unionfind): New variable.
>
> Change-Id: Ib101e67576c000dad1d4a73d008ca0376e7da95a

<https://qa.guix.gnu.org/issue/70567> reports a build failure of this
package on 32-bit platforms (armhf and i686):

--8<---------------cut here---------------start------------->8---
starting phase `check'
File "test/dune", line 2, characters 8-21:
2 |   (name TestUnionFind)
            ^^^^^^^^^^^^^
(cd _build/default/test && ./TestUnionFind.exe)
Fatal error: exception Invalid_argument("Array.make")
error: in phase 'check': uncaught exception:
%exception #<&invoke-error program: "dune" arguments: ("runtest" "--release") exit-status: 1 term-signal: #f stop-signal: #f> 
phase `check' failed after 0.6 seconds
--8<---------------cut here---------------end--------------->8---

Could you take a look?

It seems qa.guix is reporting on v1 of the patch set though because the
build logs suggest ‘ocaml-unionfind’ was lacking the (file-name
(git-file-name …)) stanza.

Apart from that the series LGTM.

Thanks,
Ludo’.

[bug#70567] [PATCH v2 7/7] gnu: frama-c: Update to 28.1.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (frama-c): Update to 28.1.

Change-Id: I0ce0d0a7db4d017ba1f5028e73c931ceb706fce5
---
 gnu/packages/maths.scm | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 9bf2f64cbb..38ce38fc2b 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9457,14 +9457,14 @@ (define-public why3
 (define-public frama-c
   (package
     (name "frama-c")
-    (version "27.1")
+    (version "28.1")
     (source (origin
               (method url-fetch)
-              (uri (string-append "http://frama-c.com/download/frama-c-"
-                                  version "-Cobalt.tar.gz"))
+              (uri (string-append "https://frama-c.com/download/frama-c-"
+                                  version "-Nickel.tar.gz"))
               (sha256
                (base32
-                "1lirkvhf5m53d33l0aw5jzc1fyzkwx5fkgh9g71732d52r55f4sv"))))
+                "14zmwghwhcryvri7k91vc1yampvxvhg36vwjxf64d8kx7dsbq802"))))
     (build-system dune-build-system)
     (arguments
       `(#:phases
@@ -9487,6 +9487,7 @@ (define-public frama-c
                          ocaml-ppx-deriving-yojson
                          ocaml-ppx-deriving-yaml
                          ocaml-ppx-import
+                         ocaml-unionfind
                          why3))
     (native-inputs (list dune-site time ocaml-menhir ocaml-graph))
     (native-search-paths
-- 
2.41.0

[bug#70567] [PATCH v2 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/ocaml.scm (ocaml-lablgtk3-sourceview3): Move gtksourceview-3 from
native-inputs to propagated-inputs.  Remove native-inputs and use
inherited inputs instead.

Change-Id: I2b242343bdace17ee3e992ce71f4e49b3c375e15
---
 gnu/packages/ocaml.scm | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 3bd923f97d..714edf83ef 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com>
 ;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;; Copyright © 2023 Csepp <raingloom@riseup.net>
-;;; Copyright © 2023 Foundation Devices, Inc. <hello@foundationdevices.com>
+;;; Copyright © 2023,2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;; Copyright © 2023 Arnaud DABY-SEESARAM <ds-ac@nanein.fr>
 ;;; Copyright © 2024 Sören Tempel <soeren@soeren-tempel.net>
 ;;;
@@ -8570,8 +8570,7 @@ (define-public ocaml-lablgtk3-sourceview3
   (package
     (inherit lablgtk3)
     (name "ocaml-lablgtk3-sourceview3")
-    (propagated-inputs (list lablgtk3))
-    (native-inputs (list gtksourceview-3 pkg-config))
+    (propagated-inputs (list gtksourceview-3 lablgtk3))
     (arguments
      `(#:package "lablgtk3-sourceview3"))
     (synopsis "OCaml interface to GTK+ gtksourceview library")

base-commit: 014875b29e68da6357a5323e6dd1eaa74a05b753
-- 
2.41.0

[bug#70567] [PATCH v2 2/7] gnu: coq-flocq: Update to 4.1.4.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/coq.scm (coq-flocq): Update to 4.1.4.

Change-Id: Ia2bf4bccad712a7bfa5427ef26ad93d39f1fc6e0
---
 gnu/packages/coq.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 105b942ad3..11d6b034f1 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -9,6 +9,7 @@
 ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
 ;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
 ;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
+;;; Copyright © 2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -217,7 +218,7 @@ (define-public proof-general
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "4.1.1")
+    (version "4.1.4")
     (source
      (origin
        (method git-fetch)
@@ -227,7 +228,7 @@ (define-public coq-flocq
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "01x38w58j95ba9679vpb5wv4bvfnrapd5dzjqlyz8k7i8a9sfqn0"))))
+         "08vrh0h909vmam1b4gfrvcmamnhmr5g0x79zx98hn7cx0vdwysh7"))))
     (build-system gnu-build-system)
     (native-inputs
      (list autoconf automake ocaml which coq))
-- 
2.41.0

[bug#70567] [PATCH v2 3/7] gnu: why3: Update to 1.7.2.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Update to 1.7.2.

Change-Id: Ie5a40b31c2c418fafbdbba52e875ac25a26fb12b
---
 gnu/packages/maths.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 93335d23f7..5e524db893 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -63,6 +63,7 @@
 ;;; Copyright © 2023 Jake Leporte <jakeleporte@outlook.com>
 ;;; Copyright © 2023 Camilo Q.S. (Distopico) <distopico@riseup.net>
 ;;; Copyright © 2023 David Elsing <david.elsing@posteo.net>
+;;; Copyright © 2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -9388,7 +9389,7 @@ (define-public numdiff
 (define-public why3
   (package
     (name "why3")
-    (version "1.6.0")
+    (version "1.7.2")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -9397,7 +9398,7 @@ (define-public why3
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0k3y98xzhrl44vwzq2m6k4nrllrwp3ll69lc2gfl8d77w0wg7gkp"))))
+                "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
     (native-inputs
      (list autoconf automake coq ocaml which))
-- 
2.41.0

[bug#70567] [PATCH v2 4/7] gnu: why3: Use new style.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Use new style and move arguments
above input fields.

Change-Id: Ia9cb04cafe426d7f20c5efb10ca540572dbd3be9
---
 gnu/packages/maths.scm | 63 +++++++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 29 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5e524db893..93370eef83 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9400,36 +9400,41 @@ (define-public why3
                (base32
                 "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
-    (native-inputs
-     (list autoconf automake coq ocaml which))
-    (propagated-inputs
-     (list camlzip ocaml-graph ocaml-menhir ocaml-num ocaml-zarith))
-    (inputs
-     (list coq-flocq emacs-minimal zlib))
     (arguments
-     `(#:phases
-       (modify-phases %standard-phases
-         (add-before 'configure 'bootstrap
-           (lambda _
-             (invoke "./autogen.sh")
-             (setenv "CONFIG_SHELL" (which "sh"))
-             (substitute* "configure"
-               (("#! /bin/sh") (string-append "#!" (which "sh")))
-               ;; find ocaml-num in the correct directory
-               (("\\$DIR/nums.cma") "$DIR/num.cma")
-               (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))
-             #t))
-         (add-after 'configure 'fix-makefile
-           (lambda _
-             (substitute* "Makefile"
-               ;; find ocaml-num in the correct directory
-               (("site-lib/num") "site-lib"))
-             #t))
-        (add-after 'install 'install-lib
-          (lambda _
-            (invoke "make" "byte")
-            (invoke "make" "install-lib")
-            #t)))))
+     (list #:phases
+           #~(modify-phases %standard-phases
+               (add-before 'configure 'bootstrap
+                 (lambda _
+                   (invoke "./autogen.sh")
+                   (setenv "CONFIG_SHELL" (which "sh"))
+                   (substitute* "configure"
+                     (("#! /bin/sh") (string-append "#!" (which "sh")))
+                     ;; find ocaml-num in the correct directory
+                     (("\\$DIR/nums.cma") "$DIR/num.cma")
+                     (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))))
+               (add-after 'configure 'fix-makefile
+                 (lambda _
+                   (substitute* "Makefile"
+                     ;; find ocaml-num in the correct directory
+                     (("site-lib/num") "site-lib"))))
+            (add-after 'install 'install-lib
+              (lambda _
+                (invoke "make" "byte")
+                (invoke "make" "install-lib"))))))
+    (native-inputs (list autoconf
+                         automake
+                         coq
+                         ocaml
+                         ocaml-findlib
+                         which))
+    (propagated-inputs (list camlzip
+                             ocaml-graph
+                             ocaml-menhir
+                             ocaml-num
+                             ocaml-zarith))
+    (inputs (list coq-flocq
+                  emacs-minimal
+                  zlib))
     (home-page "https://why3.lri.fr")
     (synopsis "Deductive program verification")
     (description "Why3 provides a language for specification and programming,
-- 
2.41.0

[bug#70567] [PATCH v2 5/7] gnu: why3: Enable extra features.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3) <propagated-inputs>: Add
ocaml-ppx-deriving, ocaml-ppx-sexp-conv, ocaml-re and ocaml-sexplib to
enable extra features.

Change-Id: Ia3b66ac08cc25097967c6e18f2193601fb748cac
---
 gnu/packages/maths.scm | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 93370eef83..3f665c0fb4 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9428,9 +9428,15 @@ (define-public why3
                          ocaml-findlib
                          which))
     (propagated-inputs (list camlzip
+                             lablgtk3
                              ocaml-graph
+                             ocaml-lablgtk3-sourceview3
                              ocaml-menhir
+                             ocaml-ppx-deriving
+                             ocaml-ppx-sexp-conv
                              ocaml-num
+                             ocaml-re
+                             ocaml-sexplib
                              ocaml-zarith))
     (inputs (list coq-flocq
                   emacs-minimal
-- 
2.41.0

[bug#70567] [PATCH v2 6/7] gnu: Add ocaml-unionfind.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/ocaml.scm (ocaml-unionfind): New variable.

Change-Id: Ib101e67576c000dad1d4a73d008ca0376e7da95a
---
 gnu/packages/ocaml.scm | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 714edf83ef..1439b51831 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3186,6 +3186,34 @@ (define ocaml-eio-luv
 (define-public ocaml5.0-eio-luv
   (package-with-ocaml5.0 ocaml-eio-luv))
 
+(define-public ocaml-unionfind
+  (package
+    (name "ocaml-unionfind")
+    (version "20220122")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+              (url "https://gitlab.inria.fr/fpottier/unionfind")
+              (commit version)))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "0hdh56rbg8vfjd61q09cbmh8l5wmry5ykivg7gsm0v5ckkb3531r"))))
+    (build-system dune-build-system)
+    (arguments
+     (list ;; The test allocates an Array that is too large for OCaml when on a
+           ;; 32-bit architecture.
+           #:tests? (target-64bit?)))
+    (home-page "https://gitlab.inria.fr/fpottier/unionFind")
+    (synopsis "Union-find data structure")
+    (description "This package provides two union-find data structure
+implementations for OCaml.  Both implementations are based on disjoint sets
+forests, with path compression and linking-by-rank, so as to guarantee good
+asymptotic complexity: every operation requires a quasi-constant number of
+accesses to the store.")
+    ;; Version 2 only, with linking exception.
+    (license license:lgpl2.0)))
+
 (define-public ocaml-uring
   (package
     (name "ocaml-uring")
-- 
2.41.0

[bug#70567] [PATCH v2 7/7] gnu: frama-c: Update to 28.1.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (frama-c): Update to 28.1.

Change-Id: I0ce0d0a7db4d017ba1f5028e73c931ceb706fce5
---
 gnu/packages/maths.scm | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 3f665c0fb4..a7a3707044 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9457,14 +9457,14 @@ (define-public why3
 (define-public frama-c
   (package
     (name "frama-c")
-    (version "27.1")
+    (version "28.1")
     (source (origin
               (method url-fetch)
-              (uri (string-append "http://frama-c.com/download/frama-c-"
-                                  version "-Cobalt.tar.gz"))
+              (uri (string-append "https://frama-c.com/download/frama-c-"
+                                  version "-Nickel.tar.gz"))
               (sha256
                (base32
-                "1lirkvhf5m53d33l0aw5jzc1fyzkwx5fkgh9g71732d52r55f4sv"))))
+                "14zmwghwhcryvri7k91vc1yampvxvhg36vwjxf64d8kx7dsbq802"))))
     (build-system dune-build-system)
     (arguments
       `(#:phases
@@ -9487,6 +9487,7 @@ (define-public frama-c
                          ocaml-ppx-deriving-yojson
                          ocaml-ppx-deriving-yaml
                          ocaml-ppx-import
+                         ocaml-unionfind
                          why3))
     (native-inputs (list dune-site time ocaml-menhir ocaml-graph))
     (native-search-paths
-- 
2.41.0

[bug#70567] [PATCH v2 7/7] gnu: frama-c: Update to 28.1.

[Andreas Enge]

Hello,

thanks for the patches and the reviews! I have pushed the commits 1 to 2
and 6 to 7, after checking that frama-c still compiles like this.

Commit 3 does not apply any more, since there have been additions to
maths.scm.

Could you please prepare a new version of commits 3 to 5 that apply
to master?

Thanks,

Andreas

[bug#70567] [PATCH v2 7/7] gnu: frama-c: Update to 28.1.

[Jean-Pierre De Jesus Diaz]

Hello Andreas,

Thanks for committing the patches!

I've sent a V3 with the rest of the unapplied patches with the conflicts
solved.

Thanks,

Jean-Pierre

On Wed, May 15, 2024 at 2:53 PM Andreas Enge <andreas@enge.fr> wrote:
>
> Hello,
>
> thanks for the patches and the reviews! I have pushed the commits 1 to 2
> and 6 to 7, after checking that frama-c still compiles like this.
>
> Commit 3 does not apply any more, since there have been additions to
> maths.scm.
>
> Could you please prepare a new version of commits 3 to 5 that apply
> to master?
>
> Thanks,
>
> Andreas
>

bug#70567: [PATCH v2 7/7] gnu: frama-c: Update to 28.1.

[Andreas Enge]

Am Wed, May 15, 2024 at 03:05:07PM +0000 schrieb Jean-Pierre De Jesus Diaz:
> I've sent a V3 with the rest of the unapplied patches with the conflicts
> solved.

That was lightning fast, I have applied and pushed them.
Thanks!

Andreas

[bug#70567] [PATCH v3 1/3] gnu: why3: Update to 1.7.2.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Update to 1.7.2.

Change-Id: Ie5a40b31c2c418fafbdbba52e875ac25a26fb12b
---
 gnu/packages/maths.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index f2280cb392..cbde85751c 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -64,6 +64,7 @@
 ;;; Copyright © 2023 Camilo Q.S. (Distopico) <distopico@riseup.net>
 ;;; Copyright © 2023 David Elsing <david.elsing@posteo.net>
 ;;; Copyright © 2024 Herman Rimm <herman@rimm.ee>
+;;; Copyright © 2024 Foundation Devices, Inc. <hello@foundation.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -9485,7 +9486,7 @@ (define-public numdiff
 (define-public why3
   (package
     (name "why3")
-    (version "1.6.0")
+    (version "1.7.2")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -9494,7 +9495,7 @@ (define-public why3
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0k3y98xzhrl44vwzq2m6k4nrllrwp3ll69lc2gfl8d77w0wg7gkp"))))
+                "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
     (native-inputs
      (list autoconf automake coq ocaml which))

base-commit: 28ce5085a0a4191c27aecdc085600acf585b607c
-- 
2.41.0

[bug#70567] [PATCH v3 2/3] gnu: why3: Use new style.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3): Use new style and move arguments
above input fields.

Change-Id: Ia9cb04cafe426d7f20c5efb10ca540572dbd3be9
---
 gnu/packages/maths.scm | 63 +++++++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 29 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index cbde85751c..1e10d4caa8 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9497,36 +9497,41 @@ (define-public why3
                (base32
                 "0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
     (build-system ocaml-build-system)
-    (native-inputs
-     (list autoconf automake coq ocaml which))
-    (propagated-inputs
-     (list camlzip ocaml-graph ocaml-menhir ocaml-num ocaml-zarith))
-    (inputs
-     (list coq-flocq emacs-minimal zlib))
     (arguments
-     `(#:phases
-       (modify-phases %standard-phases
-         (add-before 'configure 'bootstrap
-           (lambda _
-             (invoke "./autogen.sh")
-             (setenv "CONFIG_SHELL" (which "sh"))
-             (substitute* "configure"
-               (("#! /bin/sh") (string-append "#!" (which "sh")))
-               ;; find ocaml-num in the correct directory
-               (("\\$DIR/nums.cma") "$DIR/num.cma")
-               (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))
-             #t))
-         (add-after 'configure 'fix-makefile
-           (lambda _
-             (substitute* "Makefile"
-               ;; find ocaml-num in the correct directory
-               (("site-lib/num") "site-lib"))
-             #t))
-        (add-after 'install 'install-lib
-          (lambda _
-            (invoke "make" "byte")
-            (invoke "make" "install-lib")
-            #t)))))
+     (list #:phases
+           #~(modify-phases %standard-phases
+               (add-before 'configure 'bootstrap
+                 (lambda _
+                   (invoke "./autogen.sh")
+                   (setenv "CONFIG_SHELL" (which "sh"))
+                   (substitute* "configure"
+                     (("#! /bin/sh") (string-append "#!" (which "sh")))
+                     ;; find ocaml-num in the correct directory
+                     (("\\$DIR/nums.cma") "$DIR/num.cma")
+                     (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))))
+               (add-after 'configure 'fix-makefile
+                 (lambda _
+                   (substitute* "Makefile"
+                     ;; find ocaml-num in the correct directory
+                     (("site-lib/num") "site-lib"))))
+            (add-after 'install 'install-lib
+              (lambda _
+                (invoke "make" "byte")
+                (invoke "make" "install-lib"))))))
+    (native-inputs (list autoconf
+                         automake
+                         coq
+                         ocaml
+                         ocaml-findlib
+                         which))
+    (propagated-inputs (list camlzip
+                             ocaml-graph
+                             ocaml-menhir
+                             ocaml-num
+                             ocaml-zarith))
+    (inputs (list coq-flocq
+                  emacs-minimal
+                  zlib))
     (home-page "https://why3.lri.fr")
     (synopsis "Deductive program verification")
     (description "Why3 provides a language for specification and programming,
-- 
2.41.0

[bug#70567] [PATCH v3 3/3] gnu: why3: Enable extra features.

[Jean-Pierre De Jesus DIAZ]

* gnu/packages/maths.scm (why3) <propagated-inputs>: Add
ocaml-ppx-deriving, ocaml-ppx-sexp-conv, ocaml-re and ocaml-sexplib to
enable extra features.

Change-Id: Ia3b66ac08cc25097967c6e18f2193601fb748cac
---
 gnu/packages/maths.scm | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 1e10d4caa8..9a37b681e9 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9525,9 +9525,15 @@ (define-public why3
                          ocaml-findlib
                          which))
     (propagated-inputs (list camlzip
+                             lablgtk3
                              ocaml-graph
+                             ocaml-lablgtk3-sourceview3
                              ocaml-menhir
+                             ocaml-ppx-deriving
+                             ocaml-ppx-sexp-conv
                              ocaml-num
+                             ocaml-re
+                             ocaml-sexplib
                              ocaml-zarith))
     (inputs (list coq-flocq
                   emacs-minimal
-- 
2.41.0