My particular concern is about installing "coq" in Ubuntu 12.04 for Toshiba AC100 (armhf distro), which hasn't been built successfully for armhf, but is available for armel -- https://answers.launchpad.net/ac100/+question/218291.
So, can one install an armel Ubuntu package on armhf Ubuntu system, and will it work?
This should be possible with recent versions of Debian (≥ wheezy) or Ubuntu (≥ 11.10 oneiric), thanks to Multiarch support. The Debian packaging tools support installing packages from more than one architecture on the same system. You would be effectively installing two parallel systems, one with programs and libraries compiled for armhf and one with programs and libraries compiled from armel. Note that I'm not speaking from personal experience for the armel/armhf combination; it is supposed to work, but I don't know if all the bugs have been ironed out yet (the multiarch combination that gets the most attention is amd64/i386). There are success or experience reports: Linaro mailing list thread, blog post by cnxsoft.
Native code libraries are installed in different directories (/lib/arm-linux-gnueabi and /lib/arm-linux-gnueabihf/), so you can have both versions on your system, it's just a matter of disk space. Other files are installed in the same directory for every architectures, so you can only have one (e.g. all executables are in /bin or /usr/bin). In particular, if you need OCaml, I think you'll only be able to have the armel one or the armhf one.
Read the multiarch howto for how to set up your system (it's for Debian, but it should apply to setting things up manually on Ubuntu as well). First, declare armel as an additional architecture on your system:
echo foreign-architecture armel >> /etc/dpkg/dpkg.cfg.d/architectures
From wheezy/quantal onwards, run this instead:
dpkg --add-architecture armel
Then run apt-get update to download the package lists for the new architecture. To install the Coq package for armel:
apt-get install coq:armel
emacsen-common is an architecture-independent package, so the dependency should be already satisfied by having it installed. The problem is that the package manager needs to be told this. This is still the case in quantal. It's a bug in the package that can be trivially fixed by adding Multi-Arch: foreign to the package control fields. You can do this manually in /var/lib/dpkg/status (be careful not to break anything else), but you'd have to do this on every upgrade.
– Gilles
Jan 4 '13 at 20:54
/var/lib/dpkg/status: Package: emacsen-common Status: install ok installed Multi-Arch: foreign , but this doesn't help apt-get install coq:armel...
– imz -- Ivan Zakharyaschev
Jan 4 '13 at 22:44
apt-get reads from available, not from status. Manually editing available isn't going to work, it would be overwritten each time you run apt-get update. You could rebuild the packages (emacsen-common and whatever other package has the same issue), but you'd have to do that every time there's an upgrade (ok, there won't be many with this package). I think it would be easier to compile Coq manually, it's pretty straightforward if you have Ocaml working. Is Ocaml working (including the native code compiler)?
– Gilles
Jan 4 '13 at 22:55
/var/lib/dpkg/, I also had to make these edits for emacsen-common in /var/lib/apt/lists/ (ports.ubuntu.com_ubuntu-ports_dists_precise_main_binary-armel_Packages and ports.ubuntu.com_ubuntu-ports_dists_precise_main_binary-armhf_Packages) before it worked. Similar things are documented in ubuntuforums.org/showpost.php?p=12430257&postcount=6 .
– imz -- Ivan Zakharyaschev
Jan 4 '13 at 23:49
