Re: [isabelle] Isabelle Foundation & Certification



On Mi, 2015-09-16 at 16:10 +0100, Larry Paulson wrote:
> I was under the impression that this patch had been adopted. I donât believe that I saw any arguments against it.
> Larry

If this should be true, we should make it as public as possible, to stop
any rumours about Isabelle unsoundness. The best way would be to release
Isabelle2015-1 immediately, even if it would only be (Isabelle2015 +
patch), and not based on the current state of the repository.

--
  Peter


> 
> > On 16 Sep 2015, at 15:38, Peter Lammich <lammich at in.tum.de> wrote:
> > 
> > In the replied-to mail, I see more arguments that we should add proper
> > dependency checking to Isabelle/HOL as soon as possible.
> > 
> > As far as I know, there is a patch of KunÄar, which exists for more than
> > half a year now, which
> >  * ensures that consts/defs only produce conservative extensions
> >  * Does not slow down Isabelle significantly
> >  * Works with whole AFP and Isabelle-Library, i.e., is does not break
> > existing formalizations by being too restrictive.
> > 
> > However, it seems to be rejected or not given high priority by some main
> > Isabelle developers. 
> 
> 






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