reference tests for easycrypt extraction

[cassiersg]

Tests that the easycrypt extraction matches vested "golden" files, up to insignificant whitespace changes.

[cassiersg]

@vbgl Do you know why the CI fails?

I see that https://gitlab.com/jasmin-lang/jasmin/-/jobs/7317501176 fails because of No such file or directory: './scripts/extract-and-check'.

Running nix-shell --run 'make -C compiler CHECKCATS="x86-64-extraction arm-m4-extraction" check' locally works.

[vbgl]

Is it really needed to store so many expected test results? Shouldn’t a checksum be enough to detect regressions?

[cassiersg]

That could be done indeed, but w'd loose:

1. the current fine-grained approach where we can ignore non-significant white-space changes
2. ease of reviewing what changes: currently, if the test fails, it displays a diff expected vs new. (Both when promoting the new reference files as a reviewer, and when reviewing the changes as a PR reviewer.)

It is debatable whether 1. is a good idea to have. For 2., I think that it's a significant annoyance.

The long-term plan of @eponier is to move this to dune "cramtest" (and extend it to also check assembly output).

We could also try to reduce the number of files by putting all the test results in a single file (tar-like, but in a human-readable format). Would that help to adress your concerns ? Is the issue more w.r.t. to the number of files, or with the amount of data in the repository ?

[vbgl]

I’m mostly concerned by the amount of data that is added there.

[cassiersg]

(To quantify: it's about 6.8 MB of data.)

I have no strong opinion (and I am not a maintainer), so I'm totally open to moving to hashes. We can always change the approach later if point 2. above ends up being too annoying. Should I move forward with a solution with hashes?