docs: update arch-split #771

Xaphiosis · 2024-07-04T05:31:55Z

Some things were confusing, some changed over time. Hopefully this is an improvement.

Particular notes:

extend_locale was unused and removed, replaced by the _AI_2 multiple-locale strategy
the explicit global requalify_facts strategy was used but not documented

Reviewers:

probably easier to read https://github.com/Xaphiosis/l4v/blob/arch_split/docs/arch-split.md than only the diff
note the two FIXMEs, I could use some help there.
the _AI_asms vs _AI_assms is wonderfully inconsistent (1597 instances of the former, 506 of the latter): I'd like to pick one and then standardise

docs/arch-split.md

lsf37

Cool, thanks for updating the docs.

docs/arch-split.md

lsf37 · 2024-07-04T07:25:26Z

docs/arch-split.md

+FIXME: strictly speaking, there is no requirement that `Foo_AI_2` includes
+`Foo_AI_1`, but in practice we always do so (I guess because we want everything
+that got proved to be instantly available in case we need it in the proof
+chain). This would mean that the same fact gets exported multiple times?


I'm not entirely sure, but I think Isabelle is actually smart about that. We could double check, but the number of lemmas that would be instantiated twice is fairly small, so I would probably stick with a chain like this even if there was duplication.

Yeah, I guess I should check.

investigate how many lemmas of same name but different prefix this chain generates

Investigation results: at most one duplicate is generated, so can confirm that Isabelle is smart about it as you said. My initial thought that maybe we can make all the locales export with the same prefix has been demonstrated to be impossible as well, so we can leave the status quo as is, and I should remove this FIXME. Maybe I should resolve it into a note in the doc? Would that be of use to anyone?

If it can be expressed easily, it would be of use in avoiding us having the same thought and doing the same investigation some time in the future.

Agreed, adding a note would be nice, I'm sure we'll have the same question again in a few years otherwise.

corlewis

Looks good to me, this reads nicer now and should avoid some confusion. I don't have any specific comments that haven't already been mentioned.

Some things were confusing, some changed over time. Hopefully this is an improvement. Particular notes: * extend_locale was unused and removed, replaced by the `_AI_2` multiple-locale strategy * the explicit global requalify_facts strategy was used but not documented Signed-off-by: Rafal Kolanski <[email protected]>

Xaphiosis added the docs Documentation, READMEs, etc label Jul 4, 2024

Xaphiosis requested review from lsf37 and corlewis July 4, 2024 05:31