Emilio Jesús Gallego Arias

Even maybe we could call that `native_cmxs_gen=on`? But indeed, the problem of the number being quite meaningless in terms of performance still exists, IMHO we need to rethink the bench...

You already know but I probably unintentionally DOS'ed the bot triggering the minimizer.

I guess even a manual reporting process would be a marked improvement over the current situation, a bit of brainstorming on the implementation: - warning checking could be a special...

You can indeed use SerAPI to print a whole file in a slightly more controlled way, however this uses the same printer than the "beautifier", so you won't get terribly...

@spitters thanks for the link, you could implement that kind of script today in a robust way using SerAPI.

Indeed an alphabetically ordered list of faces would be the best thing IMO, with a short sentence for each one of us and a link.

Well the map is cute however it would be focused in 3 points so it wouldn't be too nice diversity-wise. IMO the developer list is more of a communication priority...

Indeed please avoid the system switch, using it is a 100% guarantee your system will become broken at some point. Compiling modern OCaml is pretty quick now that the multicore...

> 1. I would move jscoq (currently in "Standalone interfaces") in a different box entitled e.g. "Coq in the browser" or "online web interface" since it seems to be of...

Yes @Zimmi48 I mean jsCoq "2" which has its own branch here https://github.com/jscoq/jscoq/tree/v8.16+lsp (it was fully functional at some stage, but now needs a rebase)