[CI] Reenable jasmin

[eponier]

Jasmin was removed from CI in #20589 following changes in mathcomp (math-comp/math-comp#1256) that made the extraction to OCaml fail (see jasmin-lang/jasmin#1093 for the discussion).

We spent some time to make Jasmin (jasmin-lang/jasmin#1372) and its dependency coqword (jasmin-lang/coqword#37) avoid referencing the ring structures of mathcomp in the parts of Jasmin that are extracted (which were the reason of the failed extraction). Now that the changes are merged, extraction works again (we tested it with mathcomp 2.5, hopefully it works also with master), and I hope Jasmin can be enabled back in the CI.

[coqbot-app]

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

Doesn't seem to work

File "./lang/ident.v", line 29, characters 21-23:
Error: Syntax error: [def_body] expected after [ident_decl] (in [gallina]).

[SkySkimmer]

Seems like a conflict with #21611 removing of as an anonymous binder syntax outside constructors. Definition id_name & t : string := "". should work and be backwards compatible IIUC

[vbgl]

Thanks for the hint. I’ll apply the patch. And we’ll discover the next issue…

File "./lang/extraction.v", line 61, characters 0-364:
Error:
Anomaly
"File "kernel/environ.ml", line 929, characters 11-17: Assertion failed."

[SkySkimmer]

some module issue in extraction
cc @ppedrot

[coqbot-app]

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

[vbgl]

I’ve open an issue regarding the extraction issue: #21754