Email Gateway (Oct 01 2024 at 09:58): Email Gateway (Oct 01 2024 at 09:58):From: "\"He, Shuhan\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,
I would like to run Isabelle on my Linux system based on musl libc, but the
binary distribution from https://isabelle.in.tum.de/ assumes glibc and would
not work at all on musl. Are there instructions on building Isabelle from
source?
Thanks,
Shuhan
Email Gateway (Oct 02 2024 at 13:02):From: Makarius <makarius@sketis.net>
On 01/10/2024 05:54, "He, Shuhan" (via cl-isabelle-users Mailing List) wrote:
I would like to run Isabelle on my Linux system based on musl libc
Why?
the binary distribution from https://isabelle.in.tum.de/
<https://isabelle.in.tum.de/> assumes glibc and would
not work at all on musl.
There are probably a more implicit dependencies. The idea is that you have a
regular Linux box, e.g. Ubuntu with the usual things available (or macOS or
Windows).
Are there instructions on building Isabelle from source?
This question is ill-typed --- it does not make any sense to ask it nor to
answer it.
Makarius
Email Gateway (Oct 03 2024 at 13:12):From: Cobalt <cobalt@cobalt.rocks>
On October 2, 2024 12:56:39 PM UTC, Makarius <makarius@sketis.net> wrote:
On 01/10/2024 05:54, "He, Shuhan" (via cl-isabelle-users Mailing List) wrote:
I would like to run Isabelle on my Linux system based on musl libc
Why?
the binary distribution from https://isabelle.in.tum.de/ <https://isabelle.in.tum.de/> assumes glibc and would
not work at all on musl.There are probably a more implicit dependencies. The idea is that you have a regular Linux box, e.g. Ubuntu with the usual things available (or macOS or Windows).
You should be able to get most thing running on a musl-based distro but yymv for more complex components like poly/ml. The official releases tar balls won't be usable because they heavily rely on a FHS system with glibc.
My recommendation would be to use nix or a container as intermediate solution unless you want to invest significant time into getting Isabelle to run directly.
Are there instructions on building Isabelle from source?
This question is ill-typed --- it does not make any sense to ask it nor to answer it.
Please be less snarky, the question is understandable.
The Systems documentation does contain some approximate instructions on how to setup an environment for Isabelle: <https://isabelle.in.tum.de/dist/Isabelle2024/doc/system.pdf>
This should give you a rough outline on the base requirements for _running_ Isabelle.
There does not currently exist a comprehensive set of instructions of how to build Isabelle and all components contained in a release from Source.
Isabelle does contains it's own build system for this but it is not well documented. The source repository contains some shell scripts for building/ preparing an Isabelle release see the Admin/ directory in: <https://isabelle-dev.sketis.net/source/isabelle/>
Best regards
Cobalt
Email Gateway (Oct 03 2024 at 21:04):From: Makarius <makarius@sketis.net>
On 02/10/2024 15:25, Cobalt wrote:
Are there instructions on building Isabelle from source?
This question is ill-typed --- it does not make any sense to ask it nor to answer it.
Please be less snarky, the question is understandable.
The Systems documentation does contain some approximate instructions on how to setup an environment for Isabelle: <https://isabelle.in.tum.de/dist/Isabelle2024/doc/system.pdf>
This should give you a rough outline on the base requirements for _running_ Isabelle.
There does not currently exist a comprehensive set of instructions of how to build Isabelle and all components contained in a release from Source.
Isabelle does contains it's own build system for this but it is not well documented. The source repository contains some shell scripts for building/ preparing an Isabelle release see the Admin/ directory in: <https://isabelle-dev.sketis.net/source/isabelle/>
This attempt of an answer is ill-typed, and leading into the wrong direction.
You need to think about Isabelle in rather different ways: it consists of many
components from different cultures all fit together tightly, with minimal
assumptions about the external environment. Thus it does the job of docker and
nix to some extent, although Isabelle is a bit older than these.
Everything is integrated via Isabelle/Scala running on the JVM: there are no
"scripts" to assembly things, but well-typed Scala programs. We do have such
an Isabelle/Scala build tool almost every Isabelle component, to reproduce the
binaries within a certain OS context. Some other components are assembled
manually for historic reasons. Note every bit and piece can be reconstructed
from source alone.
General administrative notes about Isabelle componenents are in
Admin/components/README.md --- but nothing of that is relevant to Isabelle
end-users, only to produces of components.
Sometimes people disagree with this level of sophistication and ambition in
Isabelle system integration. Which leads us back to my initial question:
"Why?" (This should be answered first.)
Makarius
Last updated: Jan 04 2025 at 20:18 UTC