Re: [isabelle] Incompleteness and Nominal2



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


> On 7 Jul 2015, at 16:43, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> 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





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