Email Gateway (Mar 14 2023 at 11:42): Email Gateway (Mar 14 2023 at 11:42):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I am working with Isabelle/HOL on a fairly large development (tens of
thousands of lines of code). As part of our build process we have a CI
setup using a Docker container and Gitlab runners. Unfortunately, this has
suddenly started hanging after adding Word_Lib from the AFP as an
external dependency via the Isabelle components mechanism, as recommended
on the AFP website.
Mysteriously, this development builds locally on our Apple M1 Mac Pros that
we use for development but is now hanging when it is about to complete the
checking of one of our sessions (which is the first to use Word_Lib as a
dependency). There is nothing particularly complex about this session–––in
fact it is one of our simplest, as it merely consists of around five theory
files containing definitions and some modest theorems. It should not
therefore be particularly taxing to check. Nevertheless, CI now reliably
stalls when completing the checking of this session, as attested by running
isabelle build with the verbose flag option. This shows all theories in
the session (and those relevant in Word_Lib) being gradually checked by
Isabelle but then fails to progress any further in the build when it is
just about to complete checking. After one hour of stalled checking our CI
run times out–––the full development only takes approximately 30 minutes to
check locally.
We have tried bumping up the resource limits on the Gitlab runner to no
avail (it is running on our largest available runner with memory resources
far in excess of what our laptops offer). Both development and Gitlab
runner are using the same instruction set architecture (AArch64). I've
tried reducing the maximum number of parallel jobs down to the default and
that hasn't helped either.
Is there anything further that can be done to narrow down what, exactly, is
going wrong with the build?
Thanks,
Dominic
Email Gateway (Mar 14 2023 at 15:06):From: Fabian Huch <huch@in.tum.de>
You can always attach a debugger to the Isabelle/Scala JVM process and
see where it pauses.
Do you use the official docker image? If not, I would generally assume
that the environment in the container is misconfigured - e.g.,
file-system, user permission problems, missing system packages.
If you are using the official image, I would check if SElinux is
preventing files in the docker environment from being written
(temporarily disabling it may give you answers).
Fabian
Email Gateway (Mar 15 2023 at 10:33):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi Fabian,
Thanks for the suggestions. We are not using the official Docker image but
one that we developed ourselves. After more experimentation I'm fairly
confident that the problem is not in the Docker container. In the end I
managed to fix the hanging build by reconfiguring our build system to use
an AMD64 runner rather than AArch64 with no other changes. Obviously
the fix is confounded somewhat by the need to use a different build of
Isabelle, along with a different Ubuntu build–––and its attendant
userspace–––in the two containers, but it's somewhat suggestive that
there's something potentially deeper going on to cause the apparent
deadlock...
Thanks,
Dominic
Email Gateway (Mar 15 2023 at 11:56):From: Fabian Huch <huch@in.tum.de>
If that's the case, the problem is probably either a missing or broken
system package for the aarch64 environment. Generally, on an Ubuntu
container you would need something like:
- m4
- mercurial
- curl
- libgomp1
- libgmp-dev
- unzip
- swi-prolog
- lib32stdc++6
- texlive-full
- libzarith-ocaml
To run all Isabelle sessions. Often minimal docker images are missing
some of those. Maybe this helps.
Fabian
Email Gateway (Mar 15 2023 at 13:39):From: Makarius <makarius@sketis.net>
Recall that Isabelle arm64-linux/darwin still has experimental status: some
components are just missing, others are not as stable as we are used to for
x86_64.
Here are the cumulative NEWS announcements of the past releases on this topic:
New in Isabelle2022 (October 2022)
New in Isabelle2021-1 (December 2021)
New in Isabelle2021 (February 2021)
Experimental support for arm64-linux platform. The reference platform
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
Support for Apple Silicon, using mostly x86_64-darwin runtime
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
some native arm64-darwin executables (e.g. Java).
The "reference platform" is very important: so far, I only managed to get hold
on Raspberry Pi 4 (approx. 120 EUR). It would be better to have something like
Apple Studio in the backyard, to be used together with Linux on Docker.
The "almost complete support" still applies to Poly/ML: current repository
versions work well most of the time, but not always. A recent change by David
Matthews after the Isabelle2022 release improves the situation for really big
applications of native arm64 (instead of arm64_32), see also
https://isabelle-dev.sketis.net/rISABELLE014c3d00e0f
It might also help to upgrade Java: these guys are still in the progress to
polish ARM64 support. See also
https://isabelle-dev.sketis.net/rISABELLE39f8051f71d4
Note that there will be no "patch-releases" for Isabelle: it is a concession
to efficient use of our own resources.
If you want to use alternative components for regular Isabelle releases, the
simplest way is probably to use a repository clone (for the release, not an
arbitrary "latest" one), and make minimal changes to Admin/components/main.
Here is an example project to work with the Isabelle repository in such a
well-defined manner:
https://makarius.sketis.net/repos/narration/file/1c8aa0855611/README.md (it
also shows how to make your own Isabelle/Scala command-line tools.)
Makarius
Email Gateway (Mar 15 2023 at 14:14):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Yes, this was my working hypothesis when I decided to move us over to
AMD64–––namely we were seeing some potential instability owing to our use
of the relatively untested AArch64 platform. My colleagues and I have also
observed spurious failures of SMT solvers and the PolyML runtime
occasionally raising assertion failures in the garbage collector (from
memory), and this was the final push to move us onto AMD64 until things
have settled down further with Arm.
Fabian, when I come to try and move us back to Arm in the future I will
bear in mind that I need to include all of those components in the Docker
container.
Thanks!
Dominic
Email Gateway (Mar 15 2023 at 14:54):From: Makarius <makarius@sketis.net>
Some further side-remarks:
The regular "isabelle build_docker" tool provides some Isabelle/Scala entry
points that might be useful for manual setup of foreign Linux distributions.
E.g. like this via "isabelle scala":
scala> isabelle.Build_Docker.packages.mkString(" ")
val res1: String = curl less libfontconfig1 libgomp1 openssh-client pwgen
rsync unzip
scala> val res2: String = curl less libfontconfig1 libgomp1 openssh-client
pwgen rsync unzip libx11-6 libxext6 libxrender1 libxtst6 libxi6
texlive-fonts-extra texlive-font-utils texlive-latex-extra texlive-science
Mercurial is nice to have, e.g. to navigate history, but it requires Python3.
Plain "curl" is de-facto sufficient to get arbitrary version. See these links
for "hg archive" running on the server:
* tagged version:
https://isabelle.sketis.net/repos/isabelle/archive/Isabelle2022.tar.gz
* arbitrary version:
https://isabelle.sketis.net/repos/isabelle/archive/1ac2416e8432.tar.gz
* similar for AFP:
https://isabelle.sketis.net/repos/afp-2022/archive/...
https://isabelle.sketis.net/repos/afp-devel/archive/...
Isabelle tools like "isabelle version -i" work correctly for such repository
archive downloads. ("Rogue clones" on Github etc. don't work properly, because
formal versions are wrong.)
Makarius
Last updated: Apr 26 2024 at 01:06 UTC