libgnomecanvas disabled in brew

Unfortunately, the GTK gui is merely broken under macOS, even if you managed to install lablgtk or lablgtk3. You shall give a try to Ivette instead (EVA is supported, WP support is planned for near future).

added confirmed gui labels

Could you please detail how you tried to install Frama-C (opam install frama-c? Via a downloaded archive?), and which version (if you used opam, was it frama-c.26.0? Otherwise, opam update should show version 26 as available)?

The latest Frama-C release no longer uses gnomecanvas. It is based on lablgtk3. If you already have lablgtk installed in your opam switch, and/or you tried installing Frama-C 25 or older, opam will likely try to use it. If you do opam install lablgtk3, it should avoid trying to install gnomecanvas. However, as Loïc mentioned, the gtk GUI is currently broken on macOS (likely due to an upstream issue, but we were unable to get any feedback on it), even with lablgtk3.

By the way, we noticed it is possible to run a Frama-C Docker image with GUI on macOS (tested using XQuartz and Rancher Desktop). It's very cumbersome, but at the very least, there is a way to use the GTK-based Frama-C GUI on Mac, at least until Ivette is fully-featured.

Thank you! The version I tried to install is 24.0 and I used opam. I managed to finally install gnomecanvass through brew with a little trick so now frama-c 24.0 works on my machine. I just wanted to made you aware of the possible issue with previous versions depending on gnomecanvass.

Ah ok, thank you for sharing that. It's true that lack of such support will make our older releases uninstallable. Would you mind sharing the trick you used, if it could help others? We may consider adding it to the INSTALL.md file.

I am interested in using the GUI on MacOS. What Frama-C version does it support GUI? I have installed Frama-C 24.0, but it seems that there is no GUI there (or I don't know how to execute it).

Since you were asking how to install it, I will do it below. sorry if it is a bit messy, but the whole process has been a bit messy for me. Probably there is a better way of doing it, but my knowledge of the packaging structure of brew/opam is limited :-).

First, to override the limitation of installing libgnomecanvas, it is necessary to execute:

brew edit libgnomecanvas

and remove\comment the line disabling the package

disable! date: "2022-11-29", because: :repo_archived

Then I installed the necessary packages from brew:

brew install hg darcs opam gtk+ gmp gtksourceview3 libgnomecanvas autoconf

Then I installed autonconf pkgconfig and opam

brew install autoconf pkg-config opam

and I switch to Ocaml version 4.14.1 that is required by Frama-c 4.14.1. This actually creates some later conflict with Why3.

opam switch create 4.14.1

To install lablgtk3 it is necessary to add pkgconfig path from several libraries. I took this from https://frama-c.com/html/installations/titanium.html .

export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/usr/local/lib/pkgconfig

Since my machine is has an Apple Silicon SoC, I modified that variable to the directory where brew is installed in this architecture.

export PKG_CONFIG_PATH=/opt/homebrew/opt/libffi/lib/pkgconfig:/opt/homebrew/opt/libxml2/lib/pkgconfig:/opt/homebrew/lib/pkgconfig

Then I install why3 version 1.4.1

opam install zarith lablgtk3 lablgtk3-sourceview3 why3.1.4.1 why3-ide.1.4.1 alt-ergo.2.4.0

However, when doing Why3 config detect

I got an error related to some config file where why3 keeps the information about the provers. I am sorry but I didn't take note of it. The thing is that when I switched to Ocaml 4.14.1, packages are installed on a directory

~/.opam/4.14.1

But why3 config detect looks in ~/.opam/default

I don't know if there is a solution with specific opam commands. What I did was to move default to 5.0.0 and create a symbolic link default to 4.14.1. This worked :-)

Then I installed frama-c

opam install frama-c.24.0

But this couldn't be the end. It turns out that all this time the installation was using the stock make, which is a version lower than the one required by some configuration script during the installation of frama-c.

I overcome this by installing make from brew

brew install make

and adding to the path the directory where it is installed

export PATH=/opt/homebrew/opt/make/libexec/gnubin:$PATH

This did the trick!

But after all this, I still don't have GUI. According to the Frama-C manual, installing Frama-C gives the GUI. How do I get it in Frama-C 24.0, or what version do I need to install to get a GUI?

@titolo you wanted to install Frama-C 24.0 to have GUI, did you get it?

The reason why I want GUI is that I want to teach it in my module about verification, and I need WP. I won't needed it until October. Do you know if Ivette will be available by then? I can wait to provide an easier installation to the kids, but it would be good if I can play with the GUI to get use to the environment before the teaching.

Thank you very much for reading until here! (and of course for developing Frama-C!!!)

Cheers, David

Thank you for the detailed instructions on how you did it. I didn't know in particular that editing Homebrew was possible to re-enable libgnomecanvas. I tried the brew edit to remove that line, but even with that, I was unable to install the package (Error: libgnomecanvas has been disabled because it has an archived upstream repository). Then again, gnomecanvas is not strictly necessary for the Frama-C GUI (it was used only by Callgraph), so manual compilation might still work.

However, the main issue is that, even if we are able to compile the Frama-C GUI on macOS, we cannot run it anymore: it segfaults, and we are unable to precisely determine why. At first, this happened only with lablgtk3, so we used lablgtk2 as fallback; but for several months now, even that version is no longer working. Note that we are talking about the exact same code in our side; it seems that the changes happened on macOS itself (probably some of its libraries).

Due to the fact that macOS does not make it easy to "rollback" settings to a past state (as we can easily do on Linux with Docker, or on Windows using a virtual machine image, for instance), we do not even know exactly when that happened.

For several months now, we have been unable to run the Frama-C GUI in macOS, be it with lablgtk2 or lablgtk3. We filed an issue, but we didn't get a reply, and we seem to be the only application in this situation (CoqIDE, which also uses lablgtk, had some issues, but it is still working).

What's even worse with this situation, is that since the issues seem to have been caused by updates in macOS itself, we are unable to work even with old versions of the GUI, that were perfectly functional. It would be necessary to downgrade the macOS version itself to return to a previous working configuration.

We have tried a few times to rollback, but we were unable to get the GUI working. For instance, I just tried reinstalling Frama-C 24.0, but something has changed (possibly on my side), and I am getting compilation errors due to a missing sourceView2Enums.ml which I didn't have before (I did install conf-gtksourceview and the Homebrew gtksourceview).

For now, the only way I am able to run the Frama-C GUI in macOS, is by using Rancher Desktop (Docker) + XQuartz, which entails some complex commands. For instance, after running xhost +${localhost} to open connections, I can run the Frama-C GUI on local files as follows:

docker run -e DISPLAY=host.docker.internal:0 -v "$(pwd):/host" -w /host framac/frama-c-gui:26.1 frama-c-gui <files> <options>

These are not going to be very intuitive for students. But then again, if the goal is to teach students who will be using Linux in the end, that might be acceptable. If that seems useful, I might try documenting the procedure in more details.

Concerning Ivette, the WP part is under active development, and we hope it will be available as soon as possible. But I do not know if October is too early for that.

Hi Andre, thank you very much for your explanation.

I need to check my log to see what I did to install the package after editing the formula, maybe I added something else like installing from the source. Edit: after edit the formula, there is a warning from brew that says:

Warning: Unless HOMEBREW_NO_INSTALL_FROM_APIis set when runningbrew install, it will ignore your locally edited formula.

executing

export HOMEBREW_NO_INSTALL_FROM_API=true

does the trick

I understand better the problem now. Most students use Linux, but there is an increasing number of students with Apple Silicon-based machines, for which things are more difficult. I tried creating a virtual machine for an ARM Ubuntu distribution, but I faced some compilation errors during the installations and I moved to try something else. I will find what alternatives I have when the time comes.

Cheers, David

issues with Frama-C GUI on macOS are not only a matter of installing the packages. Installing GTK packages with brew is tractable (you need to export package paths...) and it works with lablgtk for Coq IDE and Why3 IDE, for instance. Compiling the Frama-C GUI from sources with lablgtk on macOS actually works, but the frama-c-gui then core dumps, immediately on after a while, which makes it not usable at all! This is why we disabled Frama-C GUI on macOS

We are working hard on a support for WP in Ivette. We plan to make it ready for mid 2023.

@lcorrenson Thank you very much. Indeed the installation of Frama-c in Linux is very smooth. I kidnap the thread to ask something (since I don't think it is an issue). I am trying to run the examples from Frama-C by examples. When I do make in any sorting algorithm I get the following:

Warning: Cannot open /home/david/.opam/4.14.1/share/frama-c/share/wp/coqwp
[cannot-open-path,filesystem]
File "./Shift_lemmas.v", line 3, characters 0-22:
Error: Cannot find a physical path bound to logical path Memory.

make[1]: *** [Makefile:12: Shift_lemmas.vo] Error 1
make: *** [../../Config/example.mk:40: ../../Drivers/driver] Error 2

It seems WP didn't install the coq libraries. I had initially installed coq 8.16.1 and I thought it would be because I was using a version that was too recent, but then I installed coq 8.15.0 and I am still facing the same error. Indeed, in .opam/4.14.1/share/frama-c/share/wp there is nothing related to coq (there is for why3).

Any idea of what I am doing wrong?

Thanks!

Frama-C by example has not been update since we have removed the native support of Coq. Today, the Coq part of the proof cannot be run anymore. I have a branch that was compatible with the Why3 Coq output, however, I believe that the scripts used to generate all proofs do not work anymore. Maybe I can have a look to ACSL by example to restore scripts but I don't when I'll be able to do that ...

by the way, the same problem applies for the WP tutorial which still uses the native output to Coq. The next-version branch has been partially updated for this but I plan to update the version of Alt-Ergo to use and it still has a few regressions that should be fixed before I can really finish the update.

I see... Well, on the bright side, everything was correctly installed from my side. I understand that it is very difficult to maintain proofs when the environment changes this fast (and I also understand the environment changes that fast considering how the verification technologies also evolve). So thank you very much for replying to my kidnapping message! I will try to do it as a "self-assignment", if time allows!

Thanks everybody for the fantastic work!

Closing:

GTK2 (thus gnomecanvas) non supported anymore
GTK3 will not receive active development anymore (moving to Ivette).

closed

mentioned in issue #2661

libgnomecanvas disabled in brew

Child items ...

Activity