Erik Martin-Dorel

@CJs0800 FYI, two other links that may be useful for you to read, to understand the use of React in the frontend (app/ folder): - https://ocaml.org/p/react/latest/doc/React/index.html - https://erratique.ch/software/react/doc/

FYI @SkySkimmer * Pending GitLab pipeline: https://gitlab.com/coq-community/docker-coq/-/pipelines/1200744207 * List of Docker-Coq tags: https://hub.docker.com/r/coqorg/coq#supported-tags

* Related: https://github.com/ocaml-sf/learn-ocaml/issues/242

I was able to push another small commit (similar to the last-but-one). Now, the only remaining error raised by `make` is: ``` Error: Multiple rules generated for _build/install/default/lib/learn-ocaml/test_lib/test_lib.cmi: - src/grader/test_lib/dune:29...

> Should both flags behave the same? I believe so. FWIW, the behavior of the `-native-compiler` flag is well-documented in the [CEP 48](https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#regarding-item-2) (which is still up-to-date in this regard).

Normally this is `mathcomp/mathcomp:2.4.0-rocq-prover-9.0`. I'll double-check with the generated README anyway

OK I saw the issue, the PR I had approved too-quickly mentioned 9.00 instead of 9.0, will fix this.

FYI @proux01, you'll need to wait that this issue is closed: https://github.com/math-comp/docker-mathcomp/issues/35 I'll try my best to address it today. (See also this comment for more details: https://github.com/math-comp/docker-mathcomp/issues/35#issuecomment-2842395976 )

FYI @proux01 I just did a release of docker-keeper (that slightly extends its `images.yml` interpolation capabilities) **TL;DR:** if this pipeline succeeds https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/1171979, then you'll have a `mathcomp:2.4.0-rocq-prover-9.0` image; (then we'll...

FYI @proux01 : - Good news, `mathcomp/mathcomp:2.4.0-rocq-prover-9.0` and `mathcomp/mathcomp:2.4.0-rocq-prover-dev` were successfully built and deployed - Unfortunately, the `mathcomp/mathcomp:2.4.0-coq-8.19` build failed because of some HB/elpi error: https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5694374 ; any clue from...