Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help to Build Latest Isabelle Release?


view this post on Zulip Email Gateway (Aug 18 2022 at 15:13):

From: "M. Wu" <mw494@cam.ac.uk>
Hi,

Does anyone know how to build the Latest Release of Isabelle?

My Isabelle (version Isabelle2009-1) runs correctly, after building the new
release successfully. tar -C /usr/local -xzf Isabelle_03-May-2010.tar.gz
/usr/local/Isabelle/build

An error occurred when running Isabelle: Missing Proof General installation
(PROOFGENERAL_HOME) I am pretty sure that the proof general is installed, I
am not familiar with Isabelle installation. I wonder if someone know what
is the problem.

Best regards,

Minghao

view this post on Zulip Email Gateway (Aug 18 2022 at 15:13):

From: Makarius <makarius@sketis.net>
On Tue, 4 May 2010, M. Wu wrote:

Does anyone know how to build the Latest Release of Isabelle?

My Isabelle (version Isabelle2009-1) runs correctly, after building the new
release successfully. tar -C /usr/local -xzf Isabelle_03-May-2010.tar.gz
/usr/local/Isabelle/build

Isabelle2009-1 is the latest release.

Building (or even using) an arbitrary development snapshot is quite
adventurous, i.e. you make yourself an alpha tester of an arbitrary point
in the history. Incoming changes can be browsed via
http://isabelle.in.tum.de/repos/isabelle and make sure to check that the
performance charts on http://isabelle.in.tum.de/devel do not indicate
serious problems.

The right place to discuss arbitrary Isabelle snapshots is the
isabelle-dev mailing list.

An error occurred when running Isabelle: Missing Proof General
installation (PROOFGENERAL_HOME) I am pretty sure that the proof general
is installed, I am not familiar with Isabelle installation. I wonder if
someone know what is the problem.

See the Isabelle system manual how settings work. You somehow need to
point to an existing Proof General version, or symlink from
Isabelle/contrib/ProofGeneral etc. Check with the official Isabelle
bundle of Isabelle2009-1 how it can be done. There will be more handiwork
than just adjusting Proof General.

Makarius


Last updated: Mar 28 2024 at 08:18 UTC