From 41634d3b5f6a4bdc7b3c42b0bdff79850d0bbedc Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Wed, 10 Jan 2024 08:43:33 +0100
Subject: gnu: frama-c: Update to 27.1.

* gnu/packages/maths.scm (frama-c): Update to 27.1.
(why3): Update to 1.6.0.

Change-Id: I74191e4274d58a88a772413875fbf7de4d243fec
---
 gnu/packages/maths.scm | 54 +++++++++++++++++++++++++++-----------------------
 1 file changed, 29 insertions(+), 25 deletions(-)

(limited to 'gnu/packages/maths.scm')

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index ada828cb3f..9a114f7f76 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
 ;;; Copyright © 2018, 2020-2022 Marius Bakke <marius@gnu.org>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
-;;; Copyright © 2018, 2021 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018, 2021, 2024 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;; Copyright © 2019, 2021-2023 Nicolas Goaziou <mail@nicolasgoaziou.fr>
 ;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
@@ -93,6 +93,7 @@ (define-module (gnu packages maths)
   #:use-module (guix build-system ant)
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system copy)
+  #:use-module (guix build-system dune)
   #:use-module (guix build-system glib-or-gtk)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system meson)
@@ -183,6 +184,7 @@ (define-module (gnu packages maths)
   #:use-module (gnu packages tcl)
   #:use-module (gnu packages texinfo)
   #:use-module (gnu packages tex)
+  #:use-module (gnu packages time)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages version-control)
   #:use-module (gnu packages wxwidgets)
@@ -9354,7 +9356,7 @@ (define-public numdiff
 (define-public why3
   (package
     (name "why3")
-    (version "1.4.1")
+    (version "1.6.0")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -9363,7 +9365,7 @@ (define-public why3
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1yca6mx8bjm8x0i594ivh31aw45s6fbimmwfj8g2v9zwrgmr1i4s"))))
+                "0k3y98xzhrl44vwzq2m6k4nrllrwp3ll69lc2gfl8d77w0wg7gkp"))))
     (build-system ocaml-build-system)
     (native-inputs
      (list autoconf automake coq ocaml which))
@@ -9411,36 +9413,38 @@ (define-public why3
 (define-public frama-c
   (package
     (name "frama-c")
-    (version "24.0")
+    (version "27.1")
     (source (origin
               (method url-fetch)
               (uri (string-append "http://frama-c.com/download/frama-c-"
-                                  version "-Chromium.tar.gz"))
+                                  version "-Cobalt.tar.gz"))
               (sha256
                (base32
-                "0x1xgip50jdz1phsb9rzwf2ra8lshn1hmd9g967xia402wrg3sjf"))))
-    (build-system ocaml-build-system)
+                "1lirkvhf5m53d33l0aw5jzc1fyzkwx5fkgh9g71732d52r55f4sv"))))
+    (build-system dune-build-system)
     (arguments
-     `(#:tests? #f; no test target in Makefile
-       #:configure-flags
-       (list "--enable-verbosemake")    ; to aid debugging
-       #:phases
-       (modify-phases %standard-phases
-         (add-before 'configure 'export-shell
-           (lambda* (#:key inputs #:allow-other-keys)
-             (setenv "CONFIG_SHELL"
-                     (search-input-file inputs "/bin/sh")))))))
+      `(#:phases
+        (modify-phases %standard-phases
+          (add-before 'build 'set-env
+            (lambda _
+              (setenv "CC" "gcc"))))))
     (inputs
      (list gmp zlib))
-    (propagated-inputs
-     (list ocaml-biniou
-           ocaml-easy-format
-           ocaml-graph
-           ocaml-yojson
-           ocaml-zarith
-           ocaml-lablgtk3-sourceview3
-           lablgtk3
-           why3))
+    (propagated-inputs (list
+                         graphviz
+                         lablgtk3
+                         ocaml-graph
+                         ocaml-odoc
+                         ocaml-lablgtk3-sourceview3
+                         ocaml-yaml
+                         ocaml-yojson
+                         ocaml-zarith
+                         ocaml-ppx-deriving
+                         ocaml-ppx-deriving-yojson
+                         ocaml-ppx-deriving-yaml
+                         ocaml-ppx-import
+                         why3))
+    (native-inputs (list dune-site time ocaml-menhir ocaml-graph))
     (native-search-paths
      (list (search-path-specification
             (variable "FRAMAC_SHARE")
-- 
cgit v1.2.3