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.
