147 is to get your code into the Isabelle distribution. For this you have |
147 is to get your code into the Isabelle distribution. For this you have |
148 to convince other developers that your code or project is of general interest. |
148 to convince other developers that your code or project is of general interest. |
149 If you managed to do this, then the problem of the moving target goes |
149 If you managed to do this, then the problem of the moving target goes |
150 away, because when checking in code, developers are strongly urged to |
150 away, because when checking in code, developers are strongly urged to |
151 test against Isabelle's code base. If your project is part of that code base, |
151 test against Isabelle's code base. If your project is part of that code base, |
152 then code maintenance is done by others. Unfortunately, this might not |
152 then maintenance is done by others. Unfortunately, this might not |
153 be a helpful advice for all types of projects. A lower threshold for inclusion has the |
153 be a helpful advice for all types of projects. A lower threshold for inclusion has the |
154 Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} |
154 Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} |
155 This archive has been created mainly for formalisations that are |
155 This archive has been created mainly for formalisations that are |
156 interesting but not necessarily of general interest. If you have ML-code as |
156 interesting but not necessarily of general interest. If you have ML-code as |
157 part of a formalisation, then this might be the right place for you. There |
157 part of a formalisation, then this might be the right place for you. There |