[isabelle-dev] Status of afp-2015

Larry Paulson lp15 at cam.ac.uk
Tue Apr 28 15:30:37 CEST 2015


Maybe I don’t understand how this works. I was under the impression that both the main repository and the AFP had been forked in preparation for the release, allowing people to add new material to the repository (with appropriate corrections to the AFP) that would be independent of the current release and included only in the one after that.

Larry

> On 28 Apr 2015, at 14:25, Makarius <makarius at sketis.net> wrote:
> 
> I am confused about the status of afp-2015 wrt. current Isabelle2015 release candidates.
> 
> According to my own post on isabelle-users, Isabelle2015-RC1 and AFP/a44a0c9e17ef correspond to each other.  It was a stable point after days of chaos before entering the final release process.
> 
> That relative stability seems to have been lost again:
> 
>  isabelle-release/18267ceb10b5
>  afp-2015/d8cda568cd81
> 
> Unfinished session(s): Call_Arity, Circus, Depth-First-Search, FunWithFunctions, Girth_Chromatic, KBPs, Launchbury, Markov_Models, Random_Graph_Subgraph_Threshold, Separation_Logic_Imperative_HOL, UpDown_Scheme
> 
> That is without the "slow" sessions.
> 
> 
> Is afp-2015 actually tested anywhere?
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list