search

isabelle-prover / conventions

https://isabelle.systems/conventions/
MIT License
2 stars 4 forks source link

[Feedback] Style #8

Closed wimmers closed 4 years ago

wimmers commented 4 years ago

Files should not be longer than 1500 lines. While this not a hard limit, exceeding this size limit should be seen as an opportunity to evaluate whether it can be sensibly split up. Tobias disagrees and says "But maybe it is not so bad too have this reminder to avoid monster files."

Do not use indexed access to fact collections, e.g. algebra_simps(3) Tobias: S/h produces them and it is a paint to get rid of them.

The preferred method of stating assumptions is by using explicit assumes clauses. Tobias: I very much disagree. In inductive proofs it introduces a lot of textual noise. I explicitly never do it in such proofs.

The seperating | between several equations is put at the beginning of the line without indentation. Tobias: I disagree strongly. Those "|" are more syntactic noise coming from ML. Haskell does not have them. It is much more readable to put them at the end of the line. Indentation provides the needed visual clue.

Tobias: I find some of the rules in Proofs too detailed, it may hurt more than it helps.

kappelmann commented 4 years ago

I added a PR #9 for this feedback ticket. Here's a summary what I did so far:

Files should not be longer than 1500 lines. While this not a hard limit, exceeding this size limit should be seen as an opportunity to evaluate whether it can be sensibly split up. Tobias disagrees and says "But maybe it is not so bad too have this reminder to avoid monster files."

I think that's pretty much what we want to achieve, so let's keep it.

Do not use indexed access to fact collections, e.g. algebra_simps(3) Tobias: S/h produces them and it is a paint to get rid of them.

I need help here. Maybe @pruvisto can give more guidance? What's your take on this?

The preferred method of stating assumptions is by using explicit assumes clauses. Tobias: I very much disagree. In inductive proofs it introduces a lot of textual noise. I explicitly never do it in such proofs.

Fixed in #9

The seperating | between several equations is put at the beginning of the line without indentation. Tobias: I disagree strongly. Those "|" are more syntactic noise coming from ML. Haskell does not have them. It is much more readable to put them at the end of the line. Indentation provides the needed visual clue.

Fixed in #9

Tobias: I find some of the rules in Proofs too detailed, it may hurt more than it helps.

I'd say it's fine, but I am open to make it shorter if anyone has suggestions.

pruvisto commented 4 years ago

I need help here. Maybe @pruvisto can give more guidance? What's your take on this?

I don't think sledgehammer does this for dynamic fact collections like algebra_simps, derivative_intros, field_simps, divide_simps. At least grepping did not reveal a single one of them in the entire distribution or AFP. (There are two for tendsto_intros, but one of them was clearly not written by sledgehammer; for the other one it's not clear)

What sledgehammer does often do is something like semiring_normalization_rules(10), but that is just a bunch of lemmas, not a dynamic collection. Those are not as fragile; they can only break if somebody actually touches the lemmas themselves. The dynamic ones can break even if there is a change in the order of imports.

kappelmann commented 4 years ago

I need help here. Maybe @pruvisto can give more guidance? What's your take on this?

I don't think sledgehammer does this for dynamic fact collections like algebra_simps, derivative_intros, field_simps, divide_simps. At least grepping did not reveal a single one of them in the entire distribution or AFP. (There are two for tendsto_intros, but one of them was clearly not written by sledgehammer; for the other one it's not clear)

What sledgehammer does often do is something like semiring_normalization_rules(10), but that is just a bunch of lemmas, not a dynamic collection. Those are not as fragile; they can only break if somebody actually touches the lemmas themselves. The dynamic ones can break even if there is a change in the order of imports.

Cool, thank you. Would you say Do not use indexed access to dynamic fact collections (e.g. algebra_simps, derivative_intros) instead of Do not use indexed access to fact collections is a good formulation then? If so, I'd update the PR with this change.

pruvisto commented 4 years ago

All right.

lukasstevens commented 4 years ago

I disagree at least on the pipes. It does not hurt do go with one of the both styles and the style with the pipes in front gives you the correct indentation for free.

lukasstevens commented 4 years ago

Additionally, I am not sure about the comment about the induction proofs. If I understand correctly the only difference is the using assms? But sometimes you don't want to have all assumptions as premises of the induction which is easier if you use the assumes style since you can name the assumptions.

wimmers commented 4 years ago

I disagree at least on the pipes. It does not hurt do go with one of the both styles and the style with the pipes in front gives you the correct indentation for free.

I agree with Lukas here. For me the pipes are "more invisible" if they are consistently placed at the beginning of the line rather than the end.

wimmers commented 4 years ago

If we cannot find an agreement on these points, maybe we should just deregulate them? (or mention that consistency is most important?)

kappelmann commented 4 years ago

I'm for deregulation as I do not want to start a war about things I do not care so much about (like pipes at the beginning vs end or stating assumptions with meta level implication in case of simple induction proofs to avoid textual noise). My proposal regarding the former can be seen here and about the latter here.

I'll post two polls on Zulip regarding these 2 questions.

kappelmann commented 4 years ago

Last chance to intervene; otherwise, #9 will be merged on Sunday evening.