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