Some more rules for Lib

[michaelmcinerney]

Currently separated into many smaller commits, but I could consolidated them into just a few commits if that's preferred: one commit for reader monad lemmas, one for lists, then one for CLib, Heap_List.thy, Corres_UL.thy, and MonadicRewrite.thy

[Xaphiosis]

Nice. I'm really behind the times with all the reader and option monad stuff, so can't really comment on those.
Something worth deciding on now: I don't know if one commit per lemma added is the right way to go. It might be more useful to group them, have one commit per group and list the lemmas in there (so they still show up in git log)? The commits don't really say where something was added either, so the knowledge they provide is kinda limited anyway. @lsf37 ?

[lsf37]

Looking good! I would indeed squash the commits as proposed.

[Xaphiosis]

Looking good! I would indeed squash the commits as proposed.

What do you think of the current result? I don't think the "many" is useful, and I was hoping that the lemma names would instead make it into the longer commit message... but if they're gone at this point, putting them back requires effort.

[lsf37]

I would still tweak the commit messages a bit. I.e. I'd drop the many from the lib: commits and indicate where the lemmas are added -- first one says "reader monad", which is fine, but in the other commits I can't tell from looking at the commit message what it is that is changing. Mentioning the theory name would work, or the corresponding concept when the theory name is too long.

[michaelmcinerney]

I would still tweak the commit messages a bit. I.e. I'd drop the many from the lib: commits and indicate where the lemmas are added -- first one says "reader monad", which is fine, but in the other commits I can't tell from looking at the commit message what it is that is changing. Mentioning the theory name would work, or the corresponding concept when the theory name is too long.

So would lib: add lemmas about lists to Lib.thy and ListLibLemmas.thy be ok? The other commits seems specific enough to me. But could we not also just use git log —name-only to see the files which are modified, if we wanted to?

[lsf37]

So would lib: add lemmas about lists to Lib.thy and ListLibLemmas.thy be ok?

The .thy doesn't carry information, so I'd go for lib: add list lemmas to Lib and ListLibLemmas

The other commits seems specific enough to me.

They mention the lemma name, but they don't say where something changes apart from lib which is very large. In this case the lemma names do kinda give you enough information (corres_stateAssert would correctly assumed to be in Corres_UL etc), so yes, you are right. We can leave those as is.

But could we not also just use git log —name-only to see the files which are modified, if we wanted to?

Yes, one could -- it's not about enumerating all changed files, but to make it possible to quickly see what areas changed when you just scan the commit headers.

[michaelmcinerney]

The .thy doesn't carry information, so I'd go for lib: add list lemmas to Lib and ListLibLemmas

Lib is the name of the session as well as the name of the file to which I'm adding lemmas, but I will go with your suggestion.

Yes, one could -- it's not about enumerating all changed files, but to make it possible to quickly see what areas changed when you just scan the commit headers.

I personally can't see the benefit of that, but if that's the case, then could the commit messages guide be updated for the case where we're adding to lib but not to a subdirectory like monads?

[lsf37]

The .thy doesn't carry information, so I'd go for lib: add list lemmas to Lib and ListLibLemmas

Lib is the name of the session as well as the name of the file to which I'm adding lemmas, but I will go with your suggestion.

It is the name of the session, but the tag already indicates that, so I don't think it would be confused.

Yes, one could -- it's not about enumerating all changed files, but to make it possible to quickly see what areas changed when you just scan the commit headers.

I personally can't see the benefit of that, but if that's the case, then could the commit messages guide be updated for the case where we're adding to lib but not to a subdirectory like monads?

The example section is trying to express that, but we can make it more explicit for lib specifically, yes.