Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Scala error

view this post on Zulip Email Gateway (Nov 12 2021 at 06:48):

From: Tobias Nipkow <nipkow@in.tum.de>
I am on 6cb700c77786

$ ### Building Isabelle/Scala (/Users/nipkow/isabelle/lib/classes/isabelle.jar) ...
/Users/nipkow/isabelle/src/Pure/Admin/build_history.scala:143: error: object
getenv is not a member of package System
System.getenv("ISABELLE_SETTINGS_PRESENT") match {

and so on. I tried "isabelle components -a" but nothing happens.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Nov 12 2021 at 08:42):

From: Tobias Nipkow <nipkow@in.tum.de>
I also emptied .isabelle/contrib and reran components -a, but the error persists.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Nov 13 2021 at 11:56):

From: Makarius <makarius@sketis.net>
persists.

Odd. From a distance, I would say there is something wrong with the classpath,
e.g. old versions of Scala or something else.

It could help to purge lib/classes/ within the Isabelle repository clone.

Moreover, you can check "isabelle components -l" and "isabelle getenv
ISABELLE_CLASSPATH CLASSPATH" to see if some old garbage left over.

Makarius

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

view this post on Zulip Email Gateway (Nov 13 2021 at 11:56):

From: Tobias Nipkow <nipkow@in.tum.de>
On 12/11/2021 10:47, Makarius wrote:

It could help to purge lib/classes/ within the Isabelle repository clone.

I should have said that I tried that as well (suggested by Fabian Huch). I
emptied lib/classes/ and it is still empty.

Moreover, you can check "isabelle components -l" and "isabelle getenv
ISABELLE_CLASSPATH CLASSPATH" to see if some old garbage left over.

$ isabelle getenv ISABELLE_CLASSPATH CLASSPATH
ISABELLE_CLASSPATH=/Users/nipkow/.isabelle/contrib/flatlaf-1.6/lib/flatlaf-1.6.jar:/Users/nipkow/.isabelle/contrib/isabelle_setup-20211109/lib/isabelle_setup.jar:/Users/nipkow/.isabelle/contrib/jedit-20211103/jedit5.6.0-patched/jedit.jar:/Users/nipkow/.isabelle/contrib/jfreechart-1.5.3/lib/iText-2.1.5.jar:/Users/nipkow/.isabelle/contrib/jfreechart-1.5.3/lib/jfreechart-1.5.3.jar:/Users/nipkow/.isabelle/contrib/jortho-1.0-2/jortho.jar:/Users/nipkow/.isabelle/contrib/kodkodi-1.5.7/jar/antlr-runtime-3.1.1.jar:/Users/nipkow/.isabelle/contrib/kodkodi-1.5.7/jar/kodkod-1.5.jar:/Users/nipkow/.isabelle/contrib/kodkodi-1.5.7/jar/kodkodi-1.5.7.jar:/Users/nipkow/.isabelle/contrib/kodkodi-1.5.7/jar/sat4j-2.3.jar:/Users/nipkow/.isabelle/contrib/postgresql-42.2.24/postgresql-42.2.24.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/jline-3.19.0.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/jna-5.3.1.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scala-compiler.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scala-library.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scalap-2.13.5.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scala-parallel-collections_2.13-1.0.0.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scala-parser-combinators_2.13-1.1.2.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scala-reflect.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scala-swing_2.13-3.0.0.jar:/Users/nipkow/.isabelle/contrib/scala-2.13.5/lib/scala-xml_2.13-1.3.0.jar:/Users/nipkow/.isabelle/contrib/sqlite-jdbc-3.36.0.3/sqlite-jdbc-3.36.0.3.jar:/Users/nipkow/.isabelle/contrib/ssh-java-20190323/lib/jsch-0.1.55.jar:/Users/nipkow/.isabelle/contrib/ssh-java-20190323/lib/jzlib-1.1.3.jar:/Users/nipkow/.isabelle/contrib/ssh-java-20190323/lib/jce.jar:/Users/nipkow/.isabelle/contrib/xz-java-1.9/lib/xz-1.9.jar
CLASSPATH=

$ isabelle components -l

Available components:
/Users/nipkow/isabelle
/Users/nipkow/isabelle/src/Tools/jEdit
/Users/nipkow/isabelle/src/Tools/GraphBrowser
/Users/nipkow/isabelle/src/Tools/Graphview
/Users/nipkow/isabelle/src/Tools/Setup
/Users/nipkow/isabelle/src/Tools/VSCode
/Users/nipkow/isabelle/src/HOL/Mutabelle
/Users/nipkow/isabelle/src/HOL/Library/Sum_of_Squares
/Users/nipkow/isabelle/src/HOL/SPARK
/Users/nipkow/isabelle/src/HOL/Tools
/Users/nipkow/isabelle/src/HOL/TPTP
/Users/nipkow/isabelle/Admin
/Users/nipkow/.isabelle
/Users/nipkow/.isabelle/contrib/gnu-utils-20211030
/Users/nipkow/.isabelle/contrib/bash_process-1.2.4-2
/Users/nipkow/.isabelle/contrib/bib2xhtml-20190409
/Users/nipkow/.isabelle/contrib/csdp-6.1.1
/Users/nipkow/.isabelle/contrib/cvc4-1.8
/Users/nipkow/.isabelle/contrib/e-2.6-1
/Users/nipkow/.isabelle/contrib/flatlaf-1.6
/Users/nipkow/.isabelle/contrib/idea-icons-20210508
/Users/nipkow/.isabelle/contrib/isabelle_fonts-20211004
/Users/nipkow/.isabelle/contrib/isabelle_setup-20211109
/Users/nipkow/.isabelle/contrib/jdk-17.0.1+12
/Users/nipkow/.isabelle/contrib/jedit-20211103
/Users/nipkow/.isabelle/contrib/jfreechart-1.5.3
/Users/nipkow/.isabelle/contrib/jortho-1.0-2
/Users/nipkow/.isabelle/contrib/kodkodi-1.5.7
/Users/nipkow/.isabelle/contrib/minisat-2.2.1-1
/Users/nipkow/.isabelle/contrib/nunchaku-0.5
/Users/nipkow/.isabelle/contrib/opam-2.0.7
/Users/nipkow/.isabelle/contrib/polyml-5.9-5d4caa8f7148
/Users/nipkow/.isabelle/contrib/postgresql-42.2.24
/Users/nipkow/.isabelle/contrib/scala-2.13.5
/Users/nipkow/.isabelle/contrib/smbc-0.4.1
/Users/nipkow/.isabelle/contrib/spass-3.8ds-2
/Users/nipkow/.isabelle/contrib/sqlite-jdbc-3.36.0.3
/Users/nipkow/.isabelle/contrib/ssh-java-20190323
/Users/nipkow/.isabelle/contrib/stack-2.7.3
/Users/nipkow/.isabelle/contrib/vampire-4.6
/Users/nipkow/.isabelle/contrib/verit-2021.06.1-rmx
/Users/nipkow/.isabelle/contrib/xz-java-1.9
/Users/nipkow/.isabelle/contrib/z3-4.4.0pre-3
/Users/nipkow/.isabelle/contrib/zipperposition-2.1-1
/Users/nipkow/AFP/devel
/Users/nipkow/Sem

Missing components:
smime.p7s

view this post on Zulip Email Gateway (Nov 13 2021 at 12:13):

From: Makarius <makarius@sketis.net>
On 12/11/2021 10:51, Tobias Nipkow wrote:

Moreover, you can check "isabelle components -l" and "isabelle getenv
ISABELLE_CLASSPATH CLASSPATH" to see if some old garbage left over.

$ isabelle getenv ISABELLE_CLASSPATH CLASSPATH

This looks fine.

$ isabelle components -l

Available components:
...
  /Users/nipkow/AFP/devel
  /Users/nipkow/Sem

What happens without these two additional components?

Moreover, you can check your $ISABELLE_HOME_USER/etc/settings to make sure
that there are no special tricks concerning Java or Scala.

I am implicitly assuming that a clean clone with separate installation name
works, e.g.

hg clone -r 4f1c1c7eb95f https://isabelle.in.tum.de/repos/isabelle isabelle-test

isabelle-test/Admin/init -I test

Makarius

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

Last updated: Jul 15 2022 at 23:21 UTC