[isabelle] Incompleteness and Nominal2

[Manuel Eberl]

Hallo,

Dana Scott just asked me why he could not get the AFP entry
Incompleteness to work. I tried it myself and found that the entry makes
use of Nominal2, but Nominal2 is not an AFP entry itself, nor is it
available anywhere else. All I found is an old version that works with
Isabelle 2014.

Strangely, when clicking ‘Browse theories’ in the Incompleteness AFP
entry, some Nominal2 theories show up, but when downloading the .tar.gz
(‘Download this entry’), they are not in the archive.

What is the current status of Nominal2, especially in combination with
Incompleteness? Having an AFP entry online that does not work when you
download it and load it into Isabelle seems highly undesirable to me.


Cheers,

Manuel

[Larry Paulson]

This is weird. It is definitely in the mercurial repository, but it doesn’t appear as an individual entry. This means that you have to download the entire AFP, all 144 MB, if you want to get it. I think that this has been the situation for a considerable time.

It’s worth mentioning that Incompleteness takes several minutes to run, even on a fast machine.

Larry Paulson

[Buday Gergely]

How about downloading it from the official Nominal Isabelle site:

http://www.inf.kcl.ac.uk/staff/urbanc/Publications/Nominal2-2014.tgz

I don't know though if the incompleteness proof works with this version.

- Gergely
________________________________________
From: cl-isabelle-...@lists.cam.ac.uk [cl-isabelle-...@lists.cam.ac.uk] On Behalf Of Larry Paulson [lp...@cam.ac.uk]
Sent: Tuesday, July 07, 2015 5:51 PM
To: Manuel Eberl
Cc: isabelle-users
Subject: Re: [isabelle] Incompleteness and Nominal2

[Manuel Eberl]

That's Isabelle 2014. It doesn't work with the current version of
Isabelle. Since Incompleteness depends on Nominal2, is in the AFP, and
works in the automatic tests (I think), there must be an up-to-date
version of Nominal2. The question is just: Where is it?

Manuel

[Makarius]

On Tue, 7 Jul 2015, Larry Paulson wrote:

> This is weird. It is definitely in the mercurial repository, but it
> doesn’t appear as an individual entry. This means that you have to
> download the entire AFP, all 144 MB, if you want to get it. I think that
> this has been the situation for a considerable time.

I've always found the official AFP website a bit inconvenient wrt. entries
that depend on other entries; in practice I am always using a repository
clone (official or devel).

For Nominal2, the situation seems to be worse, since it is not even an
official entry -- which I did not know before, but I am not an AFP editor,
just a maintainer.


Here is the relevant changeset history with the typical dry humor
of changelog entries:


changeset: 3379:2c497230e04c
user: kleing
date: Thu Feb 21 10:39:00 2013 +1100
description:
added Nominal2 session temporarily; expected to be merged into Isabelle


changeset: 4008:c228a6bd7a2b
user: wenzelm
date: Tue Dec 31 13:36:44 2013 +0100
description:
tuned comment;

--- a/thys/Nominal2/ROOT Mon Dec 30 15:23:40 2013 +0000
+++ b/thys/Nominal2/ROOT Tue Dec 31 13:36:44 2013 +0100
@@ -1,7 +1,5 @@
-chapter AFP
-
-(* This session is expect to be merged into the Isabelle distribution
- before the next release *)
+(* This session is expected to be merged into the Isabelle distribution
+ before the next release *) (* FIXME since 21-Feb-2013 *)


changeset: 5342:641cc20ec48e
user: wenzelm
date: Wed Apr 01 18:19:17 2015 +0200
description:
proper chapter;
removed outdated comment;

diff -r 52a8a76eddaf -r 641cc20ec48e thys/Nominal2/ROOT
--- a/thys/Nominal2/ROOT Wed Apr 01 17:17:09 2015 +0200
+++ b/thys/Nominal2/ROOT Wed Apr 01 18:19:17 2015 +0200
@@ -1,5 +1,4 @@
-(* This session is expected to be merged into the Isabelle distribution
- before the next release *) (* FIXME since 21-Feb-2013 *)
+chapter AFP

session "Nominal2" (AFP) = HOL +
options [document = false]


The last change merely formalizes the de-facto situation that Nominal2 is
a permanent part of AFP. IIRC, it was also based on some private
discussions with Christian Urban and/or Gerwin Klein.


Makarius

[Gerwin Klein]

What’s going on is that Nominal2 is not an official entry, so has no website entry and no separate tar file to download.

Nominal2 was supposed to go into the Isabelle distribution and replace Nominal. This has not happened in over a year, and I’m not happy with this situation. It should either become a real entry or be removed.

Currently, the best way to get it is to download the whole AFP release (from the download link in the navigation panel on the left).

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

[Ken Kubota]

Hello,

With the following download links I was successful (14.06.2015):

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015.dmg
http://sourceforge.net/projects/afp/files/afp-Isabelle2015/afp-2015-05-28.tar.gz/download

Kind regards,

Ken Kubota

[Christian Urban]

Just to add that I updated my nominal web-page with a
current version of Nominal2 for Isabelle 2015. Sorry, I
was still running Isabelle 2014 and somehow forgot to
do this.

Please let me know if there is anything not working
or not available.

Best wishes,
Christian