Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Isabelle repository version, problems star...

Email Gateway (Mar 12 2021 at 12:23):

From: Peter Lammich <lammich@in.tum.de>
Hi,

I'm trying to start the Isabelle repo version, but only get as far as

peter@peterXps:~/devel/Isabelle-devel$ ./bin/isabelle

Building Isabelle/Scala ...

Unknown JAVA_HOME

Email Gateway (Mar 12 2021 at 12:25):

From: Manuel Eberl <eberlm@in.tum.de>
Have you done the usual "isabelle components -a"?

Manuel
smime.p7s

Email Gateway (Mar 12 2021 at 12:34):

From: Peter Lammich <lammich@in.tum.de>
On Fri, 2021-03-12 at 13:24 +0100, Manuel Eberl wrote:

Have you done the usual "isabelle components -a"?

I would like to, but it has no effect. Produces no output, and returns
with exit-code 0.

peter@peterXps:~/devel/Isabelle-devel$ ./bin/isabelle components -a
peter@peterXps:~/devel/Isabelle-devel$ echo $?
0

Manuel

On 12/03/2021 13:23, Peter Lammich wrote:

Hi,

I'm trying to start the Isabelle repo version, but only get as far
as

peter@peterXps:~/devel/Isabelle-devel$ ./bin/isabelle

Building Isabelle/Scala ...

Unknown JAVA_HOME -- Java unavailable
Failed to compile sources
peter@peterXps:~/devel/Isabelle-devel$ echo $JAVA_HOME
/usr/lib/jvm/java-14-openjdk-amd64

My machine is brand new, so I might be lacking some prerequisites?
Isabelle2021 runs without problems.

--
Peter

peter@peterXps:~/devel/Isabelle-devel$ hg tip
changeset: 73411:1f1366966296
tag: tip
user: haftmann
date: Thu Mar 11 07:05:38 2021 +0000
summary: avoid name clash

---

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

---

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Mar 12 2021 at 12:37):

From: Fabian Huch <huch@in.tum.de>
You probably need to initialize the user settings first with "isabelle
components -I" if it's a new machine.

Fabian

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Mar 12 2021 at 13:28):

From: Makarius <makarius@sketis.net>
What does "isabelle components -l" say?

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Mar 12 2021 at 13:58):

From: Peter Lammich <lammich@in.tum.de>
On Fri, 2021-03-12 at 14:28 +0100, Makarius wrote:

On 12/03/2021 13:34, Peter Lammich wrote:

On Fri, 2021-03-12 at 13:24 +0100, Manuel Eberl wrote:

Have you done the usual "isabelle components -a"?

I would like to, but it has no effect. Produces no output, and
returns
with exit-code 0.

peter@peterXps:~/devel/Isabelle-devel$ ./bin/isabelle components -a

What does "isabelle components -l" say?

It listed a few components as available, and none as missing. Java was
in neither list!

(As I have fixed the problem now, I cannot reproduce the exact output
any more)

Email Gateway (Mar 12 2021 at 15:11):

From: Makarius <makarius@sketis.net>
It listed the components that are "built-in" the repository clone, but not the
add-on components, which are "bundled" for a proper release.

I can think of ways to make this even simpler and more robust, but just a few
days ago I've found our "quick-start from 0 to 100" from the repository
exceedingly straight-forward compared to software distributions by our
colleagues with OCaml or Haskell background.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Mar 12 2021 at 15:57):

From: Peter Lammich <lammich@in.tum.de>

I can think of ways to make this even simpler and more robust, but
just a few
days ago I've found our "quick-start from 0 to 100" from the
repository
exceedingly straight-forward compared to software distributions by
our
colleagues with OCaml or Haskell background.

I agree, once you find the README_REPOSITORY, there are no open
questions any more, and at least on Linux it took me much less than the
advertised 30 minutes to be up and running :)

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Dec 21 2024 at 16:20 UTC