Test-suite should enable native compilation

[ppedrot]

Version

Coq 8.8.

Description of the problem

Contrarily to the stdkib, the test-suite is compiled with automatic native compilation disabled. This prevents systematic checking of many kernel constructions that do not appear in the stdlib.

[gares]

@maximedenes IIRC most tests are not run via coqc but rather coqtop... can native be triggered in this case?

[maximedenes]

IIRC most tests are not run via coqc but rather coqtop... can native be triggered in this case?

No, indeed. IMHO the test suite should generate .vo files, also be compiled using the native compiler, and checked using coqchk. So maybe we can generalize this issue.

One step would be to stop using file names that are not valid for coqc in the test suite.

[Zimmi48]

One step would be to stop using file names that are not valid for coqc in the test suite.

Or to generalize what filenames are valid for coqc... Whether to do one or the other has been a long standing question if I'm not mistaken.

[maximedenes]

Good point, I'll open an issue so that we can discuss it.

[SkySkimmer]

It should be fairly easy to add some coqnative calls in the test suite nowadays.

[ejgallego]

@Alizter what's the status of this in your test-suite branch?

[Alizter]

@ejgallego native is not enabled since I don't know how to do the deps correctly. Currently the test suite pr doesn't work with any form of configure.

I have a coq native rule ready in there though, and it seems to work. But it would be good to support native enabled from the beginning.

[JasonGross]

This is fixed now, right?

[SkySkimmer]

When coq is configured with native enabled the test suite now runs with native ondemand AFAICT