Bug 1795083 - The frama-c and frama-c-gui programs abort on startup in Rawhide (f32)
Summary: The frama-c and frama-c-gui programs abort on startup in Rawhide (f32)
Keywords:
Status: CLOSED ERRATA
Alias: None
Product: Fedora
Classification: Fedora
Component: frama-c
Version: 32
Hardware: x86_64
OS: Linux
unspecified
low
Target Milestone: ---
Assignee: Jerry James
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2020-01-27 01:46 UTC by Ian Laurie
Modified: 2020-04-25 02:20 UTC (History)
1 user (show)

Fixed In Version: frama-c-20.0-1.fc32 frama-c-19.1-4.fc31 frama-c-20.0-2.fc32
Doc Type: If docs needed, set a value
Doc Text:
Clone Of:
Environment:
Last Closed: 2020-04-22 23:23:34 UTC
Type: Bug
Embargoed:


Attachments (Terms of Use)

Description Ian Laurie 2020-01-27 01:46:17 UTC
Description of problem:
The frama-c and frama-c-gui programs abort on startup.

Version-Release number of selected component (if applicable):
frama-c-19.1-5.fc32.x86_64

How reproducible:
Always.

Steps to Reproduce:
1. Launch frama-c or frama-c-gui.
2.
3.

Actual results:
zufa$ frama-c
[kernel] User Error: [findlib] package 'num' not found (required by `why3')
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
zufa$ 

Expected results:
Should work.

Additional info:
The why3 package isn't installed, but installing it doesn't change the problem.

The same problem exists in the released version Fedora 31.

Comment 1 Ben Cotton 2020-02-11 17:25:35 UTC
This bug appears to have been reported against 'rawhide' during the Fedora 32 development cycle.
Changing version to 32.

Comment 2 Fedora Update System 2020-03-27 23:59:36 UTC
FEDORA-2020-bc649d3429 has been submitted as an update to Fedora 32. https://bodhi.fedoraproject.org/updates/FEDORA-2020-bc649d3429

Comment 3 Ian Laurie 2020-03-28 00:50:22 UTC
I tested the Rawhide version frama-c-20.0-1.fc33 and I'm getting a very similar error as before.

rawhide# frama-c
[kernel] User Error: [findlib] package 'seq' not found (required by `why3')
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
rawhide# 

Could there be dependencies that aren't getting installed?  I installed just frama-c, which downloaded and installed 102 packages.

Comment 4 Fedora Update System 2020-03-28 14:59:47 UTC
FEDORA-2020-bc649d3429 has been pushed to the Fedora 32 testing repository.
In short time you'll be able to install the update with the following command:
`sudo dnf upgrade --enablerepo=updates-testing --advisory=FEDORA-2020-bc649d3429`
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2020-bc649d3429

See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.

Comment 5 Ian Laurie 2020-03-28 22:52:18 UTC
Installed from updates-testing onto Fedora 32 and exact same results:

fc32beta$ frama-c
[kernel] User Error: [findlib] package 'seq' not found (required by `why3')
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
fc32beta$

Is there something else I need to be doing/installing?  Is there a config file that needs tweaking *before* I try run it?

Comment 6 Jerry James 2020-04-03 22:43:19 UTC
Sorry, this has taken quite a lot of work to address.  I believe that once Richard Jones completes his current rebuild of all OCaml packages in Rawhide, that it will finally work in Rawhide.  If that is the case, then I will work my way back from there to the previous Fedora releases to get them patched up.  I'm going to let the update of comment 4 go stable, because it will fix dependency problems with coq in F32.  The update pusher will automatically close this bug, but I'll open it back up again until the problem is fully addressed.

I apologize for taking so long, but many of the delays involved were simply unavoidable.

Comment 7 Ian Laurie 2020-04-04 03:24:02 UTC
Please don't apologize, I really do appreciate the effort.  It will be great to see this package working in Fedora.

Comment 8 Fedora Update System 2020-04-05 00:16:20 UTC
FEDORA-2020-bc649d3429 has been pushed to the Fedora 32 stable repository.
If problem still persists, please make note of it in this bug report.

Comment 9 Jerry James 2020-04-09 20:10:38 UTC
Reopening, because it hasn't actually been fixed yet; see comment 6.

Comment 10 Fedora Update System 2020-04-09 20:53:46 UTC
FEDORA-2020-71d1e460e6 has been submitted as an update to Fedora 32. https://bodhi.fedoraproject.org/updates/FEDORA-2020-71d1e460e6

Comment 11 Jerry James 2020-04-10 18:59:34 UTC
I've been looking at the options for fixing this in Fedora 31.  There are really only 2:

1. Update the ocaml-zip package and rebuild everything that depends on it.
2. Remove zip support from the why3 package.

Since Fedora 31 is already halfway through its lifespan, I think #2 is the way to go.  I'll do the necessary builds today and submit an update.

Comment 12 Fedora Update System 2020-04-10 22:12:12 UTC
FEDORA-2020-4aff844684 has been submitted as an update to Fedora 31. https://bodhi.fedoraproject.org/updates/FEDORA-2020-4aff844684

Comment 13 Ian Laurie 2020-04-11 04:00:05 UTC
OK I looked at Fedora 31 first.  I still can't launch Frama-c but the error is different as follows:

abydos$ frama-c
[kernel] User Error: cannot load plug-in 'frama-c-jessie': cannot load module
  Details: interface mismatch on Types
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
abydos$ 

abydos$ rpm -qa | grep jessie
why-jessie-2.41-9.fc31.x86_64
abydos$ 

A couple of very minor observations:
(1) The why3.desktop file references an icon why3.png but this icon is nowhere on the system (there is a why.png referenced by jessie.desktop).
(2) Not sure how one can launch why3 from the menu because "Exec=why3 ide %f" seems to demand a file argument even though the help implies it is optional.  Maybe the program needs to prompt for one when none is provided?  This is more of an upstream issue I understand.

Comment 14 Fedora Update System 2020-04-11 18:51:08 UTC
FEDORA-2020-71d1e460e6 has been pushed to the Fedora 32 testing repository.
In short time you'll be able to install the update with the following command:
`sudo dnf upgrade --enablerepo=updates-testing --advisory=FEDORA-2020-71d1e460e6`
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2020-71d1e460e6

See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.

Comment 15 Fedora Update System 2020-04-11 22:50:13 UTC
FEDORA-2020-4aff844684 has been pushed to the Fedora 31 testing repository.
In short time you'll be able to install the update with the following command:
`sudo dnf upgrade --enablerepo=updates-testing --advisory=FEDORA-2020-4aff844684`
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2020-4aff844684

See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.

Comment 16 Ian Laurie 2020-04-12 01:25:52 UTC
For Fedora 32 beta my results are exactly the same as originally reported.

fc32beta$ frama-c
[kernel] User Error: [findlib] package 'num' not found (required by `why3')
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
fc32beta$ rpm -qa | grep frama-c
frama-c-20.0-2.fc32.x86_64
fc32beta$

Comment 17 Fedora Update System 2020-04-12 19:03:08 UTC
FEDORA-2020-71d1e460e6 has been submitted as an update to Fedora 32. https://bodhi.fedoraproject.org/updates/FEDORA-2020-71d1e460e6

Comment 18 Fedora Update System 2020-04-12 20:26:13 UTC
FEDORA-2020-4aff844684 has been submitted as an update to Fedora 31. https://bodhi.fedoraproject.org/updates/FEDORA-2020-4aff844684

Comment 19 Jerry James 2020-04-12 20:27:53 UTC
I think I finally understand the problem.  I've done new why3 builds in F31+ which should really, finally, fix the issue.

Comment 20 Fedora Update System 2020-04-13 18:32:14 UTC
FEDORA-2020-4aff844684 has been pushed to the Fedora 31 testing repository.
In short time you'll be able to install the update with the following command:
`sudo dnf upgrade --enablerepo=updates-testing --advisory=FEDORA-2020-4aff844684`
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2020-4aff844684

See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.

Comment 21 Fedora Update System 2020-04-13 21:17:12 UTC
FEDORA-2020-71d1e460e6 has been pushed to the Fedora 32 testing repository.
In short time you'll be able to install the update with the following command:
`sudo dnf upgrade --enablerepo=updates-testing --advisory=FEDORA-2020-71d1e460e6`
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2020-71d1e460e6

See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.

Comment 22 Ian Laurie 2020-04-14 02:26:35 UTC
Regarding comment #19 these have not yet made it to updates-testing correct?  At this time I see no changes after updating with updates-testing enabled.

Regarding f32, there is more on https://bodhi.fedoraproject.org/updates/FEDORA-2020-71d1e460e6 than I have installed (for frama-c).  Are there missing dependencies in frama-c or are these simply required rebuilds for other purposes, that is, not needed for a basic vanilla install of frama-c?

Comment 23 Ian Laurie 2020-04-15 03:59:43 UTC
On f32 ocaml-why3 just updated to ocaml-why3-1.3.1-4.fc32.x86_64 and the update brought in some extra ocaml package dependencies.

Frama-C now starts correctly on the f32 beta branch.

Comment 24 Fedora Update System 2020-04-22 23:23:34 UTC
FEDORA-2020-4aff844684 has been pushed to the Fedora 31 stable repository.
If problem still persists, please make note of it in this bug report.

Comment 25 Fedora Update System 2020-04-25 02:20:10 UTC
FEDORA-2020-71d1e460e6 has been pushed to the Fedora 32 stable repository.
If problem still persists, please make note of it in this bug report.


Note You need to log in before you can comment on or make changes to this bug.