Re: [isabelle] Incompleteness and Nominal2



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.