Planning for Copilot 4.7

[ivanperez-keera]

The following is a tentative plan for Copilot 4.7:

• Focus:

  • copilot-language - Unable to drop as many elements from Stream as prepended #607; @RyanGlScott to review, me and Ryan to coordinate with author to include changes.
  • Special Float values are translated incorrectly #697; potentially for @tkann-galois .
  • copilot-theorem: Examples do not compile #692; potentially for @chathhorn-galois .
  • Eliminate some unnecessary extensions (see: Planning for Copilot 4.6.1 #684 (comment)); potentially for @carte731 (partly already done).

• Other ideas / stretch goals:

  • Warnings when uploading packages #690
  • copilot-c99: Raise error when compiling an empty array or struct #695
  • Update the documentation for the Bluespec backend (?).
  • This list of libraries doesn't include all packages in the Copilot project: https://github.com/Copilot-Language/copilot?tab=readme-ov-file#api-documentation-and-tutorials

Please comment below if you are available to help out with this release, and if there's an issue you'd like to work on or you think we should be adding to this release.

The last release was hard to finish on time because it took me more than anticipated to catch up after I returned from holidays.

For the upcoming release (4.7), everything has to be merged by Feb 21. We have over a month for planning, implementation, testing & acceptance.

[RyanGlScott]

We're certainly willing to contribute some patches for the 4.7 release! Feel free to assign myself, @tkann-galois, and @chathhorn-galois to the issues you list above.

[ivanperez-keera]

Noted. Thanks!

[chathhorn-galois]

Can I officially take on at least #692 and #695?

[ivanperez-keera]

@chathhorn-galois Please wait until I assign it. I need to sit with the plan.

[ivanperez-keera]

@chathhorn-galois I thought someone from Galois already had a fix for #695. Was that you, was it someone else, or am I misremembering?

[chathhorn-galois]

Yes that was me: #649

[ivanperez-keera]

Thanks, @chathhorn-galois .

[agoodloe]

Yes, that should be fine. I want these fixed and I would like to come up with a few more examples. Maybe we can chat early next week.

[ivanperez-keera]

@chathhorn-galois Before you jump into implementing this please let me review the plan and officially assign it.

[ivanperez-keera]

@RyanGlScott what is the status wrt Kind2 support and Kind2 versions? I know we used to work with an older version only. Is that still the case? How difficult would it be to upgrade copilot-theorem to work with a current version?

[RyanGlScott]

what is the status wrt Kind2 support and Kind2 versions? I know we used to work with an older version only. Is that still the case?

Yes, that's correct. copilot-theorem's Kind2 backend currently requires Kind2-0.7.2 in order to work.

How difficult would it be to upgrade copilot-theorem to work with a current version?

This would require a non-trivial amount of work, I'm afraid.

copilot-theorem's Kind2 backend currently emits TransSys code, where TransSys is an S-expression-based intermediate language that Kind2 uses internally. Unfortunately, TransSys's syntax is not documented anywhere (as far as I can tell), and it has seen some backwards-incompatible changes over time. Specifically, TransSys's schema completely changed in Kind2-1.0, which means that Kind2-1.0 or later cannot parse TransSys code that copilot-theorem generates. (Note that Kind2 is currently on version 2.3.0, so it is possible that there may have been even more breaking changes to TransSys since the 1.0 series.)

If we wanted to continue to generate TransSys code, we'd need to investigate what the new schema for TransSys is and update copilot-theorem to generate code that adheres to the new schema. Given that the changes introduced in Kind2-1.0 are backwards-incompatible with pre-1.0 versions, this likely means that we'd have to drop support for pre-1.0 versions of Kind2. (Perhaps this is fine, given that Kind2-0.7.2 is over a decade old.)

Another alternative is to stop generating TransSys code and instead generate Lustre syntax, which Kind2 can also parse. I find this option somewhat appealing, as (1) this syntax is actually documented in Kind2's documentation, and (2) it appears to be more stable than TransSys. That being said, this would be a more ambitious change, given that Lustre syntax is quite different from TransSys.

[chathhorn-galois]

FWIW I'd volunteer to work on this whatever direction you'd like to go (Lustre or TransSys).

[ivanperez-keera]

I'd need to know more about this to understand how much work this is and which release it could be put under.

We should meet to discuss.

[ivanperez-keera]

Alwyn and I just talked about this. Once you are done with #695, can you please check out the new TransSys and try to estimate how difficult it would be to target it?

We don't need to create a prototype yet, we are just trying to know more to understand the level of effort it would require.