Assistance with nightly-testing

Stream: CSLib

[Kim Morrison]

Dear CSLib contributors!

Unfortunately the infrastructure for continuously testing CSLib against nightly releases of Lean got out of sync, and we have a bit of catching up to do now!

I've fixed a number of problems on the nightly-testing branch, but some remain that I'm still having trouble with --- all, unfortunately, related to grind! It's exciting that CSLib is making good use of grind, but well, it's early days, and the implementation is changing underneath you and some breakages are to be expected. :-)

Could I ask the authors of these files for some help trying to work out what is still going wrong?

@Tanner Duve and @Bhavik Mehta:

• Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic

@Chris Henson:

• Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
• Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence

If you have ideas/solutions, please either push directly to the nightly-testing branch if you have appropriate permissions, create a PR against the nightly-testing branch, or just post here.

[Chris Henson]

I can't say I understand the why in all cases, but I was able to intuit what needed to be fixed and pushed to nightly-testing (including the linear logic file, because I think I suggested those while reviewing).

[Chris Henson]

There are lots of messages now from grind annotations without a specified pattern. We had already discouraged them, I am thinking they should be disallowed outright now? I can make a pass to fix these.

[Kim Morrison]

Yes, that's right. A plain @[grind] now makes suggestions about more specific grind annotations (e.g. @[grind =], @[grind .], @[grind ←]) that would be valid here, and we need to go through and select one.

[Kim Morrison]

Thank you, @Chris Henson, for the help fixing these problems! I will have a look at your diff later, but higher priority is now to get v4.25.0-rc1 out: this was the last concern holding it up.

[Kim Morrison]

I'll make sure not to move Cslib to v4.25.0-rc1 until we've fixed up these grind annotation messages. If you could make a first pass that would be very much appreciated; I can look too if you're busy.

[Chris Henson]

I have pushed a commit fixing all the annotation messages. How should I be thinking about grind .? Is this solely for backwards comparability, or a new general pattern?

[Bhavik Mehta]

I think grind . does what grind used to do, and now grind lists what the options are. And I think that in cases where grind = and grind give the same thing, grind = is preferred, but otherwise changing grind to grind . should be fine

[Chris Henson]

@Kim Morrison This nightly failure is caused by it incorrectly merging in the changes I made in cslib#113. Is the right thing to do here to go ahead and open a PR to main with our recent nightly changes?

[Chris Henson]

(I went ahead and fixed nightly-testing, so hopefully future merges are fine in the meantime)

[Kim Morrison]

Yes, feel free to simply push to nightly-testing, and if changes should be "backported" to main then do so via PR.