[isabelle] Isabelle/OPAM

[Lars Hupel]

I'm circling back to an old email thread about OCaml support in
Isabelle:
<https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2018-May/007874.html>

The consensus, as far as I understood it, was to bundle OPAM as an
Isabelle component.

While Ubuntu 18.04 LTS still ships a "good" compiler version (4.05.0), I
think this is unfinished business and should be addressed. I'm pretty
sure Ubuntu 19.04 will ship a newer version, and people on other
platforms like Arch, Fedora and macOS may already have one that doesn't
work. Additionally, while preparing distribution upgrades through our
chair infrastructure, I'd really like to have a dependable OCaml version.

I have prepared a component that attempts to do just that:

<https://github.com/larsrh/isabelle-opam>

Steps to use it:

1) Clone the repository.
2) Run "./get_opam.sh", which will download the latest OPAM version
(2.0) for all supported platforms and verifies the checksum.
3) Register as a component in "~/.isabelle/etc/components".
4) Run "isabelle opam_setup".
5) To try it out, build the session "HOL-Codegenerator_Test", which
should successfully build the theory "Code_Test_OCaml".

This will:
- automatically set the "ISABELLE_OCAML" and "ISABELL_OCAMLC" variables
- provide the Isabelle tools "ocaml" and "ocamlc"
- upon use, download and install OCaml 4.05.0 into "~/.isabelle/opam" so
that it doesn't interfere with any user installation
- read the "ISABELLE_OCAML_VERSION" variable and pick the compiler
version accordingly

(Un)known issues:
- may not be thread-safe (to be investigated; it appears that OPAM locks
its workspace)
- can't install packages yet (like "zarith"), but for 4.05.0 that's
unproblematic

All the heavy lifting is done by OPAM, which means the component just
has maybe 70 lines of scripts.

So far, I have not yet uploaded this to
<https://isabelle.in.tum.de/components/>, and I don't plan to do that
just yet.

Next: Packaging stack, because the Haskell version mess is even bigger
than for OCaml.

[Makarius]

Post by Lars Hupel
The consensus, as far as I understood it, was to bundle OPAM as an
Isabelle component.
<https://github.com/larsrh/isabelle-opam>

I will take a look at it soon -- I would like to understand how OPAM
works, and see how to fit it perfectly into the Isabelle environment.

Post by Lars Hupel
Next: Packaging stack, because the Haskell version mess is even bigger
than for OCaml.

That is another old question. As it happens, I've just had problems with
the slightly odd AFP/HLDE session and its Haskell code generation and
compilation (I did not pin them down yet).

Moreover, someone else approached me to connect Isabelle to Haskell in a
better way. I still have no idea how distribution packaging really works
in that community, but I will look through this in the coming days.


There is another meta-problem: we need to formalize maintenance of
Isabelle components better, such that (1) all administrative sources are
in Admin/components/ in the Isabelle repository, (2) preferably tools in
Isabelle/Scala instead of odd shell scripts (e.g. see "isabelle
build_jdk"), and (3) somehow automated multi-platform builds on one of
these continuous-testing platforms (without introducing a strong
dependence on big commercial players that are coming and going over the
years).


Makarius

[Lars Hupel]

Post by Makarius
I will take a look at it soon -- I would like to understand how OPAM
works, and see how to fit it perfectly into the Isabelle environment.

In the meantime I have received some hints from an OCaml expert. In
principle this should work, but of course it requires some actual
"battle testing" by users.

Post by Makarius
There is another meta-problem: we need to formalize maintenance of
Isabelle components better, such that (1) all administrative sources are
in Admin/components/ in the Isabelle repository, (2) preferably tools in
Isabelle/Scala instead of odd shell scripts (e.g. see "isabelle
build_jdk"), and (3) somehow automated multi-platform builds on one of
these continuous-testing platforms (without introducing a strong
dependence on big commercial players that are coming and going over the
years).

(3) is probably the hardest issue. There are some big players in the
market of hosted continuous integration and build services, but the
multi-platform aspect is usually lacking.

Currently, I'm only aware of two free services that can produce macOS
and Windows binaries; these are Travis CI and Appveyor, respectively.
Both have been around for a while and offer only low-end virtual
machines. For compiling components, they should be sufficient, though.

Linux has many more options. Travis CI can build Linux, as can its
direct competitors Circle CI and Drone. But there's also openSUSE Build
Service that offers many distributions.

I don't really see a problem with relying on third-party vendors here:
if one of them disappears, we'd have to migrate. That's still better
than what we have now, by requiring component authors to assemble
binaries from various machines with only incidental, i.e. not managed,
configuration.

[Makarius]

Post by Lars Hupel
if one of them disappears, we'd have to migrate. That's still better
than what we have now, by requiring component authors to assemble
binaries from various machines with only incidental, i.e. not managed,
configuration.

The "managed configuration" appears to be a selling point for these
services, but we've never had real problems without it. I can understand
why people out there use it, but for us it is irrelevant.


Makarius

[Lars Hupel]

Post by Makarius
The "managed configuration" appears to be a selling point for these
services, but we've never had real problems without it. I can
understand
why people out there use it, but for us it is irrelevant.

It's very much relevant, and we do (and did) have real problems with
incidental configuration. The initial email in this thread is evidence
of that.

[Lars Hupel]

Post by Lars Hupel

Post by Makarius
The "managed configuration" appears to be a selling point for these
services, but we've never had real problems without it. I can understand
why people out there use it, but for us it is irrelevant.

It's very much relevant, and we do (and did) have real problems with
incidental configuration. The initial email in this thread is evidence
of that.

Additionally, the entire concept of packaged Isabelle components is an
attempt to avoid incidental configuration.

[Makarius]

Post by Lars Hupel

Post by Lars Hupel

Post by Makarius
The "managed configuration" appears to be a selling point for these
services, but we've never had real problems without it. I can understand
why people out there use it, but for us it is irrelevant.

It's very much relevant, and we do (and did) have real problems with
incidental configuration. The initial email in this thread is evidence
of that.

Additionally, the entire concept of packaged Isabelle components is an
attempt to avoid incidental configuration.

The concept of Isabelle components is somehow "polymorphic" over a range
of OS versions, with minimal assumptions about the target platform.

Its own build process requires a few more assumptions, but not very
much, e.g. a certain OS version that is not too old nor too young.
Usually we've had just some odd machines around the corner that were
available for builds, and used by many other things as well.

The general model is that Isabelle (or its administrative build tasks)
provide their own critical requirements in a mostly self-contained way.


Makarius

[Makarius]

Post by Lars Hupel
<https://github.com/larsrh/isabelle-opam>

I have briefly looked through this: it looks mostly fine, but there are
also some odd details that need to be revisited. I will come back to
this later: next week I will discuss with some Isabelle users Haskell,
not OCaml/OPAM. Afterwards it should be clearer what is abstractly
required, and how OCaml and Haskell can be unified within Isabelle
eventually.

Post by Lars Hupel
- may not be thread-safe (to be investigated; it appears that OPAM locks
its workspace)

That is not a problem. System configuration (e.g. "isabelle components
-a") is done outside the running Isabelle application, with an implicit
assumption that nothing bad happens concurrently. We even have that
assumption for "isabelle build".

Post by Lars Hupel
- can't install packages yet (like "zarith"), but for 4.05.0 that's
unproblematic

That is a high-level question how Isabelle code generation uses proper
integers. I don't know what is really canonical in terms of OCaml.

Post by Lars Hupel
Next: Packaging stack, because the Haskell version mess is even bigger
than for OCaml.

I have started using the Haskell "stack" tool and actually like it. It
looks like a professional tool, where everything just works and no
tinkering is required: e.g. I could build a demo application on Linux,
Mac OS X, Windows on the spot, without even thinking about the usual
problems.

Now I only need to tinker with VSCode to get a Haskell IDE. That
platform seems to be defined for old-fashioned Emacs/vi-like tinkering ...


Makarius

[Lars Hupel]

Post by Makarius
That is not a problem. System configuration (e.g. "isabelle components
-a") is done outside the running Isabelle application, with an implicit
assumption that nothing bad happens concurrently. We even have that
assumption for "isabelle build".

True, but "isabelle build" (and PIDE) may call out to "isabelle ocaml"
multiple times in parallel. That's the issue here. Currently I have set
it up that every call to "isabelle ocaml" will install the necessary
OCaml version if not present. This may end up installing OCaml in
parallel. But this can easily be changed to just *check* the presence
and bail out if it's absent.

Post by Makarius
That is a high-level question how Isabelle code generation uses proper
integers. I don't know what is really canonical in terms of OCaml.

What we do right now is acceptable until 4.05.0. After that, the new
thing, as far as I understand it, is "zarith", but the legacy "num" is
still available as a package: <https://opam.ocaml.org/packages/num/>

[Makarius]

Post by Lars Hupel

Post by Makarius
That is not a problem. System configuration (e.g. "isabelle components
-a") is done outside the running Isabelle application, with an implicit
assumption that nothing bad happens concurrently. We even have that
assumption for "isabelle build".

True, but "isabelle build" (and PIDE) may call out to "isabelle ocaml"
multiple times in parallel. That's the issue here. Currently I have set
it up that every call to "isabelle ocaml" will install the necessary
OCaml version if not present. This may end up installing OCaml in
parallel. But this can easily be changed to just *check* the presence
and bail out if it's absent.

That is one of the open problems: it is generally fragile to make a
dynamic installation of a tool that pretends to be there, but isn't.
There could be many other odd effects, such as bad or absent network
connection.

Anyway, I will continue looking at how these things work ("opam" and
"stack"). At the end it should be plain and simple and robust as usual.

(BTW, I failed to setup any Haskell IDE for VSCode. It shows that these
guys still have a lot of fundamental problems to solve.)


Makarius

[Makarius]

Post by Lars Hupel
The consensus, as far as I understood it, was to bundle OPAM as an
Isabelle component.
<https://github.com/larsrh/isabelle-opam>
1) Clone the repository.
2) Run "./get_opam.sh", which will download the latest OPAM version

Back to the start of this thread.

First note that x86-linux is actually obsolete for Isabelle: the
underlying OS will always be x86_64.

Did you find a proper Windows version of OPAM anywhere? It seems to be
in the making, maybe some of these OCaml support companies already have
it. If not, we need to modify the plan slightly, to make a more abstract
"ocaml_setup" tool for Isabelle that will do something else for
Windows/Cygwin (which we bundle anyway).


Makarius

[Lars Hupel]

Post by Makarius
Did you find a proper Windows version of OPAM anywhere? It seems to be
in the making, maybe some of these OCaml support companies already have
it. If not, we need to modify the plan slightly, to make a more abstract
"ocaml_setup" tool for Isabelle that will do something else for
Windows/Cygwin (which we bundle anyway).

I tried to, but I didn't find anything satisfactory. Everybody keeps
saying "experimental", "soon" etc.

There's this question on Stack Overflow
<https://stackoverflow.com/q/39560241> with one promising answer but
also one demotivating comment:

"OCaml has many builds for Windows. Cygwin, MinGW, MSVC and now even for
Bash on Windows. Each has its own glitches."

I guess with Windows 10 there's also WSL thrown into the mix.

[Lars Hupel]

Post by Lars Hupel
I tried to, but I didn't find anything satisfactory. Everybody keeps
saying "experimental", "soon" etc.

After sending this message I realized I could look at the Cygwin package
list, and they have it:

https://cygwin.com/cgi-bin2/package-cat.cgi?file=x86_64%2Fopam%2Fopam-1.2.2-2&grep=opam

However, I have no clue how simple it is to programmatically install a
Cygwin package; nor whether this package works well.

[Makarius]

Post by Lars Hupel

Post by Lars Hupel
I tried to, but I didn't find anything satisfactory. Everybody keeps
saying "experimental", "soon" etc.

After sending this message I realized I could look at the Cygwin package
https://cygwin.com/cgi-bin2/package-cat.cgi?file=x86_64%2Fopam%2Fopam-1.2.2-2&grep=opam
However, I have no clue how simple it is to programmatically install a
Cygwin package; nor whether this package works well.

I was too implicit about Cygwin: there is already Isabelle support for
it, as part of the normal application bundling. It would be trivial to
include OCaml from the outset, but it is probably too big.

Adding it later might be feasible: it needs one or too close looks at
existing batch files.

Generally, this multi-platform bundling of Isabelle is a delicate art:
it has evolved in the past 10 years to a relatively sophisticated state.


Makarius

[Lars Hupel]

Post by Makarius
I was too implicit about Cygwin: there is already Isabelle support for
it, as part of the normal application bundling. It would be trivial to
include OCaml from the outset, but it is probably too big.

I meant just opam. I agree that OCaml is too big, but bundling just opam
should be feasible, no?

[Makarius]

Post by Lars Hupel

Post by Makarius
I was too implicit about Cygwin: there is already Isabelle support for
it, as part of the normal application bundling. It would be trivial to
include OCaml from the outset, but it is probably too big.

I meant just opam. I agree that OCaml is too big, but bundling just opam
should be feasible, no?

I will try it ...


Makarius

[Makarius]

Post by Lars Hupel
"OCaml has many builds for Windows. Cygwin, MinGW, MSVC and now even for
Bash on Windows. Each has its own glitches."
I guess with Windows 10 there's also WSL thrown into the mix.

Yes, I've seen that, too.

Isabelle and WSL is still an open question: right now it is not
supported, but it might at some point help out of such situations.

(I propose to close this thread here, and move the discussion over to
the isabelle-dev thread about "AFP/HLDE", or other new threads.)


Makarius

[w***@cs.princeton.edu]

I'd like to add an encouraging note about OPAM on Windows: the version at
https://fdopen.github.io/opam-repository-mingw/installation/ (the first one
mentioned in the StackOverflow question) has served me well for several
years, and I don't think it's considered experimental any longer.

Regards,
William

-----Original Message-----
From: cl-isabelle-users-***@lists.cam.ac.uk
<cl-isabelle-users-***@lists.cam.ac.uk> On Behalf Of Lars Hupel
Sent: Sunday, October 7, 2018 3:23 PM
To: Makarius <***@sketis.net>
Cc: cl-isabelle-***@lists.cam.ac.uk
Subject: Re: [isabelle] Isabelle/OPAM

Post by Makarius
Did you find a proper Windows version of OPAM anywhere? It seems to be
in the making, maybe some of these OCaml support companies already
have it. If not, we need to modify the plan slightly, to make a more
abstract "ocaml_setup" tool for Isabelle that will do something else
for Windows/Cygwin (which we bundle anyway).

I tried to, but I didn't find anything satisfactory. Everybody keeps saying
"experimental", "soon" etc.

There's this question on Stack Overflow
<https://stackoverflow.com/q/39560241> with one promising answer but also
one demotivating comment:

"OCaml has many builds for Windows. Cygwin, MinGW, MSVC and now even for
Bash on Windows. Each has its own glitches."

I guess with Windows 10 there's also WSL thrown into the mix.