Email Gateway (Sep 08 2023 at 11:22): Email Gateway (Sep 08 2023 at 11:22):From: "\"Kohlen, Bram (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
[Apologies if you receive this e-mail twice, I accidentally sent it to the wrong mailing list]
Hello mailing list,
I am currently trying out RC5 on a new laptop and found some unintuitive behaviour in isabelle components caused by the absence of "curl" on my Ubuntu 22.04 distribution. Adding the AFP (development branch) using "./isabelle components -u <path to afp-devel>/thys" initially seems to work, but upon inspection with "./isabelle components -l" I am getting the following:
Available components:
....
<path to afp_devel>/thys
<path to afp_devel>
Missing components:
HOME/.isabelle/contrib/hugo-0.88.1
HOME/.isabelle/contrib/ci-extras-2
somehow the path to afp_devel is added twice, once with /thys and once without. Both were not there before running the initial command. Also there is some missing components (hugo and ci-extras) that my proofs don't seem to depend on as everything still runs smoothly. Furthermore, when I now thy to add another component (for debugging/reproducibility purposes, I use the 2023 branch of the isabelle_llvm project: https://github.com/lammich/isabelle_llvm) using
"./isabelle components -u <path to isabelle_llvm>/thys" it will give the following message:
*** Bad Isabelle environment variable: "ISABELLE_CI_EXTRAS_JAR"
And it does not add the new component as shown by "./isabelle components -l"
I have explored the following workarounds:
* adding Isabelle_LLVM before adding the AFP will work. It still produces the same error after adding the AFP but at least it will allow me to run my project flawlessly.
* installing "curl" will allow Isabelle to automatically download the requested packages (hugo and ci-extras) when adding the AFP.
I also compared this behaviour to Isabelle2022, where this behaviour does not seem to occur (although the AFP is still added twice, once with the /thys and once without just like I observed in RC5).
I do think that this behaviour is unintentional. Especially not being able to add any new components after adding the AFP if one hasn't installed curl. I am also not sure what hugo and ci-extras are supposed to do here, for reference, ci-extras seems to consist mostly of .jar files. I am looking forward to read other opinions on this.
Kind regards,
Bram
Email Gateway (Sep 09 2023 at 11:31):From: Makarius <makarius@sketis.net>
On 08/09/2023 13:16, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users Mailing
List) wrote:
I am currently trying out RC5 on a new laptop and found some unintuitive
behaviour in isabelle components caused by the absence of "curl" on my Ubuntu
22.04 distribution. Adding the AFP (development branch) using "./isabelle
components -u <path to afp-devel>/thys" initially seems to work
[...]
Thanks for the detailed experience report. We have indeed accumulated a bit
too much complexity in the Isabelle + AFP setup. It all needs to be sorted out
soon in a coming release, and properly integrated into the Isabelle Prover IDE.
(I will start discussions about that on the isabelle-dev mailing list: we do
need to make clear which component dependencies for AFP are really necessary.)
Back to your text: reading it twice, I first got worried about the state in
Isabelle2023, which will become final and unchangeable in a few days.
Then I pretended to be a regular user of Isabelle2023-RC5 + AFP +
isabelle_llvm and managed to setup everything in half the time of reading +
worrying about the issue (of course, I know which diversions and pitfalls need
to be avoided).
So here is my summary:
* Isabelle releases like Isabelle2023-RC5 need the corresponding AFP
release: afp-2023 instead of afp-devel.
* Repository versions of Isabelle + AFP do need the "curl" command, as
stated in Isabelle/README_REPOSITORY --- and you need to do invoke
"Admin/init" until all components are saturated.
* Regular release versions of Isabelle + AFP neither need "curl" nor
"Admin/init". For Isabelle all required components are already built and
bundled. For AFP, components are suppressed, since they are "administrative"
only. The main download afp-current.tar.gz from
https://www.isa-afp.org/download worked for me on the spot without problems.
* Mixing release downloads with repository snapshots requires detailed
understanding of how things work. It is better to make a clear decision under
which regime you want to work: either release or repository.
Some of these extra details are as follows:
Available components:
....
<path to afp_devel>/thys
<path to afp_devel>somehow the path to afp_devel is added twice, once with /thys and once
without.
That is because AFP repository clones provide two components, and there is
some builtin smartness to add the second one automatically in certain situations.
Also there is
some missing components (hugo and ci-extras) that my proofs don't seem to
depend on as everything still runs smoothly.
"hugo-0.88.1" helps to produce the AFP websites: its absence or presence
normally does not get into the way.
"ci-extras" are a left-over from rather old times, and now I would say
"experimental" or even "obsolete". We need to find out how to put it into
proper form, or better eliminate it. ("ci-extras-2" introduces a reference to
some $ISABELLE_CI_EXTRAS_JAR that is required for the Isabelle/Scala setup of
AFP: without that it won't build.)
I have explored the following workarounds:
* installing "curl" will allow Isabelle to automatically download the
requested packages (hugo and ci-extras) when adding the AFP.
That is not a workaround, but a regular requirement for Isabelle + AFP
repository clones, to saturate components.
It is sad that Ubuntu has discontinued "curl" as default --- as it seems for
no particular reason. Some years ago, "curl" was considered bread-and-butter
for https access: I wonder what has happened there recently.
I also compared this behaviour to Isabelle2022, where this behaviour does not
seem to occur (although the AFP is still added twice, once with the /thys and
once without just like I observed in RC5).
afp-2022 also depends on "ci-extras", but it is "ci-extras-1" with slightly
different (non-canonical) setup. It happens to build, but the failure to
access the required jar is postponed to runtime. (In Isabelle, everything is
as "static" as possible, instead of "dynamic" or untyped/unscoped.)
I do think that this behaviour is unintentional. Especially not being able to
add any new components after adding the AFP if one hasn't installed curl.
The "curl" requirement is intentional. The rest is some overcomplexity that we
need to sort out on our side, but not for Isabelle2023.
Makarius
Email Gateway (Sep 09 2023 at 16:29):From: Fabian Huch <huch@in.tum.de>
The main problem here is that you are trying to compose a release
version of Isabelle with a development version of the AFP. In principle
this can work, but for development versions one does need to resolve
components (for Isabelle as well when using devel).
So most of the behaviour is expected, though I'll have to investigate
why both afp (in the devel version, this contains some tooling) and
afp/thys are added when you only added the afp/thys component - that
does not seem ideal.
Fabian
Email Gateway (Sep 12 2023 at 18:55):From: Makarius <makarius@sketis.net>
See also this changeset
changeset: 11878:3a9c2004b599
user: wenzelm
date: Sat Jun 05 20:44:59 2021 +0200
files: ROOTS thys/etc/settings
description:
more robust component setup for AFP/thys: support "isabelle components -u" and
init $AFP_BASE on demand;
no ROOTS in $AFP_BASE: proper support for "isabelle build -a" with $AFP_BASE
component, but without $AFP component;
This needs to be understood in the context of the isabelle-users thread "The
instructions in AFP's "Using Entries" do not work" from Jun-2021. E.g. see
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2021-06/msg00006.html
Makarius
Last updated: Apr 28 2024 at 16:17 UTC