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.
On 24 May 2025, at 08:07, Florian Weimer fw@deneb.enyo.de wrote:
- 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.
The polyc script only runs g++ to link executables. So I would imagine from the clue in the name that redhat-annobin-cc1 won’t have any effect on it. Also I don’t think “-g" affects linking.
The polyml default for CFLAGS is “-O3”. I think that’s probably belt-and-braces but it doesn’t seem inappropriate given what the ld man pages on Mac OS and linux say about the -O option (which is that you can do “-O0” to turn what optimisations it does off).
Experiments on Mac OS and Fedora indicate that the CFLAGS setting doesn’t make any significant difference to the generated object file.
Regards,
Rob.
Poly/ML mailing list -- polyml@lists.polyml.org To unsubscribe send an email to polyml-leave@lists.polyml.org
I stripped most flags out of the Makefile as Florian suggested and pushed some new Fedora builds. Your local Fedora mirror may have them already; if not, they should show up soon. Please try one of these builds and let me know if you have any further issues:
polyml-5.9.1-7.fc42 (for Fedora 42) polyml-5.9.1-6.fc41 (for Fedora 41)
On Mon, Jun 9, 2025 at 3:54 PM Rob Arthan rda@lemma-one.com wrote:
On 24 May 2025, at 08:07, Florian Weimer fw@deneb.enyo.de wrote:
- 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.
The polyc script only runs g++ to link executables. So I would imagine from the clue in the name that redhat-annobin-cc1 won’t have any effect on it. Also I don’t think “-g" affects linking.
The polyml default for CFLAGS is “-O3”. I think that’s probably belt-and-braces but it doesn’t seem inappropriate given what the ld man pages on Mac OS and linux say about the -O option (which is that you can do “-O0” to turn what optimisations it does off).
Experiments on Mac OS and Fedora indicate that the CFLAGS setting doesn’t make any significant difference to the generated object file.
Regards,
Rob.
Poly/ML mailing list -- polyml@lists.polyml.org To unsubscribe send an email to polyml-leave@lists.polyml.org
* Rob Arthan:
On 24 May 2025, at 08:07, Florian Weimer fw@deneb.enyo.de wrote:
- 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.
The polyc script only runs g++ to link executables. So I would imagine from the clue in the name that redhat-annobin-cc1 won’t have any effect on it. Also I don’t think “-g" affects linking.
I suppose it's slightly misnamed, redhat-annobin-cc1 and the cc1_options specs clause it contains is also used for cc1plus.
On 15 Jun 2025, at 18:56, Florian Weimer fw@deneb.enyo.de wrote:
- Rob Arthan:
On 24 May 2025, at 08:07, Florian Weimer fw@deneb.enyo.de wrote:
- 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.
The polyc script only runs g++ to link executables. So I would imagine from the clue in the name that redhat-annobin-cc1 won’t have any effect on it. Also I don’t think “-g" affects linking.
I suppose it's slightly misnamed, redhat-annobin-cc1 and the cc1_options specs clause it contains is also used for cc1plus.
I didn’t make myself clear: what I had in mind was that cc1 refers to the phase of the compiler that turns pre-processed source into assembler, so it runs prior to looking.
Regards,
Rob.
Poly/ML mailing list -- polyml@lists.polyml.org To unsubscribe send an email to polyml-leave@lists.polyml.org
-
Florian Weimer -
Jerry James -
Rob Arthan