Dear All,
I have been trying to get ProofPower to work under Linux on Apple Silicon using UTM and have a working build now. I have a pre-built VM for Fedora 41 and installed the various packages that ProofPower depends on. I was very pleased that the packages for Poly/ML were there and working, but did notice one missing dependency at the first point that the ProofPower make files try to run polyc
echo "use"polyml-build.sml";" | poly > slrp-bin.log 2>&1 polyc -o slrp-bin slrp-bin.o g++: fatal error: cannot read spec file '/usr/lib/rpm/redhat/redhat-annobin-cc1': No such file or directory
The fix was to install the package redhat-rpm-config. What I found particularly odd is that I had checked by hand that gcc was working before I started the ProofPower build and the ProofPower build had successfully compiled some C programs before this failure and has been successfully running poly (as you can see above). So this seems to be something specific to polyc.
I thought I’d mention this here (a) in case anyone else comes across the same problem with polyc and wants a fix and (b) because it looks there are some dependencies between packages that are missing in the packages for Poly/ML on this distro (which I can report if understand a bit better what is going on).
Regards,
Rob.
Hi Rob,
Sorry for the late reply. I've been traveling and am finally catching up on email.
On Thu, May 15, 2025 at 4:36 PM Rob Arthan rda@lemma-one.com wrote:
I have been trying to get ProofPower to work under Linux on Apple Silicon using UTM and have a working build now. I have a pre-built VM for Fedora 41 and installed the various packages that ProofPower depends on. I was very pleased that the packages for Poly/ML were there and working, but did notice one missing dependency at the first point that the ProofPower make files try to run polyc
echo "use"polyml-build.sml";" | poly > slrp-bin.log 2>&1 polyc -o slrp-bin slrp-bin.o g++: fatal error: cannot read spec file '/usr/lib/rpm/redhat/redhat-annobin-cc1': No such file or directory
The fix was to install the package redhat-rpm-config. What I found particularly odd is that I had checked by hand that gcc was working before I started the ProofPower build and the ProofPower build had successfully compiled some C programs before this failure and has been successfully running poly (as you can see above). So this seems to be something specific to polyc.
I thought I’d mention this here (a) in case anyone else comes across the same problem with polyc and wants a fix and (b) because it looks there are some dependencies between packages that are missing in the packages for Poly/ML on this distro (which I can report if understand a bit better what is going on).
I maintain the Fedora polyml package. All Fedora packages are built with a standard set of flags, including "-specs=/usr/lib/rpm/redhat/redhat-annobin-cc1" to build binaries with annobin (https://sourceware.org/annobin/). The polyml build stashes the flags that were used to build polyml itself into polyc; see the CFLAGS definition. I could use some guidance here. We can do one of two things.
1. Make polyml depend on redhat-rpm-config. This will make polyc build binaries with the same flags used to build Fedora packages. This may or may not be desirable.
2. We can do some trickery in the polyml package build to trim CFLAGS in polyc down to a minimal set (which set?).
What would the users of polyml on Fedora prefer?
* Jerry James:
I maintain the Fedora polyml package. All Fedora packages are built with a standard set of flags, including "-specs=/usr/lib/rpm/redhat/redhat-annobin-cc1" to build binaries with annobin (https://sourceware.org/annobin/). The polyml build stashes the flags that were used to build polyml itself into polyc; see the CFLAGS definition. I could use some guidance here. We can do one of two things.
There's a variant of %build_cflags called %extension_cflags. It contains just flags that can be hard-coded into build tools because they do not have dependencies on separate files. It would have to be used in addition to polyml's own defaults (which presumably includes -O2 -g at least), unlike %build_cflags.
-
Florian Weimer -
Jerry James -
Rob Arthan