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 _______________________________________________ devel mailing list -- devel@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to devel-leave@xxxxxxxxxxxxxxxxxxxxxxx
