compilation of Frama-C 25.0~beta does not stop on macOS

Could you use --verbose in opam in order to pinpoint the problematic command?

I ran opam install --verbose frama-c &> frama.out and interrupted the build after about an hour.

It appears to hang at Generating /Users/jens/.opam/4.13.1/.opam-switch/build/frama-c.25.0~beta/lib/plugins/top/Metrics.mli

Attached is the log.

frama.out

I just tried on my Mac Mini 10.15.7, with opam 2.0.8, and a 4.13.1, but I couldn't reproduce it. In my case, it was able to proceed until the end.

The lines after the last ones in your build log are calls to ocamldep, with the generation of a .depend file at the end. We did see, in some rare occasions, some instances of infinite looping related to the generation of .depend files in macOS, but we were never able to investigate them closely, since usually make clean or something similar would make them disappear. They seemed related to file timestamps, and could possibly be related to the old Make binaries shipped with macOS ; since I replaced my BSD make with GNU make, that could explain why I'm unable to reproduce it.

When compiling Frama-C manually from the source, we were able to avoid the issue by running make depend explicitly before make on macOS, but without editing the opam file directly, I don't know how to do it for the opam package version.

We could try adding the make depend step to the opam file:

 build: [
   ["autoconf"] {dev}
   ["./configure" "--prefix" prefix
                  "--mandir=%{man}%"
   ]
+  [make "depend"]
   [make "-j%{jobs}%"]
   [make "-C" "doc" "download"] {with-doc}
 ]

But it doesn't help understand why it happens, and why only in rare occasions. And I'm not even sure the issue you are having is related to it.

Also, this will likely disappear when we switch to Dune.

If you have an easy way of testing whether the modified opam file helps, that could be a quick workaround. Otherwise, maybe erasing the temporary directory where opam builds it (I assume it already does that, but I'm not sure) could reset the file timestamps and help them work? Otherwise, Loïc will possibly have better recommendations.

@gerlach, the addition of [make "depend"] can be done in a specific branch that can be pinned before performing the command opam install frama-c.

Just a short remark: In my case the infinite loop occurs always. By no means rarely.

Ok, I'll see if I can reproduce it. Could you please confirm if you are using macOS' default make (make --version should return 3.81, I believe), or if you aliased it to GNU make (Homebrew usually proposes it as an option, besides the usual gmake)?

Also, it might be useful to get your GCC (Clang, in fact) version, via gcc -v.

Indeed, make is aliased to gmake and gmake has version 4.3
gcc -v produces

Apple clang version 13.1.6 (clang-1316.0.21.2.5)
Target: x86_64-apple-darwin21.5.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

I'm not very used to macOS, so I'm having a hard time finding out how to upgrade to clang 13 (I'm on clang 11, and even after updating to Monterey, I do not find a way to update the tools... SO and similar sites contain lots of commands, but none seem to work).

In any case, I think we'll try the "pin a specific branch" approach, with a make depend command.

Could you please try opam pin add git@git.frama-c.com:pub/frama-c.git#fix/make-depend-macos and see if it helps? I just pushed the branch, based on stable/manganese.

By the way, there are a few non-public fixes since the beta release, so if the compilation works for you in that branch, please tell us so I will push the fixes to that branch as well. This should allow you testing with a more recent version.

I have exactly the same version of gcc on my mac and it works perfectly with Frama-C.

My GNU make version is also the same and it works...

Is there any other GNU-like tool involved during the make depend step ? Does the problem persist after a ./bin/rebuild.sh (the script performs a deep clean, reconfigure and rebuild) ?

I guess @gerlach tried installing directly via opam, so he cannot run scripts in bin. But completely erasing the /Users/jens/.opam/4.13.1/.opam-switch/build/frama-c.25.0~beta/ directory (if it exists) might have an equivalent effect. But I guess this directory only exists in my computer because I had a opam pin add at a given moment; I don't know if opam keeps caches of packages built normally. I think it rebuilds from scratch when a new opam install is executed.

I think it rebuilds from scratch when a new opam install is executed.

I believe so.

The problem persists with the Frama-c 25.0 release.

We did not merge the proposed patch above because we were not sure it would fix anything, so it's expected that the final release behaves the same. However, were you able to test the command opam pin add git@git.frama-c.com:pub/frama-c.git#fix/make-depend-macos as suggested above? We can still patch the opam file on the opam repository if it helps.

Could you also tell us what version of bash you're using? In the log the line

src/plugins/value/gen-api.sh: line 25: ${module^}: bad substitution

is quite suspicious, and this script explicitly requires bash

Good point. macOS uses zsh as default shell and I have switched to it about two years ago.

You mean you don't have bash installed at all? The script mentioned above explicitly asks about it via /usr/bin/env bash, thus I'd say that the error message would be quite different if there were no bash on the system.

After some digging into bash's Changelog, the ^ case conversion operator appeared in bash 4.0, which comes also with a licence change to GPLv3, so that Apple will probably never upgrade, although newer versions are certainly available via homebrew.

I have a pretty old version

bash --version
GNU bash, version 3.2.57(1)-release (x86_64-apple-darwin21)
Copyright (C) 2007 Free Software Foundation, Inc.

Using brew I have installed

bash --version
GNU bash, version 5.1.16(1)-release (x86_64-apple-darwin21.1.0)

Now the compilation succeeds! Thanks a lot to all!

OK, thanks for the feedback.

Thanks Jens. In any case, we adapted a script which used Bash 4 features to ensure it also works with macOS's standard bash (3.2). That script might have been a cause of this issue.

mentioned in merge request !7 (closed)

closed

compilation of Frama-C 25.0~beta does not stop on macOS

Child items ...

Activity