On Wed, Aug 30, 2017 at 07:23:04PM -0600, Jerry James wrote:
BTW, most of the packages that sit on top of coq have new versions
available, so when this is fixed, I will want to update the other
packages anyway. If you could let me know when a fix for this issue
is available, I will take care of building everything else.
Sure.
>> (3) Disable the problematic coq modules. I'm not clear
if they are
>> necessary however, since I've only used Coq as an end user, I've never
>> delved into how it works.
Which ones are problematic? All of them?
It could be all of them. The first failure is:
rm -f theories/Init/Datatypes.glob
bin/coqtop -boot -native-compiler -compile theories/Init/Datatypes.v -noinit -R
theories Coq
File "./theories/Init/Datatypes.v", line 13, characters 0-38:
Error: while loading
/home/rjones/d/coq/plugins/syntax/nat_syntax_plugin.cmxs:
error loading shared library: /home/rjones/d/coq/plugins/syntax/nat_syntax_plugin.cmxs:
undefined symbol: camlLoc__3
(‘make -k’ doesn't get past this point)
The problem specifically is that we're carrying this patch:
https://github.com/ocaml/ocaml/pull/1268
which marks most global symbols that need to be loaded into registers
as ‘.hidden’. However this "over-hides", in this case hiding
camlLoc__3 (some anon function in the Loc module) which does actually
need to be public.
We need this patch to get OCaml to compile at all on aarch64, so the
answer is not to remove this patch, but to fix it in some other way.
Rich.
--
Richard Jones, Virtualization Group, Red Hat
http://people.redhat.com/~rjones
Read my programming and virtualization blog:
http://rwmj.wordpress.com
virt-top is 'top' for virtual machines. Tiny program with many
powerful monitoring features, net stats, disk stats, logging, etc.
http://people.redhat.com/~rjones/virt-top