[isabelle-dev] Duplications in AFP

Clemens Ballarin ballarin at in.tum.de
Thu Oct 16 14:04:14 CEST 2008


[This message is mainly directed to the AFP programme committee.]

The AFP contains clones and duplications of theory files and even  
entire directories between the entries.  For example, I recently  
discovered that JinjaThreads/DFA is an identical copy of Jinja/DFA  
(see the diff below).

While cloning cannot always be avoided, duplicates are a nuisance.   
They put additional burden on maintainers.  I suggest to change the  
AFP review policy so that clones will only be accepted in justified  
cases and duplicates (as the one above) will not be admitted altogether.

Clemens

----
lapbroy72:~/isabelle/afp-devel/thys/Jinja/DFA ballarin$ for n in  
*.thy; do diff $n ../../JinjaThreads/DFA/$n; done
2c2
<     ID:         $Id: Abstract_BV.thy,v 1.4 2008/07/25 15:07:14  
fhaftmann Exp $
---
 >     ID:         $Id: Abstract_BV.thy,v 1.4 2008/07/25 08:22:52  
fhaftmann Exp $
2c2
<     ID:         $Id: Err.thy,v 1.12 2008/10/16 07:59:45 ballarin Exp $
---
 >     ID:         $Id: Err.thy,v 1.7 2008/10/16 07:59:46 ballarin Exp $
2c2
<     ID:         $Id: Kildall.thy,v 1.12 2008/10/16 07:59:46  
ballarin Exp $
---
 >     ID:         $Id: Kildall.thy,v 1.6 2008/10/16 07:59:46  
ballarin Exp $
2c2
<     ID:         $Id: LBVComplete.thy,v 1.9 2008/07/25 15:07:15  
fhaftmann Exp $
---
 >     ID:         $Id: LBVComplete.thy,v 1.4 2008/07/25 08:22:53  
fhaftmann Exp $
2c2
<     ID:         $Id: LBVCorrect.thy,v 1.7 2008/07/25 15:07:15  
fhaftmann Exp $
---
 >     ID:         $Id: LBVCorrect.thy,v 1.4 2008/07/25 08:22:54  
fhaftmann Exp $
2c2
<     ID:         $Id: LBVSpec.thy,v 1.7 2008/07/25 15:07:16  
fhaftmann Exp $
---
 >     ID:         $Id: LBVSpec.thy,v 1.4 2008/07/25 08:22:54  
fhaftmann Exp $
2c2
<     ID:         $Id: Listn.thy,v 1.9 2008/10/16 07:59:46 ballarin  
Exp $
---
 >     ID:         $Id: Listn.thy,v 1.6 2008/10/16 07:59:46 ballarin  
Exp $
2c2
<     ID:         $Id: Opt.thy,v 1.6 2008/07/25 15:07:16 fhaftmann Exp $
---
 >     ID:         $Id: Opt.thy,v 1.3 2008/06/12 06:57:21 lsf37 Exp $
2c2
<     ID:         $Id: Product.thy,v 1.10 2008/07/25 15:07:16  
fhaftmann Exp $
---
 >     ID:         $Id: Product.thy,v 1.6 2008/07/25 08:22:54  
fhaftmann Exp $
2c2
<     ID:         $Id: Semilat.thy,v 1.10 2008/07/25 15:07:17  
fhaftmann Exp $
---
 >     ID:         $Id: Semilat.thy,v 1.6 2008/07/25 08:22:55  
fhaftmann Exp $
2c2
<     ID:         $Id: SemilatAlg.thy,v 1.7 2008/10/16 07:59:46  
ballarin Exp $
---
 >     ID:         $Id: SemilatAlg.thy,v 1.5 2008/10/16 07:59:46  
ballarin Exp $
2c2
<     ID:         $Id: Semilattices.thy,v 1.4 2008/07/25 15:07:17  
fhaftmann Exp $
---
 >     ID:         $Id: Semilattices.thy,v 1.4 2008/07/25 07:12:11  
fhaftmann Exp $
2c2
<     ID:         $Id: Typing_Framework.thy,v 1.4 2008/07/25 15:07:17  
fhaftmann Exp $
---
 >     ID:         $Id: Typing_Framework.thy,v 1.3 2008/06/12  
06:57:22 lsf37 Exp $
2c2
<     ID:         $Id: Typing_Framework_err.thy,v 1.4 2008/07/25  
15:07:17 fhaftmann Exp $
---
 >     ID:         $Id: Typing_Framework_err.thy,v 1.3 2008/06/12  
06:57:22 lsf37 Exp $





More information about the isabelle-dev mailing list