Re: [isabelle] Incompleteness and Nominal2
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?
On 07/07/15 19:39, Buday Gergely wrote:
> How about downloading it from the official Nominal Isabelle site:
> I don't know though if the incompleteness proof works with this version.
> - Gergely
> From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Larry Paulson [lp15 at cam.ac.uk]
> Sent: Tuesday, July 07, 2015 5:51 PM
> To: Manuel Eberl
> Cc: isabelle-users
> Subject: 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:
>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and