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

  • Done
  • quality assurance status badge
Details
5 participants
  • Andreas Enge
  • Arnaud Daby-Seesaram
  • Jean-Pierre De Jesus DIAZ
  • Julien Lepiller
  • Ludovic Courtès
Owner
unassigned
Submitted by
Jean-Pierre De Jesus DIAZ
Severity
normal
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:08 +0200
(address . guix-patches@gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
cover.1714050321.git.jean@foundation.xyz
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:12 +0200
[PATCH 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
fed82eb94f9d8f797e8ff23f3f4d45657295c1de.1714050321.git.jean@foundation.xyz
* 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(-)

Toggle diff (25 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:12 +0200
[PATCH 3/7] gnu: why3: Update to 1.7.2.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
428630065739ac8913d338b5ee182b9dd329f42e.1714050321.git.jean@foundation.xyz
* 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(-)

Toggle diff (32 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:12 +0200
[PATCH 5/7] gnu: why3: Enable extra features.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
46392d7f1d7404f2b78623c512737a046db71e5c.1714050321.git.jean@foundation.xyz
* 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(+)

Toggle diff (22 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:12 +0200
[PATCH 6/7] gnu: Add ocaml-unionfind.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
3019a8693bf8589e09e840916ea6463cf87393a7.1714050321.git.jean@foundation.xyz
* gnu/packages/ocaml.scm (ocaml-unionfind): New variable.

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

Toggle diff (36 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:12 +0200
[PATCH 2/7] gnu: coq-flocq: Update to 4.1.4.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
830c2d48556ea1720ca3f72f6e4df365246c3928.1714050321.git.jean@foundation.xyz
* 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(-)

Toggle diff (32 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:12 +0200
[PATCH 7/7] gnu: frama-c: Update to 28.1.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
409df579886d71d579d4df3da980d08f061d585a.1714050321.git.jean@foundation.xyz
* 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(-)

Toggle diff (32 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 15:12 +0200
[PATCH 4/7] gnu: why3: Use new style.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
8d9581a5f8063da2f40c4d9d35529219d3a0ee6b.1714050321.git.jean@foundation.xyz
* 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(-)

Toggle diff (77 lines)
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
J
J
Julien Lepiller wrote on 25 Apr 16:30 +0200
Re: [bug#70567] [PATCH 0/7] frama-c: Update to 28.1.
9F75F023-232F-4791-9D77-817861AB3984@lepiller.eu
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 :
Toggle quote (25 lines)
>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
A
A
Arnaud Daby-Seesaram wrote on 25 Apr 16:54 +0200
(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
8734r9a3x1.fsf@nanein.fr
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
-----BEGIN PGP SIGNATURE-----

iQJEBAEBCgAuFiEEMgqfJ4U0fby1t860ojLKXoMTiAwFAmYqbqoQHGRzLWFjQG5h
bmVpbi5mcgAKCRCiMspegxOIDCoND/43BXYYujaxTjcdLNaRN4BBvj4MbrZVY4dm
aJFUWOVhjlix6uY1UNiCkJeH4L+NwlQMBspvhBLYRrZavc6M3XAV1Hqte8uxTyL+
FpkhFXgiXB0uA6dHQJRV7Rs28MaEL/eAp8iIYebEWoXnJVOgBemh5TiHXEo/V+SM
gTXlnSCfsldO5RbmIBjwDy2ENpOv09LriwbYoLnlOabONcQKDyzX4B+RZJFxMNV/
xEAIJ3v4jXLidiCfp/F+ZliylOrMf0R3WzaXYfwlXn5WyjlYP6cMtF7reznNLgBp
oJ9NxkpV94w9x7sfZoJBZIx6ajd4FsY7cFaJesNvY3lbhpEWFxAG06Op7BaG8XNq
ra6YGXLGOtWU0S7WECSJZpXDJ7v8msJChO0bwWMJ/AtP5JuwZuB4D8L90cVTlnrU
JUIhXJz+lCUgIjJEGhNswAVdyqRhmPV9mqVoMUvV8TGTEwX+c138LXA/NQhW/USR
tWGfI1rsPm1QxFtVh2kPBSycQrGH/wr0IqXAPA/EliH4yLMfEe6JhrJQlEqOXwD7
dffJj3AINM4SeKMH0d9g6nYN6VUurQ9ibv5PRbuR15gTRZX5y9SIbQs1o0AHQZ6E
H9y9RRIc/mbiuJIlQzUn5rtqEV8T/RKhePobgbadc74T1hEhRKsCKxPecceD8aDi
ao85zhxgKQ==
=ovSx
-----END PGP SIGNATURE-----

J
J
Jean-Pierre De Jesus Diaz wrote on 25 Apr 17:08 +0200
(name . Arnaud Daby-Seesaram)(address . ds-ac@nanein.fr)
CAG1gdUonTQgyfBi2xT5UTQwOuSo5YZCo9dEWxhHn-evXvQSdSw@mail.gmail.com
Hi,

Toggle quote (10 lines)
>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.


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

Toggle quote (2 lines)
>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:
Toggle quote (33 lines)
>
> 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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 17:21 +0200
[PATCH v2 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
fed82eb94f9d8f797e8ff23f3f4d45657295c1de.1714058471.git.jean@foundation.xyz
* 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(-)

Toggle diff (27 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 17:21 +0200
[PATCH v2 2/7] gnu: coq-flocq: Update to 4.1.4.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
830c2d48556ea1720ca3f72f6e4df365246c3928.1714058471.git.jean@foundation.xyz
* 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(-)

Toggle diff (32 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 17:21 +0200
[PATCH v2 3/7] gnu: why3: Update to 1.7.2.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
428630065739ac8913d338b5ee182b9dd329f42e.1714058471.git.jean@foundation.xyz
* 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(-)

Toggle diff (32 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 17:21 +0200
[PATCH v2 4/7] gnu: why3: Use new style.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
8d9581a5f8063da2f40c4d9d35529219d3a0ee6b.1714058471.git.jean@foundation.xyz
* 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(-)

Toggle diff (77 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 17:21 +0200
[PATCH v2 5/7] gnu: why3: Enable extra features.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
46392d7f1d7404f2b78623c512737a046db71e5c.1714058471.git.jean@foundation.xyz
* 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(+)

Toggle diff (22 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 17:21 +0200
[PATCH v2 7/7] gnu: frama-c: Update to 28.1.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
6e37c8b260af004b4379c157c863d285695ff6bd.1714058471.git.jean@foundation.xyz
* 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(-)

Toggle diff (33 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 25 Apr 17:21 +0200
[PATCH v2 6/7] gnu: Add ocaml-unionfind.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
4715ea80d95284555c5240e2834598ce7abbe609.1714058471.git.jean@foundation.xyz
* gnu/packages/ocaml.scm (ocaml-unionfind): New variable.

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

Toggle diff (37 lines)
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
A
A
Arnaud Daby-Seesaram wrote on 25 Apr 17:23 +0200
Re: [bug#70567] [PATCH 0/7] frama-c: Update to 28.1.
(name . Jean-Pierre De Jesus Diaz)(address . jean@foundation.xyz)
87y1918o11.fsf@nanein.fr
Toggle quote (4 lines)
> 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 :).


Toggle quote (2 lines)
> 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).
Toggle quote (2 lines)
> but for privacy reasons should be on https IMO.

Best,

--
Arnaud
-----BEGIN PGP SIGNATURE-----

iQJEBAEBCgAuFiEEMgqfJ4U0fby1t860ojLKXoMTiAwFAmYqdVoQHGRzLWFjQG5h
bmVpbi5mcgAKCRCiMspegxOIDN5mD/9rwj/f+OJAx9WcocNKEFOKvYLIIkvM1+WK
/hKIcTdL4FH7u0uNlze7NECx1Qi7Z8MOzWYWX1JJUkH599jrZ+uhH7Q/WVehgPoC
mIPzrC5KprAgLspv1GyNYR7IWi9AM5TvYHfng5dRbin2/8tFrKXPODRcZY9L5hpN
W15ZyiAZl0ykttygwcLrUpkqsQf53GwbMCXk1WYAV8tsoHuIi6b8DM7UG7kSr5lO
m+yPtVC7qPYwoTa2PbubQ0JfwSjlbZgTEneaC4PqJglTU2MX62rHppUdg3e0sreJ
7I6yt/6UnPRftRmJ5iuhzMb4f7pLO8E4pqkVqkoM4xjeDKfqkJQqEJjTAx2BO79x
2WGrJ8jJ53zzpnS5+e9YsrngGHuOxMG1Qf0mgUrK3UjRkIXRpIkkuEW0QWQet7Z4
gTbEsu8/4YGfzTdqJfOQ4QMhW5guMuUjQhCmo3M7Ps7Qt0BVyI/f8gLxY1GKXF0J
6NB7htNAerJezLwNvh5VVodCs22O6U24MoH9ImG7wzQoBFrg89Q1RkSltLiKxcfp
f37fyKxzxetUOexrcR105uT6DJoJad+ytVWjKhzzaQQKQCUjH2y8ct0Renh7HbGX
83uWjcHUTCwHKpz7lqKsGmxbioBbSdmE6VmBPf4jr0MHaF5wB8eoJsDcTDuEkC2H
lF2WcjmAgQ==
=H9cW
-----END PGP SIGNATURE-----

J
J
Julien Lepiller wrote on 25 Apr 17:22 +0200
23FB3A3D-8FED-418D-AF36-0EF59C95F0E7@lepiller.eu
Le 25 avril 2024 16:54:34 GMT+02:00, Arnaud Daby-Seesaram via Guix-patches via <guix-patches@gnu.org> a écrit :
Toggle quote (24 lines)
>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

Toggle quote (4 lines)
>
>
>Orthogonal comment: should "http://" be replaced by "https://"?

If the website is available at https, yes

Toggle quote (4 lines)
>
>
>Best regards,
>
J
J
Jean-Pierre De Jesus Diaz wrote on 25 Apr 17:35 +0200
(name . Julien Lepiller)(address . julien@lepiller.eu)
CAG1gdUrp_3_GwSLWre0fYceO-TDqEpi13HBGjWFHLFXqX6b19w@mail.gmail.com
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:
Toggle quote (40 lines)
>
>
>
> 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,
> >
A
A
Andreas Enge wrote on 25 Apr 17:35 +0200
(name . Julien Lepiller)(address . julien@lepiller.eu)
Zip4TdRxA4Bqs6nS@jurong
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
J
J
Jean-Pierre De Jesus Diaz wrote on 26 Apr 15:03 +0200
(name . Andreas Enge)(address . andreas@enge.fr)
CAG1gdUpHH4OvujTS_gLEbs76Odp4Wv1YuHnnR2fudymdtckQtA@mail.gmail.com
Hi,

Toggle quote (7 lines)
>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.

Toggle quote (4 lines)
>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:
Toggle quote (16 lines)
>
> 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
>
A
A
Andreas Enge wrote on 28 Apr 16:01 +0200
(name . Jean-Pierre De Jesus Diaz)(address . jean@foundation.xyz)
Zi5WtyGSVKyguWiv@jurong
Am Fri, Apr 26, 2024 at 01:03:44PM +0000 schrieb Jean-Pierre De Jesus Diaz:
Toggle quote (6 lines)
> >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
L
L
Ludovic Courtès wrote on 1 May 18:13 +0200
Re: [bug#70567] [PATCH v2 6/7] gnu: Add ocaml-unionfind.
(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
87bk5p5x4e.fsf@gnu.org
Hi Jean-Pierre,

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

Toggle quote (4 lines)
> * 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):

Toggle snippet (11 lines)
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

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’.
J
J
Jean-Pierre De Jesus DIAZ wrote on 7 May 17:57 +0200
[PATCH v2 2/7] gnu: coq-flocq: Update to 4.1.4.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
8eb3cfb6952f76a6178ae6548502580ebb46a1af.1715097365.git.jean@foundation.xyz
* 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(-)

Toggle diff (32 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 7 May 17:57 +0200
[PATCH v2 1/7] gnu: ocaml-lablgtk3-sourceview3: Fix inputs.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
dd981ac1613da5b3dc94f643cc86b1afd194ca0e.1715097365.git.jean@foundation.xyz
* 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(-)

Toggle diff (27 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 7 May 17:57 +0200
[PATCH v2 3/7] gnu: why3: Update to 1.7.2.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
3cfc3809a52a94a13e64cebf21ef8f29789b56a0.1715097365.git.jean@foundation.xyz
* 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(-)

Toggle diff (32 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 7 May 17:57 +0200
[PATCH v2 5/7] gnu: why3: Enable extra features.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
5f9156b041743f4293a65f1a26ddd33bbf8951ac.1715097365.git.jean@foundation.xyz
* 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(+)

Toggle diff (22 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 7 May 17:57 +0200
[PATCH v2 6/7] gnu: Add ocaml-unionfind.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
5888bbbca8fb1369c915e0c7867222ad54b031f1.1715097365.git.jean@foundation.xyz
* gnu/packages/ocaml.scm (ocaml-unionfind): New variable.

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

Toggle diff (41 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 7 May 17:57 +0200
[PATCH v2 4/7] gnu: why3: Use new style.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
927ba426e4e455b80294a6df4a7528f1bb708af4.1715097365.git.jean@foundation.xyz
* 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(-)

Toggle diff (77 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 7 May 17:57 +0200
[PATCH v2 7/7] gnu: frama-c: Update to 28.1.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
0d544c7063b7986013f640125b6c9ef3ee249a4c.1715097365.git.jean@foundation.xyz
* 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(-)

Toggle diff (33 lines)
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
A
A
Andreas Enge wrote on 15 May 16:52 +0200
(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
ZkTMRPtTxgw-mh2S@jurong
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 15 May 17:01 +0200
[PATCH v3 1/3] gnu: why3: Update to 1.7.2.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
8b22a962e6ece2c17b45c1844fc4e63d3145c6ae.1715785259.git.jean@foundation.xyz
* 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(-)

Toggle diff (34 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 15 May 17:01 +0200
[PATCH v3 2/3] gnu: why3: Use new style.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
75eac710c55c0c6a9494c03e30adefaf19e3c558.1715785259.git.jean@foundation.xyz
* 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(-)

Toggle diff (77 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 15 May 17:01 +0200
[PATCH v3 3/3] gnu: why3: Enable extra features.
(address . 70567@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
fbfa410c4737c4a1754987baad3ddddbaf3a975f.1715785259.git.jean@foundation.xyz
* 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(+)

Toggle diff (22 lines)
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
J
J
Jean-Pierre De Jesus Diaz wrote on 15 May 17:05 +0200
Re: [bug#70567] [PATCH v2 7/7] gnu: frama-c: Update to 28.1.
(name . Andreas Enge)(address . andreas@enge.fr)
CAG1gdUokiqBc1hEhpfrb7H7oAi-1Tvc13u_TArFXULJcQOycyQ@mail.gmail.com
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:
Toggle quote (16 lines)
>
> 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
>
A
A
Andreas Enge wrote on 15 May 17:23 +0200
(name . Jean-Pierre De Jesus Diaz)(address . jean@foundation.xyz)
ZkTTfLgIOBU4Jk0E@jurong
Am Wed, May 15, 2024 at 03:05:07PM +0000 schrieb Jean-Pierre De Jesus Diaz:
Toggle quote (3 lines)
> 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
Closed
?
Your comment

This issue is archived.

To comment on this conversation send an email to 70567@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 70567
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch