Hanno Becker (May 30 2024 at 14:09): Hanno Becker (May 30 2024 at 14:09):Hi. Are there instructions anywhere for how to build Isabelle from source?
Mathias Fleury (May 30 2024 at 19:37):like the ones from the README_REPOSITORY or what are looking for?
Mathias Fleury (May 30 2024 at 19:39):or the Admin/Release/CHECKLIST to produce a report?
Fabian Huch (May 31 2024 at 08:22):Actually, Isabelle is 'built from source' every time you execute it with changed sources.
Fabian Huch (May 31 2024 at 08:25):What is not re-built are the supplied components. Those are external dependencies as well as a pre-built bootstrapping module.
Fabian Huch (May 31 2024 at 08:26):You can build those with the appropriate isabelle component_<name> tool, provided you use the repository version.
Hanno Becker (May 31 2024 at 15:41):Thank you @Mathias Fleury @Fabian Huch, that's helpful :pray:
Mario Carneiro (Jul 26 2024 at 12:51):I'm also trying to figure out how to build isabelle directly from the sketis repository. I am on Ubuntu Linux. I installed the latest versions of java, scala, polyml, but Admin/init returned Unknown JAVA_HOME -- Java unavailable. I then used whereis to find my JDK and set ISABELLE_JDK_HOME=/usr/lib/jvm/java-11-openjdk-amd64, then Admin/init returns
Error: Could not find or load main class isabelle.setup.Setup
Caused by: java.lang.ClassNotFoundException: isabelle.setup.Setup
What should I try at this point? None of the bin/isabelle * commands work.
Mario Carneiro (Jul 26 2024 at 12:55):ISABELLE_CLASSPATH appears to be unset
Fabian Huch (Jul 26 2024 at 13:40):Which Ubuntu are you on? You do not need to install any of java/scala/polyml, all you need for the repository version is Mercurial to clone it.
Fabian Huch (Jul 26 2024 at 13:41):What is the output of bin/isabelle components -I? It looks like it could not create the user home.
Fabian Huch (Jul 26 2024 at 13:43):(The components tool works without working Isabelle)
Mathias Fleury (Jul 26 2024 at 14:59):(and do not forget `bin/isabelle components -a if the -I did not produce any error!)
Mario Carneiro (Jul 26 2024 at 21:14):I sat down with Makarius to troubleshoot this and it turns out the issue was that lib/Tools/components was not executable, caused by a bad backup some years ago. Apparently hg update doesn't fix permissions issues. Deleting and recreating the repo from scratch fixed the issue.
Last updated: Dec 21 2024 at 12:33 UTC