Add additional extraction language in plugins

[vbergeron]

Follow-up to #22487: allow plugins to add extraction languages.

• Table.lang gets External of string; Extraction Language accepts any registered identifier.

• Common.register_language registers a language_descr; built-in languages use it too.

• Per-language special cases move to language_descr fields: unquote, upper_types, char_type, string_type, modular, id_of_filename.

• error_scheme becomes error_not_modular, for any language, with a hint to use single-file extraction.

• Added / updated test-suite.

• Added changelog.

• Added / updated documentation.

  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

[SkySkimmer]

seems reasonable, if some other language needs more flexibility we can change the API later.

[SkySkimmer]

Do you have scala as an external plugin to add to CI?

[vbergeron]

Switched to CString.Map and to an expected output file, thanks.
The Scala plugin isn't published yet; I'll add it to CI in a follow-up PR once it is !

[SkySkimmer]

@coqbot run full ci

[ppedrot]

Also, a naive question to @vbergeron: what were the limitations of the JSON export that prevented you from writing your code directly above it?

[vbergeron]

Also, a naive question to @vbergeron: what were the limitations of the JSON export that prevented you from writing your code directly above it?
Hello !

The JSON export drops some information the proposed Scala backend relies on:

• ind_kind: coinductives and records come out as plain decl:ind, so no laziness for coinductives and no field names for records
• cofix and fix are both printed as decl:fixgroup
• custom matches from Extract Inductive are ignored, and custom types with parameters are flattened to a name
• the scrutinee type of match, which I use to drop unneeded casts.

An external translator would also have to redo the keyword/case renaming that Common already does without clashes.

Last but not least, the JSON backend is marked as for "development and debugging". Enriching and stabilizing the format seemed like a bigger commitment than a plugin API.

Happy to discuss it further if needed