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.
This bug appears to have been reported against 'rawhide' during the Fedora 32 development cycle. Changing version to 32.
FEDORA-2020-bc649d3429 has been submitted as an update to Fedora 32. https://bodhi.fedoraproject.org/updates/FEDORA-2020-bc649d3429
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.
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.
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?
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.
Please don't apologize, I really do appreciate the effort. It will be great to see this package working in Fedora.
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.
Reopening, because it hasn't actually been fixed yet; see comment 6.
FEDORA-2020-71d1e460e6 has been submitted as an update to Fedora 32. https://bodhi.fedoraproject.org/updates/FEDORA-2020-71d1e460e6
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.
FEDORA-2020-4aff844684 has been submitted as an update to Fedora 31. https://bodhi.fedoraproject.org/updates/FEDORA-2020-4aff844684
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.
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.
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.
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$
I think I finally understand the problem. I've done new why3 builds in F31+ which should really, finally, fix the issue.
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?
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.
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.
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.