Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOL-Nominal to Isabelle2008


view this post on Zulip Email Gateway (Aug 18 2022 at 14:21):

From: Christian Urban <urbanc@in.tum.de>
Hi David,

David Streader writes:

Hi
I am just rebuilding Isabelle2009.
Unpacking HOL-Nominal_x86-linux.tar.gz it built directory Isabelle2008
and puts the heaps in there!
Is is safe to move the heaps to Isabelle2009 or is this an old set of heaps?

I am a bit confused what you want to do, or where
the problem is. HOL-Nominal should be fully integrated
with Isabelle 2009 and should always be up-to-date
with every release since 2009. Indeed, the tar-file
HOL-Nominal_x86-linux.tar.gz from

http://isabelle.in.tum.de/download_x86-linux.html

puts its content to

Isabelle2009/heaps/polyml-5.2.1_x86-linux/HOL-Nominal
Isabelle2009/heaps/polyml-5.2.1_x86-linux/log/HOL-Nominal.gz

Having downloaded the sources for Isabelle 2009, you
should also be able to rebuild the HOL-Nominal package
manually by typing

./build -m HOL-Nominal HOL

inside the directory where the Isabelle sources are
located.

Moving heaps between Isabelle releases, I am sure is
asking for trouble.

Hope this helps,
Christian


Last updated: Apr 26 2024 at 01:06 UTC