| Message ID | cover.1714050321.git.jean@foundation.xyz |
|---|---|
| Headers | show |
| Series | frama-c: Update to 28.1. | expand |
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
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,
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
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, >
> 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,
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, > >
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
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 >
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