On 08/05/18 13:49, Lawrence Paulson wrote: > I have two interns from École Polytechnique. They have been going over > HOL-Algebra and Group-Ring-Module, providing new proofs of the best results > in the latter and tidying up some messy proofs in the former, as well. They > are also systematising the chaotic naming conventions that they found there. > So there will be big changes to HOL-Algebra in the coming weeks. This is an > early warning in case anybody else wants to work on this directory.
Is the chaotic naming in Group-Ring-Module or HOL-Algebra? According to my information, Clemens Ballarin has taken great care about HOL-Algebra over many years (even with contributions by students). Beyond that, I am just hoping that we are not sliding into the "best practices" of the average Github project, with huge commits / merges coming out of the blue, which are hard to understand later. Both the sources and their history need to be readable, in order to sort out subtle problems. These days I read history even more often than the latest version of the sources. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev