Link binary with (recently added) features - Pancake

[mktnk3]

based on some feedback from the local Pancake users:

As more features are added, we often find ourselves in a situation where we have to figure out what features are supported by a particular binary we have at hand. This is certainly possible via some chasing, but it would be nice to have more direct ways to obtain such information, e.g.:

• add links to the corresponding PRs/commits/binary for each entry in pancake/NEWS.md (which connects human readable form to binary)
• add an option to binary that prints out the most recently added features (or even just the content of NEWS.md, up to the newly added features)

[IlmariReissumies]

The second option sounds easy to do, I'll take a stab at it :)

[KurtWu10]

The motivation for the issue is to improve the compatibility of Pancake programs, i.e. to enable programmers to write a single Pancake program that selects language features based on availability, similar to feature test macros in C.

For example, future versions of the compiler may support the bitwise negation operator. However, there is no easy way to write a single Pancake program text (with C macros) that uses the operator on newer compilers while using alternative implementations on older compilers.

[KurtWu10]

After discussing with the systems people (Julia @midnightveil), we decided that we will use the latest Pancake compiler for Microkit components for simplicity, and there may not be a need for such a feature.

[midnightveil]

Having such a feature where we can print a version is likely a good idea - we can at least provide a helpful error in our build system.

In theory also supporting a way to test for new features seems useful, but it's not critical at this stage (& for the amount of time we have to care about backcompat).

[KurtWu10]

currently we can print the version of the compiler

$ cake --version
The CakeML compiler

Version details:
Mon Aug 10 15:23:36 2026 UTC

CakeML: 2a49ebcb2da1d79e8d54bf130c203425d93e03e6
HOL4:   fac52534ceb43806d35b11f91dafd558266bcbb6
PolyML: Poly/ML 5.9 Release    RTS version: X86_64-5.9

[IlmariReissumies]

In theory also supporting a way to test for new features seems useful, but it's not critical at this stage (& for the amount of time we have to care about backcompat).

Okay good to know @midnightveil ! Even if it's not urgent, at this point I'll finish the PR anyway since I'm almost done with it :)

As a side note, it's not entirely obvious to me that you'd always be able to use the latest version. For example, if some other tooling you depend on (such as the Pancake to Viper pipeline) falls behind mainline Pancake a bit.

[midnightveil]

Yes, that's true. But I expect we'd at least use a consistent version, or the expected one.

I'm mostly thinking in terms that maintaining code to patch over the differences is usually more effort than updating or not updating.

[KurtWu10]

I expect we can collect different implementations in the same place, e.g. for inlining,

// in util.pnk
#ifdef INLINE_SUPPORTED
#define INLINE inline
#else
#define INLINE
#endif

// in driver code
INLINE fun f() {
  return 0;
}

I have already created a wrapper for bitwise_not(), which may be natively supported by future compilers.

[mktnk3]

As a side note, it's not entirely obvious to me that you'd always be able to use the latest version. For example, if some other tooling you depend on (such as the Pancake to Viper pipeline) falls behind mainline Pancake a bit.

This is indeed something to consider, because the "verified version" (to come) will depend on the Pancake-to-Viper transpiler, which is unlikely to be always available for latest version.

What Kurt suggested is a reasonable thing to have in general, I thought, not just for the specific context of Microkit/sDDF.

[midnightveil]

Yes. I agree it's useful, I just didn't think that it was worth the effort at this time.

[IlmariReissumies]

Now that #1470 is merged, I'll unassign myself from the issue. @mktnk3 do you want to close this issue now, or do you still think more work should be done at some point? If the latter, it would be good to clarify here what is still outstanding.